Rational Numbers

The rationals will be defined in terms of a pair of integers. \(\mathbb{Q} = \mathbb{Z}\times \mathbb{Z}_{\neq 0} / \langle (x,y)\sim(w,z) \iff xz=wy \rangle \). Strictly speaking we should include a proof that the second argument is non-zero in the constructor, however for brevity we omit this. To create a positive and negative rationals: For convenience we can also just write the number as a decimal and it will convert it to a rational number.
We can multply two natural numbers together:
And add them:
Equality:

Strictly speaking the constructor should be of this type: