Constructing ℤ, ℚ and ℝ

With $(a, b) \sim (c, d)$ iff $a + d = c + b$, which pairs of natural numbers lie in the class that represents the integer $-2$? (Choose all that apply.)

Using $[(a, b)] \cdot [(c, d)] = [(ac + bd,\, ad + bc)]$, compute $[(3, 5)] \cdot [(4, 1)]$. Which integer does the resulting class represent?

In the proof that equality of fractions ($ad = cb$) is transitive, from $ad = cb$ and $cf = ed$ we derive $(af)d = (eb)d$. Which step needs the hypothesis that the ring has no zero divisors?

Each rule below is defined on a representative $a/b$ (or two, $a/b$ and $c/d$) of a rational number, with $b, d \neq 0$. Which rules are not well defined as functions of the rational numbers? (Choose all that apply.)

Which of these subsets of $\Q$ are Dedekind cuts (non-empty, not all of $\Q$, closed downwards, no greatest element)? (Choose all that apply.)

Which example shows that $\Q$ is not complete (that not every non-empty, bounded-above subset has a least upper bound in $\Q$)?

In the lesson's Lean file, PairInt.add is defined with Quotient.map₂ (fun p q => (p.1 + q.1, p.2 + q.2)) (proof). What is the second argument, and what happens if you leave it out?

Implement the integers as pairs of natural numbers. Write canonical(p), returning the representative of the class of p that has a $0$ in at least one coordinate, and mul(p, q) using $(a, b)(c, d) = (ac + bd, ad + bc)$. Then check, for all pairs with entries up to $5$, that mul is well defined: equivalent inputs give outputs with the same canonical form.