Rat

-- ℚ: Rat/frac.nova's Rat quotiented by CROSS-MULTIPLICATION,
-- n₁/d₁ ~ n₂/d₂ iff n₁·d₂ ≡ n₂·d₁ in Int. The relation is stated with
-- Int/mul.nova's intMul on the denominators' images under nzToInt;
-- code-quot takes an arbitrary Ω relation, so nothing has to be proved
-- about it up front (it IS an equivalence — denominators are non-zero
-- and Int is a domain — but the quotient does not ask).
-- ===== the bridge from scaling to multiplication =====
-- intScale d z is multiplication by d's image: on representatives the
-- two differ only by a Z*x summand

import Natural (+, *, plusZeroId, zeroPlusId, plusComm, plusAssoc, sucPlus, multZeroId, multSucId, zeroMult, sucMult, multComm, multDistrib, multAssoc)
import Int (Int, intZero, intOne, intNeg)
import Int.add (+, intAddComm, intAddAssoc)
import Int.mul (*, intMulComm, intMulAssoc, intMulOneL, intMulOneR, intMulZeroL, intMulZeroR, intMulDistribL, intMulDistribR, intAddCong2, intMulCong2, classCong2, oneMult, intNegNeg, intAddNegR, intMulNegL)
import Rat.frac (NZ, nzPos, nzNeg, nzOne, nzMul, nzMulComm, nzMulOneL, nzMulOneR, nzToInt, intScale, intScaleOne, Rat, mkRat, num, den, denInt, ratAdd, ratAddComm, ratAddZeroL, ratAddZeroR, ratNeg, ratZero, ratOne, ratEta, half, third)
import Natural.eq (predEq)
import Core.equality (trans, cong, sym, paireta)

intScaleIsMul : (d : NZ) (z : Int) → intScale d z ≡ nzToInt d * z
  using (Int.Int.eq,
    Int.Int.unfold,
    Int.intNeg.eq,
    Int.mul.*.eq,
    plusZeroId.rw,
    Rat.frac.NZ.unfold,
    Rat.frac.intScale.eq,
    Rat.frac.intScaleN.eq,
    Rat.frac.nzNeg.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    zeroMult.rw,
    zeroPlusId.rw)
intScaleIsMul =
  λd z. ⊎-elim
    n. quot-elim (v. intScale (nzPos n) v ≡ nzToInt (nzPos n) * v) (p. ⋆) z
    n. quot-elim (v. intScale (nzNeg n) v ≡ nzToInt (nzNeg n) * v) (p. ⋆) z
    d

-- (m+1)(k+1) = mk + m + k + 1: the magnitude law behind nzMul
-- a + (b + c) ≡ c + (a + b), the rotation strict-mode descent needs
addRot : (a b c : ℕ) → a + (b + c) ≡ c + (a + b)
addRot = λa b c. trans _ _ _ (sym _ _ (plusAssoc a b c)) (plusComm c (a + b))

sucMulSuc : (m k : ℕ) → S m * S k ≡ S (m * k + m + k)
sucMulSuc =
  λm k. S m * S k
    ≡⟨ multSucId (S m) k ⟩ S m + S m * k
    ≡⟨ sucMult m k ⟩ S m + (k + m * k)
    ≡⟨ sucPlus m (k + m * k) ⟩ S (m + (k + m * k))
    ≡⟨ addRot m k (m * k) ⟩ S (m * k + (m + k))
    ≡⟨ plusAssoc (m * k) m k ⟩ S (m * k + m + k)

-- nzToInt is multiplicative
nzToIntMul : (d e : NZ) → nzToInt (nzMul d e) ≡ nzToInt d * nzToInt e
  using (Int.Int.eq,
    Int.mul.*.eq,
    multZeroId.rw,
    Natural.sucPlus,
    plusAssoc,
    plusZeroId.rw,
    Rat.frac.NZ.unfold,
    Rat.frac.nzMul.eq,
    Rat.frac.nzNeg.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    sucMulSuc,
    zeroMult,
    zeroMult.rw,
    zeroPlusId,
    zeroPlusId.rw)
nzToIntMul =
  λd e. ⊎-elim
    m. ⊎-elim (v. nzToInt (nzMul (nzPos m) v) ≡ nzToInt (nzPos m) * nzToInt v) (k. ⋆) (k. ⋆) e
    m. ⊎-elim (v. nzToInt (nzMul (nzNeg m) v) ≡ nzToInt (nzNeg m) * nzToInt v) (k. ⋆) (k. ⋆) e
    d

-- ===== rearranging four-fold products =====
--
-- intMulComm and intMulAssoc are both permutative, so they never
-- rewrite; every rearrangement has to be a chain of explicit
-- congruences. These three build the one permutation the descent
-- needs: swapping the outer two factors of (a·b)·(c·d).
mulCongL : (x y z : Int) → (x ≡ y) → x * z ≡ y * z using (Int.Int.unfold, Int.mul.intMulCong2)
mulCongL = λx y z h. ⋆

mulCongR : (x y z : Int) → (y ≡ z) → x * y ≡ x * z using (Int.Int.unfold, Int.mul.intMulCong2)
mulCongR = λx y z h. ⋆

-- x·(y·z) ≡ y·(x·z)
mulSwapHead : (x y z : Int) → x * (y * z) ≡ y * (x * z) using (intMulAssoc)
mulSwapHead =
  λx y z. trans
    _
    _
    _
    sym _ _ (intMulAssoc x y z)
    trans _ _ _ (mulCongL _ _ z (intMulComm x y)) (intMulAssoc y x z)

-- a·(c·d) ≡ d·(c·a)
mulSwapInner : (a c d : Int) → a * (c * d) ≡ d * (c * a)
mulSwapInner =
  λa c d. trans
    _
    _
    _
    mulSwapHead a c d
    trans _ _ _ (mulCongR c _ _ (intMulComm a d)) (sym _ _ (mulSwapHead d c a))

-- (a·b)·(c·d) ≡ (d·b)·(c·a)
mulSwapOuter : (a b c d : Int) → a * b * (c * d) ≡ d * b * (c * a)
mulSwapOuter =
  λa b c d. trans
    _
    _
    _
    intMulAssoc a b (c * d)
    trans
      _
      _
      _
      mulSwapHead a b (c * d)
      trans
        _
        _
        _
        mulCongR b _ _ (mulSwapInner a c d)
        trans _ _ _ (mulSwapHead b d (c * a)) (sym _ _ (intMulAssoc d b (c * a)))

-- ===== the quotient =====
dInt : Rat → Int using (Int.Int.unfold)
dInt = λp. nzToInt (den p)

RatR : Rat → Rat → Ω
RatR = λp q. num p * dInt q ≡ num q * dInt p

Q : 𝕌
Q = Rat / (x y. RatR x y)

qcls : Rat → Q using (Rat.Q.unfold)
qcls = λp. class p

-- ½ and 2/4 are the same rational
qHalfTest : qcls half ≡ qcls (mkRat (class (2, Z)) (nzPos 3))
  using (Int.Int.eq,
    Int.Int.unfold,
    Int.intOne.eq,
    Int.mul.*.eq,
    Natural.*.eq,
    Natural.+.eq,
    Rat.frac.Rat.eq,
    Rat.frac.den.eq,
    Rat.frac.half.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    Rat.Q.eq,
    Rat.RatR.eq,
    Rat.dInt.eq,
    Rat.qcls.eq)
qHalfTest = ⋆

-- ===== well-definedness of addition on ℚ =====
-- the arithmetic heart, stated purely in Int: cross-multiplying the
-- two sums and cancelling. Expand both products by right
-- distributivity; the n₁-terms are the SAME four factors rearranged,
-- and the n₂-terms differ exactly by the hypothesis.
crossAddWD : {n1 d1 n2 d2 n3 d3 : Int}
  (h : n2 * d3 ≡ n3 * d2)
  → (d2 * n1 + d1 * n2) * (d1 * d3) ≡ (d3 * n1 + d1 * n3) * (d1 * d2)
crossAddWD =
  λn1 d1 n2 d2 n3 d3 h. trans
    _
    _
    _
    intMulDistribR (d2 * n1) (d1 * n2) (d1 * d3)
    trans
      _
      _
      _
      intAddCong2
        _
        _
        _
        _
        mulSwapOuter d2 n1 d1 d3
        trans
          _
          _
          _
          mulSwapOuter d1 n2 d1 d3
          trans
            _
            _
            _
            mulCongL
              _
              _
              d1 * d1
              trans _ _ _ (intMulComm d3 n2) (trans _ _ _ h (intMulComm n3 d2))
            sym _ _ (mulSwapOuter d1 n3 d1 d2)
      sym _ _ (intMulDistribR (d3 * n1) (d1 * n3) (d1 * d2))

-- ratAdd's two components, in intMul form
ratAddNumMul : (p q : Rat) → num (ratAdd p q) ≡ dInt q * num p + dInt p * num q
  using (Int.Int.unfold,
    Int.intNeg.eq,
    Int.add.+.eq,
    Int.mul.*.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.intScale.eq,
    Rat.frac.intScaleN.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzToInt.eq,
    Rat.frac.ratAdd.eq,
    Rat.dInt.eq)
ratAddNumMul =
  λp q. intAddCong2 _ _ _ _ (intScaleIsMul (den q) (num p)) (intScaleIsMul (den p) (num q))

ratAddDenMul : (p q : Rat) → dInt (ratAdd p q) ≡ dInt p * dInt q
  using (Int.Int.unfold,
    Int.add.+.eq,
    Int.mul.*.eq,
    nzToIntMul,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.intScale.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzNeg.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    Rat.frac.ratAdd.eq,
    Rat.dInt.eq)
ratAddDenMul = λp q. nzToIntMul (den p) (den q)

-- the relation instance the inner well-definedness goal reduces to
-- inner well-definedness of ratAdd — explicit trans (a calc chain's
-- steps rewrite inside quot-elim scrutinees, which strict replay
-- rejects; the same route as lemma applications is unconstrained)
qAddWDInner : (p : Rat)
  {q q' : Rat}
  (h : RatR q q')
  → num (ratAdd p q) * dInt (ratAdd p q') ≡ num (ratAdd p q') * dInt (ratAdd p q)
  using (Int.Int.unfold, Rat.frac.NZ.unfold, Rat.frac.Rat.unfold, Rat.RatR.eq, Rat.RatR.unfold)
qAddWDInner =
  λp q q' h. trans
    _
    _
    _
    intMulCong2 _ _ _ _ (ratAddNumMul p q) (ratAddDenMul p q')
    trans
      {Int}
      (dInt q * num p + dInt p * num q) * (dInt p * dInt q')
      (dInt q' * num p + dInt p * num q') * (dInt p * dInt q)
      _
      crossAddWD h
      sym _ _ (intMulCong2 _ _ _ _ (ratAddNumMul p q') (ratAddDenMul p q))

-- el-quot-eq: a proof of the relation gives equal classes
clsEqOfRel : (p q : Rat) → RatR p q → class p ≡ class q ∈ Q
  using (Q.eq,
    RatR.eq,
    Int.Int.unfold,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.eq,
    Rat.frac.Rat.unfold,
    Rat.Q.unfold,
    Rat.RatR.unfold)
clsEqOfRel = λp q h. ⋆

qAddWDInnerCls : {p q q' : Rat} (h : RatR q q') → class (ratAdd p q) ≡ class (ratAdd p q') ∈ Q
  using (Int.Int.eq,
    Int.Int.unfold,
    Int.mul.*.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.num.eq,
    Rat.frac.ratAdd.eq,
    Rat.Q.unfold,
    Rat.RatR.eq,
    Rat.RatR.unfold,
    Rat.dInt.eq)
qAddWDInnerCls = λp q q' h. clsEqOfRel _ _ (qAddWDInner p h)

-- the OUTER case needs no new arithmetic: ratAddComm turns it into
-- the inner one with the arguments swapped
qAddWDOuterCls : {p p' c : Rat} (h : RatR p p') → class (ratAdd p c) ≡ class (ratAdd p' c) ∈ Q
  using (Rat.Q.unfold)
qAddWDOuterCls =
  λp p' c h. trans
    _
    _
    _
    cong (λu. Q) (λr. class r) (ratAddComm p c)
    trans
      {Q}
      class (ratAdd c p)
      class (ratAdd c p')
      _
      qAddWDInnerCls h
      cong (λu. Q) (λr. class r) (sym _ _ (ratAddComm p' c))

-- ...in the quot-elim shape the elaborator asks for
qAddWDOuter : (p p' : Rat)
  (h : RatR p p')
  (v : Q)
  → quot-elim (w. Q) (x. class (ratAdd p x)) v ≡ quot-elim (x. class (ratAdd p' x)) v
  using (Int.Int.unfold,
    qAddWDInnerCls,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.Q.unfold,
    Rat.RatR.unfold)
qAddWDOuter =
  λp p' h v. quot-elim
    w. quot-elim (z. Q) (x. class (ratAdd p x)) w ≡ quot-elim (x. class (ratAdd p' x)) w
    c. qAddWDOuterCls h
    v

infixl 6 +
+ : Q → Q → Q
  using (Int.Int.unfold,
    qAddWDInnerCls,
    qAddWDOuter,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.Q.unfold,
    Rat.RatR.unfold)
(+) = λu v. quot-elim (p. quot-elim (q. class (ratAdd p q)) v) u

-- ===== ℚ, at last =====
qZero : Q using (Rat.Q.unfold)
qZero = qcls ratZero

qOne : Q using (Rat.Q.unfold)
qOne = qcls ratOne

-- β: addition on ℚ is ratAdd on representatives
qAddCls : (p q : Rat) → qcls p + qcls q ≡ qcls (ratAdd p q)
  using (Int.Int.unfold,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.ratAdd.eq,
    Rat.Q.unfold,
    Rat.+.eq,
    Rat.qcls.eq)
qAddCls = λp q. ⋆

-- ½ + ½ = 1. On Rat this was 4/4; the quotient identifies it with 1/1
qAddHalves : qcls half + qcls half ≡ qOne
  using (clsEqOfRel,
    Int.Int.eq,
    Int.intOne.eq,
    Int.add.+.eq,
    Int.mul.*.eq,
    Natural.*.eq,
    Natural.+.eq,
    Rat.frac.Rat.eq,
    Rat.frac.den.eq,
    Rat.frac.half.eq,
    Rat.frac.intScale.eq,
    Rat.frac.intScaleN.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzOne.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    Rat.frac.ratAdd.eq,
    Rat.frac.ratOfInt.eq,
    Rat.frac.ratOne.eq,
    Rat.Q.eq,
    Rat.RatR.eq,
    Rat.dInt.eq,
    Rat.+.eq,
    Rat.qOne.eq,
    Rat.qcls.eq)
qAddHalves = ⋆

-- ⅓ + ⅓ = ⅔
qAddThirds : qcls third + qcls third ≡ qcls (mkRat (class (2, Z)) (nzPos 2))
  using (clsEqOfRel,
    Int.Int.eq,
    Int.Int.unfold,
    Int.intOne.eq,
    Int.add.+.eq,
    Int.mul.*.eq,
    Natural.*.eq,
    Natural.+.eq,
    Rat.frac.Rat.eq,
    Rat.frac.den.eq,
    Rat.frac.intScale.eq,
    Rat.frac.intScaleN.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    Rat.frac.ratAdd.eq,
    Rat.frac.third.eq,
    Rat.Q.eq,
    Rat.RatR.eq,
    Rat.dInt.eq,
    Rat.+.eq,
    Rat.qcls.eq)
qAddThirds = ⋆

qAddComm : (u v : Q) → u + v ≡ v + u
  using (Int.Int.unfold,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.ratAdd.eq,
    Rat.Q.unfold,
    Rat.RatR.unfold,
    Rat.+.eq)
qAddComm = λu v. quot-elim (p. quot-elim (q. cong (λx. Q) (λr. class r) (ratAddComm p q)) v) u

qAddZeroL : (u : Q) → qZero + u ≡ u
  using (Int.Int.unfold,
    Int.intZero.eq,
    Int.add.+.eq,
    nzMulOneL,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.intScale.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.ratAdd.eq,
    Rat.frac.ratOfInt.eq,
    Rat.frac.ratZero.eq,
    Rat.Q.unfold,
    Rat.RatR.unfold,
    Rat.+.eq,
    Rat.qZero.eq,
    Rat.qcls.eq)
qAddZeroL = λu. quot-elim (p. cong (λx. Q) (λr. class r) {ratAdd ratZero p} {p} ratAddZeroL) u

qAddZeroR : (u : Q) → u + qZero ≡ u
  using (Int.Int.unfold,
    Int.intZero.eq,
    Int.add.+.eq,
    nzMulOneR,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.intScale.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.ratAdd.eq,
    Rat.frac.ratOfInt.eq,
    Rat.frac.ratZero.eq,
    Rat.Q.unfold,
    Rat.RatR.unfold,
    Rat.+.eq,
    Rat.qZero.eq,
    Rat.qcls.eq)
qAddZeroR = λu. quot-elim (p. cong (λx. Q) (λr. class r) {ratAdd p ratZero} {p} ratAddZeroR) u

-- ===== associativity =====
-- The magnitudes of nzMul associate. Rather than permute the seven
-- monomials of ((mk+m+k)l + (mk+m+k) + l) by hand, go through the
-- SUCCESSORS: S of each side is a product of S m, S k, S l by
-- sucMulSuc, multAssoc equates those, and S is injective
-- (Natural/eq.nova's predEq).
magAssoc : {m k l : ℕ}
  → (m * k + m + k) * l + (m * k + m + k) + l ≡ m * (k * l + k + l) + m + (k * l + k + l)
  using (plusAssoc, Natural.sucPlus, zeroPlusId)
magAssoc =
  λm k l. predEq
    {Z + ((m * k + m + k) * l + (m * k + m + k) + l)}
    {Z + (m * (k * l + k + l) + m + (k * l + k + l))}
    trans
      S ((m * k + m + k) * l + (m * k + m + k) + l)
      _
      S (m * (k * l + k + l) + m + (k * l + k + l))
      sym _ _ (sucMulSuc (m * k + m + k) l)
      trans
        _
        _
        _
        trans
          _
          _
          _
          cong (λu. ℕ) (λw. w * S l) (sym _ _ (sucMulSuc m k))
          multAssoc (S m) (S k) (S l)
        trans _ _ _ (cong (λu. ℕ) (λw. S m * w) (sucMulSuc k l)) (sucMulSuc m (k * l + k + l))

-- eight sign cases, one magnitude law
nzMulAssoc : (x y z : NZ) → nzMul (nzMul x y) z ≡ nzMul x (nzMul y z)
  using (magAssoc,
    plusAssoc,
    Rat.frac.NZ.unfold,
    Rat.frac.nzMul.eq,
    Rat.frac.nzNeg.eq,
    Rat.frac.nzPos.eq)
nzMulAssoc =
  λx y z. ⊎-elim
    m. ⊎-elim
      b. nzMul (nzMul (nzPos m) b) z ≡ nzMul (nzPos m) (nzMul b z)
      k. ⊎-elim
        c. nzMul (nzMul (nzPos m) (nzPos k)) c ≡ nzMul (nzPos m) (nzMul (nzPos k) c)
        l. cong
          λu. NZ
          nzPos
          {(m * k + m + k) * l + (m * k + m + k) + l}
          {m * (k * l + k + l) + m + (k * l + k + l)}
          magAssoc
        l. cong
          λu. NZ
          nzNeg
          {(m * k + m + k) * l + (m * k + m + k) + l}
          {m * (k * l + k + l) + m + (k * l + k + l)}
          magAssoc
        z
      k. ⊎-elim
        c. nzMul (nzMul (nzPos m) (nzNeg k)) c ≡ nzMul (nzPos m) (nzMul (nzNeg k) c)
        l. cong
          λu. NZ
          nzNeg
          {(m * k + m + k) * l + (m * k + m + k) + l}
          {m * (k * l + k + l) + m + (k * l + k + l)}
          magAssoc
        l. cong
          λu. NZ
          nzPos
          {(m * k + m + k) * l + (m * k + m + k) + l}
          {m * (k * l + k + l) + m + (k * l + k + l)}
          magAssoc
        z
      y
    m. ⊎-elim
      b. nzMul (nzMul (nzNeg m) b) z ≡ nzMul (nzNeg m) (nzMul b z)
      k. ⊎-elim
        c. nzMul (nzMul (nzNeg m) (nzPos k)) c ≡ nzMul (nzNeg m) (nzMul (nzPos k) c)
        l. cong
          λu. NZ
          nzNeg
          {(m * k + m + k) * l + (m * k + m + k) + l}
          {m * (k * l + k + l) + m + (k * l + k + l)}
          magAssoc
        l. cong
          λu. NZ
          nzPos
          {(m * k + m + k) * l + (m * k + m + k) + l}
          {m * (k * l + k + l) + m + (k * l + k + l)}
          magAssoc
        z
      k. ⊎-elim
        c. nzMul (nzMul (nzNeg m) (nzNeg k)) c ≡ nzMul (nzNeg m) (nzMul (nzNeg k) c)
        l. cong
          λu. NZ
          nzPos
          {(m * k + m + k) * l + (m * k + m + k) + l}
          {m * (k * l + k + l) + m + (k * l + k + l)}
          magAssoc
        l. cong
          λu. NZ
          nzNeg
          {(m * k + m + k) * l + (m * k + m + k) + l}
          {m * (k * l + k + l) + m + (k * l + k + l)}
          magAssoc
        z
      y
    x

-- the numerator identity behind associativity, in Int: distribute the
-- outer factor on both sides and match the three monomials
crossAssocNum : {n1 d1 n2 d2 n3 d3 : Int}
  → d3 * (d2 * n1 + d1 * n2) + d1 * d2 * n3 ≡ d2 * d3 * n1 + d1 * (d3 * n2 + d2 * n3)
  using (intMulAssoc)
crossAssocNum =
  λn1 d1 n2 d2 n3 d3. trans
    _
    _
    _
    intAddCong2 _ (d1 * d2 * n3) _ (d1 * d2 * n3) (intMulDistribL d3 (d2 * n1) (d1 * n2)) ⋆
    trans
      _
      _
      _
      intAddAssoc (d3 * (d2 * n1)) (d3 * (d1 * n2)) (d1 * d2 * n3)
      trans
        _
        _
        _
        intAddCong2
          _
          _
          _
          _
          trans _ _ _ (sym _ _ (intMulAssoc d3 d2 n1)) (mulCongL _ _ n1 (intMulComm d3 d2))
          intAddCong2 _ _ _ _ (mulSwapHead d3 d1 n2) (intMulAssoc d1 d2 n3)
        intAddCong2
          d2 * d3 * n1
          _
          d2 * d3 * n1
          _
          ⋆
          sym _ _ (intMulDistribL d1 (d3 * n2) (d2 * n3))

-- the two composite numerators, expanded into intMul form
ratAddNumMulL : {p q r : Rat}
  → num (ratAdd (ratAdd p q) r)
    ≡ dInt r * (dInt q * num p + dInt p * num q) + dInt p * dInt q * num r
  using (intMulAssoc, nzToIntMul)
ratAddNumMulL =
  λp q r. trans
    _
    _
    _
    ratAddNumMul (ratAdd p q) r
    intAddCong2
      _
      _
      _
      _
      intMulCong2 (dInt r) _ (dInt r) _ ⋆ (ratAddNumMul p q)
      intMulCong2 _ (num r) _ (num r) (ratAddDenMul p q) ⋆

ratAddNumMulR : (p q r : Rat)
  → num (ratAdd p (ratAdd q r))
    ≡ dInt q * dInt r * num p + dInt p * (dInt r * num q + dInt q * num r)
  using (intMulAssoc, nzToIntMul)
ratAddNumMulR =
  λp q r. trans
    _
    _
    _
    ratAddNumMul p (ratAdd q r)
    intAddCong2
      _
      _
      _
      _
      intMulCong2 _ (num p) _ (num p) (ratAddDenMul q r) ⋆
      intMulCong2 (dInt p) _ (dInt p) _ ⋆ (ratAddNumMul q r)

ratAddAssocNum : {p q r : Rat} → num (ratAdd (ratAdd p q) r) ≡ num (ratAdd p (ratAdd q r))
ratAddAssocNum =
  λp q r. trans
    _
    _
    _
    ratAddNumMulL
    trans
      dInt r * (dInt q * num p + dInt p * num q) + dInt p * dInt q * num r
      _
      _
      crossAssocNum
      sym _ _ (ratAddNumMulR p q r)

-- the denominators associate on the nose, by nzMulAssoc
ratAddAssocDen : {p q r : Rat} → den (ratAdd (ratAdd p q) r) ≡ den (ratAdd p (ratAdd q r))
  using (Int.Int.unfold,
    Int.add.+.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.intScale.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzNeg.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.ratAdd.eq)
ratAddAssocDen = λp q r. nzMulAssoc (den p) (den q) (den r)

-- so addition is associative already on Rat — no quotient needed
ratAddAssoc : {p q r : Rat} → ratAdd (ratAdd p q) r ≡ ratAdd p (ratAdd q r)
  using (Int.Int.unfold, Rat.frac.NZ.unfold, Rat.frac.Rat.unfold, Rat.frac.ratEta)
ratAddAssoc =
  λp q r. trans
    _
    mkRat (num (ratAdd p (ratAdd q r))) (den (ratAdd (ratAdd p q) r))
    _
    cong
      λu. Rat
      λx. mkRat x (den (ratAdd (ratAdd p q) r))
      {num (ratAdd (ratAdd p q) r)}
      {num (ratAdd p (ratAdd q r))}
      ratAddAssocNum
    cong
      λu. Rat
      λd. mkRat (num (ratAdd p (ratAdd q r))) d
      {den (ratAdd (ratAdd p q) r)}
      {den (ratAdd p (ratAdd q r))}
      ratAddAssocDen

qAddAssoc : (u v w : Q) → u + v + w ≡ u + (v + w)
  using (Int.Int.unfold,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.ratAdd.eq,
    Rat.Q.unfold,
    Rat.RatR.unfold,
    Rat.+.eq)
qAddAssoc =
  λu v w. quot-elim
    p. quot-elim
      q. quot-elim
        r. cong (λx. Q) (λt. class t) {ratAdd (ratAdd p q) r} {ratAdd p (ratAdd q r)} ratAddAssoc
        w
      v
    u

-- ⅓ + (⅓ + ⅓) = 1, the associated way round
qAddThirdsAssoc : qcls third + (qcls third + qcls third) ≡ qOne
  using (clsEqOfRel,
    Int.Int.eq,
    Int.intOne.eq,
    Int.add.+.eq,
    Int.mul.*.eq,
    Natural.*.eq,
    Natural.+.eq,
    Rat.frac.Rat.eq,
    Rat.frac.den.eq,
    Rat.frac.intScale.eq,
    Rat.frac.intScaleN.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzOne.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    Rat.frac.ratAdd.eq,
    Rat.frac.ratOfInt.eq,
    Rat.frac.ratOne.eq,
    Rat.frac.third.eq,
    Rat.Q.eq,
    Rat.RatR.eq,
    Rat.dInt.eq,
    Rat.+.eq,
    Rat.qOne.eq,
    Rat.qcls.eq)
qAddThirdsAssoc = ⋆

-- ===== negation: ℚ is a group =====
-- negation respects the relation: (−n₁)·d₁′ ≡ −(n₁·d₁′) ≡ −(n₁′·d₁)
ratNegWD : {p p' : Rat}
  (h : RatR p p')
  → num (ratNeg p) * dInt (ratNeg p') ≡ num (ratNeg p') * dInt (ratNeg p)
  using (intMulNegL,
    Int.Int.eq,
    Int.Int.unfold,
    Int.intNeg.eq,
    Int.mul.*.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzToInt.eq,
    Rat.frac.ratNeg.eq,
    Rat.RatR.eq,
    Rat.RatR.unfold,
    Rat.dInt.eq)
ratNegWD =
  λp p' h. trans
    _
    _
    _
    intMulNegL (num p) (dInt p')
    trans
      _
      _
      num (ratNeg p') * dInt (ratNeg p)
      cong (λu. Int) intNeg {num p * dInt p'} {num p' * dInt p} h
      sym _ _ (intMulNegL (num p') (dInt p))

ratNegWDCls : (p p' : Rat) (h : RatR p p') → class (ratNeg p) ≡ class (ratNeg p') ∈ Q
  using (intMulNegL,
    Int.Int.eq,
    Int.Int.unfold,
    Int.mul.*.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.num.eq,
    Rat.frac.ratNeg.eq,
    Rat.Q.unfold,
    Rat.RatR.eq,
    Rat.RatR.unfold,
    Rat.dInt.eq)
ratNegWDCls = λp p' h. clsEqOfRel _ _ (ratNegWD h)

qNeg : Q → Q
  using (Int.Int.unfold,
    ratNegWDCls,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.Q.unfold,
    Rat.RatR.unfold)
qNeg = λu. quot-elim (p. class (ratNeg p)) u

qNegCls : (p : Rat) → qNeg (qcls p) ≡ qcls (ratNeg p)
  using (Int.Int.unfold,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.ratNeg.eq,
    Rat.Q.unfold,
    Rat.qNeg.eq,
    Rat.qcls.eq)
qNegCls = λp. ⋆

-- p + (−p) has numerator zero: collect the common denominator and use
-- z + (−z) ≡ 0 in Int
ratAddNegNum : (p : Rat) → num (ratAdd p (ratNeg p)) ≡ intZero
  using (intAddNegR,
    intMulZeroR,
    Int.Int.unfold,
    Int.intNeg.eq,
    Int.add.+.eq,
    Int.mul.*.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzToInt.eq,
    Rat.frac.ratNeg.eq,
    Rat.dInt.eq)
ratAddNegNum =
  λp. trans
    _
    dInt p * num p + dInt p * intNeg (num p)
    _
    ratAddNumMul p (ratNeg p)
    trans
      _
      _
      _
      sym _ _ (intMulDistribL (dInt p) (num p) (intNeg (num p)))
      trans _ _ intZero (mulCongR (dInt p) _ _ (intAddNegR (num p))) intMulZeroR

-- ...so p + (−p) is 0/(d²), which the quotient identifies with 0/1.
-- This is the first law that is NOT already true on Rat.
ratAddNegRel : (p : Rat)
  → num (ratAdd p (ratNeg p)) * dInt ratZero ≡ num ratZero * dInt (ratAdd p (ratNeg p))
  using (Int.Int.unfold,
    Int.intNeg.eq,
    Int.intZero.eq,
    Int.add.+.eq,
    Int.mul.*.eq,
    ratAddNegNum,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.intScale.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzToInt.eq,
    Rat.frac.ratAdd.eq,
    Rat.frac.ratNeg.eq,
    Rat.frac.ratOfInt.eq,
    Rat.frac.ratZero.eq,
    Rat.dInt.eq)
ratAddNegRel =
  λp. trans
    _
    _
    _
    trans _ _ _ (mulCongL _ _ (dInt ratZero) (ratAddNegNum p)) (intMulZeroL (dInt ratZero))
    sym _ _ (intMulZeroL (dInt (ratAdd p (ratNeg p))))

qAddNegR : (u : Q) → u + qNeg u ≡ qZero
  using (Int.Int.eq,
    Int.Int.unfold,
    Int.intZero.eq,
    Int.mul.*.eq,
    ratAddNegNum,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.num.eq,
    Rat.frac.ratAdd.eq,
    Rat.frac.ratNeg.eq,
    Rat.frac.ratOfInt.eq,
    Rat.frac.ratZero.eq,
    Rat.Q.unfold,
    Rat.RatR.eq,
    Rat.RatR.unfold,
    Rat.dInt.eq,
    Rat.+.eq,
    Rat.qNeg.eq,
    Rat.qZero.eq,
    Rat.qcls.eq)
qAddNegR = λu. quot-elim (p. clsEqOfRel (ratAdd p (ratNeg p)) ratZero (ratAddNegRel p)) u

qAddNegL : (u : Q) → qNeg u + u ≡ qZero using (qAddNegR)
qAddNegL = λu. trans _ _ _ (qAddComm (qNeg u) u) (qAddNegR u)

-- negation is involutive, and ½ − ⅓ = ⅙
qNegNeg : (u : Q) → qNeg (qNeg u) ≡ u
  using (intNegNeg,
    Int.Int.unfold,
    Int.intNeg.eq,
    ratEta,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.ratNeg.eq,
    Rat.Q.unfold,
    Rat.RatR.unfold,
    Rat.qNeg.eq)
qNegNeg =
  λu. quot-elim
    p. cong
      λx. Q
      λt. class t
      trans _ _ p (cong (λu2. Rat) (λx. mkRat x (den p)) (intNegNeg (num p))) ratEta
    u

qHalfMinusThird : qcls half + qNeg (qcls third) ≡ qcls (mkRat intOne (nzPos 5))
  using (Int.Int.eq,
    Int.intNeg.eq,
    Int.intOne.eq,
    Int.add.+.eq,
    Int.mul.*.eq,
    Natural.*.eq,
    Natural.+.eq,
    Rat.frac.Rat.eq,
    Rat.frac.den.eq,
    Rat.frac.half.eq,
    Rat.frac.intScale.eq,
    Rat.frac.intScaleN.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    Rat.frac.ratAdd.eq,
    Rat.frac.ratNeg.eq,
    Rat.frac.third.eq,
    Rat.Q.eq,
    Rat.RatR.eq,
    Rat.dInt.eq,
    Rat.+.eq,
    Rat.qNeg.eq,
    Rat.qcls.eq)
qHalfMinusThird = ⋆

-- ===== multiplication =====
ratMul : Rat → Rat → Rat using (Rat.frac.Rat.unfold)
ratMul = λp q. mkRat (num p * num q) (nzMul (den p) (den q))

-- like addition, multiplication is already commutative and
-- associative on Rat, and 1/1 is already a unit there
ratMulComm : (p q : Rat) → ratMul p q ≡ ratMul q p
  using (Int.Int.unfold,
    Int.mul.*.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.ratMul.eq)
ratMulComm =
  λp q. trans
    _
    mkRat (num q * num p) (nzMul (den p) (den q))
    _
    cong (λu. Rat) (λx. mkRat x (nzMul (den p) (den q))) (intMulComm (num p) (num q))
    cong
      λu. Rat
      λd. mkRat (num q * num p) d
      {nzMul (den p) (den q)}
      {nzMul (den q) (den p)}
      nzMulComm

ratMulAssoc : {p q r : Rat} → ratMul (ratMul p q) r ≡ ratMul p (ratMul q r)
  using (intMulAssoc,
    Int.Int.unfold,
    Int.mul.*.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.ratMul.eq)
ratMulAssoc =
  λp q r. trans
    _
    mkRat (num p * (num q * num r)) (nzMul (nzMul (den p) (den q)) (den r))
    _
    cong
      λu. Rat
      λx. mkRat x (nzMul (nzMul (den p) (den q)) (den r))
      intMulAssoc (num p) (num q) (num r)
    cong (λu. Rat) (λd. mkRat (num p * (num q * num r)) d) (nzMulAssoc (den p) (den q) (den r))

ratMulOneR : {p : Rat} → ratMul p ratOne ≡ p
  using (intMulOneR,
    Int.Int.unfold,
    Int.intOne.eq,
    Int.mul.*.eq,
    nzMulOneR,
    ratEta,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzNeg.eq,
    Rat.frac.nzOne.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.ratOfInt.eq,
    Rat.frac.ratOne.eq,
    Rat.ratMul.eq)
ratMulOneR =
  λp. trans
    _
    _
    _
    trans
      ratMul p ratOne
      _
      _
      cong (λu. Rat) (λx. mkRat x (nzMul (den p) nzOne)) (intMulOneR (num p))
      cong (λu. Rat) (λd. mkRat (num p) d) {nzMul (den p) nzOne} {den p} nzMulOneR
    ratEta

-- d₃·n₂ ≡ d₂·n₃, the relatedness hypothesis with both products
-- commuted; it comes up in every well-definedness proof
relFlip : (n2 d2 n3 d3 : Int) (h : n2 * d3 ≡ n3 * d2) → d3 * n2 ≡ d2 * n3
relFlip = λn2 d2 n3 d3 h. trans _ _ _ (intMulComm d3 n2) (trans _ _ _ h (intMulComm n3 d2))

-- inner well-definedness of ratMul — explicit trans (see qAddWDInner:
-- strict replay rejects chain steps under quot-elim scrutinees)
qMulWDInner : (p : Rat)
  {q q' : Rat}
  (h : RatR q q')
  → num (ratMul p q) * dInt (ratMul p q') ≡ num (ratMul p q') * dInt (ratMul p q)
  using (Int.Int.eq,
    Int.Int.unfold,
    Int.mul.*.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzNeg.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    Rat.RatR.eq,
    Rat.RatR.unfold,
    Rat.dInt.eq,
    Rat.ratMul.eq)
qMulWDInner =
  λp q q' h. trans
    _
    _
    _
    mulCongR (num p * num q) (dInt (ratMul p q')) (dInt p * dInt q') (nzToIntMul (den p) (den q'))
    trans
      _
      _
      _
      mulSwapOuter (num p) (num q) (dInt p) (dInt q')
      trans
        _
        _
        _
        mulCongL _ _ (dInt p * num p) (relFlip (num q) (dInt q) (num q') (dInt q') h)
        trans
          _
          _
          _
          sym _ _ (mulSwapOuter (num p) (num q') (dInt p) (dInt q))
          sym
            num (ratMul p q') * dInt (ratMul p q)
            num p * num q' * (dInt p * dInt q)
            mulCongR
              num p * num q'
              dInt (ratMul p q)
              dInt p * dInt q
              nzToIntMul (den p) (den q)

qMulWDInnerCls : {p q q' : Rat} (h : RatR q q') → class (ratMul p q) ≡ class (ratMul p q') ∈ Q
  using (Int.Int.eq,
    Int.Int.unfold,
    Int.mul.*.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.num.eq,
    Rat.Q.unfold,
    Rat.RatR.eq,
    Rat.RatR.unfold,
    Rat.dInt.eq,
    Rat.ratMul.eq)
qMulWDInnerCls = λp q q' h. clsEqOfRel _ _ (qMulWDInner p h)

qMulWDOuterCls : {p p' c : Rat} (h : RatR p p') → class (ratMul p c) ≡ class (ratMul p' c) ∈ Q
  using (Rat.Q.unfold)
qMulWDOuterCls =
  λp p' c h. trans
    _
    _
    _
    cong (λu. Q) (λr. class r) (ratMulComm p c)
    trans
      {Q}
      class (ratMul c p)
      class (ratMul c p')
      _
      qMulWDInnerCls h
      cong (λu. Q) (λr. class r) (sym _ _ (ratMulComm p' c))

qMulWDOuter : (p p' : Rat)
  (h : RatR p p')
  (v : Q)
  → quot-elim (w. Q) (x. class (ratMul p x)) v ≡ quot-elim (x. class (ratMul p' x)) v
  using (Int.Int.unfold,
    qMulWDInnerCls,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.Q.unfold,
    Rat.RatR.unfold)
qMulWDOuter =
  λp p' h v. quot-elim
    w. quot-elim (z. Q) (x. class (ratMul p x)) w ≡ quot-elim (x. class (ratMul p' x)) w
    c. qMulWDOuterCls h
    v

infixl 7 *
* : Q → Q → Q
  using (Int.Int.unfold,
    qMulWDInnerCls,
    qMulWDOuter,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.Q.unfold,
    Rat.RatR.unfold)
(*) = λu v. quot-elim (p. quot-elim (q. class (ratMul p q)) v) u

qMulCls : (p q : Rat) → qcls p * qcls q ≡ qcls (ratMul p q)
  using (Int.Int.unfold,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.Q.unfold,
    Rat.*.eq,
    Rat.qcls.eq,
    Rat.ratMul.eq)
qMulCls = λp q. ⋆

qMulComm : (u v : Q) → u * v ≡ v * u
  using (Int.Int.unfold,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.Q.unfold,
    Rat.RatR.unfold,
    Rat.*.eq,
    Rat.ratMul.eq)
qMulComm = λu v. quot-elim (p. quot-elim (q. cong (λx. Q) (λt. class t) (ratMulComm p q)) v) u

qMulAssoc : (u v w : Q) → u * v * w ≡ u * (v * w)
  using (intMulAssoc,
    Int.Int.unfold,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.Q.unfold,
    Rat.RatR.unfold,
    Rat.*.eq,
    Rat.ratMul.eq)
qMulAssoc =
  λu v w. quot-elim
    p. quot-elim
      q. quot-elim
        r. cong (λx. Q) (λt. class t) {ratMul (ratMul p q) r} {ratMul p (ratMul q r)} ratMulAssoc
        w
      v
    u

qMulOneR : (u : Q) → u * qOne ≡ u
  using (intMulOneR,
    Int.Int.unfold,
    Int.intOne.eq,
    Int.mul.*.eq,
    nzMulOneR,
    ratEta,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.ratOfInt.eq,
    Rat.frac.ratOne.eq,
    Rat.Q.unfold,
    Rat.RatR.unfold,
    Rat.*.eq,
    Rat.qOne.eq,
    Rat.qcls.eq,
    Rat.ratMul.eq)
qMulOneR = λu. quot-elim (p. cong (λx. Q) (λt. class t) {ratMul p ratOne} {p} ratMulOneR) u

qMulOneL : (u : Q) → qOne * u ≡ u using (qMulOneR)
qMulOneL = λu. trans _ _ _ (qMulComm qOne u) (qMulOneR u)

-- ⅓ · ½ = ⅙
qMulTest : qcls third * qcls half ≡ qcls (mkRat intOne (nzPos 5))
  using (Int.intOne.eq,
    Int.mul.*.eq,
    Natural.*.eq,
    Natural.+.eq,
    Rat.frac.den.eq,
    Rat.frac.half.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.third.eq,
    Rat.Q.unfold,
    Rat.*.eq,
    Rat.qcls.eq,
    Rat.ratMul.eq)
qMulTest = ⋆

-- ===== distributivity =====
--
-- The first law that needs the quotient for its DENOMINATOR: p·(q+r)
-- has denominator d₁d₂d₃ while p·q + p·r has d₁²d₂d₃. Both numerator
-- and denominator of the right-hand side are the left-hand side's,
-- scaled by d₁ — so the cross-multiplication relation collapses to
-- moving that one factor across.
-- (a·b)·(c·d) ≡ a·(c·(b·d))
mulHoist : (a b c d : Int) → a * b * (c * d) ≡ a * (c * (b * d))
mulHoist = λa b c d. trans _ _ _ (intMulAssoc a b (c * d)) (mulCongR a _ _ (mulSwapHead b c d))

-- x·(a·y) ≡ (a·x)·y
mulShiftL : {x a y : Int} → x * (a * y) ≡ a * x * y using (intMulAssoc)
mulShiftL = λx a y. trans _ _ _ (sym _ _ (intMulAssoc x a y)) (mulCongL _ _ y (intMulComm x a))

-- dInt of the product-of-sums denominator, expanded
dIntMul3 : (p q r : Rat) → dInt (ratMul p (ratAdd q r)) ≡ dInt p * (dInt q * dInt r)
  using (Int.Int.unfold,
    Int.add.+.eq,
    Int.mul.*.eq,
    nzToIntMul,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.intScale.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzNeg.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    Rat.frac.ratAdd.eq,
    Rat.dInt.eq,
    Rat.ratMul.eq)
dIntMul3 =
  λp q r. trans
    _
    _
    _
    nzToIntMul (den p) (nzMul (den q) (den r))
    mulCongR (dInt p) (dInt (ratAdd q r)) (dInt q * dInt r) (nzToIntMul (den q) (den r))

distribDen : (p q r : Rat)
  → dInt (ratAdd (ratMul p q) (ratMul p r)) ≡ dInt p * dInt (ratMul p (ratAdd q r))
  using (Int.Int.unfold,
    Int.add.+.eq,
    Int.mul.*.eq,
    nzToIntMul,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.intScale.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzNeg.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    Rat.frac.ratAdd.eq,
    Rat.dInt.eq,
    Rat.ratMul.eq)
distribDen =
  λp q r. trans
    _
    _
    _
    trans
      dInt (ratAdd (ratMul p q) (ratMul p r))
      dInt (ratMul p q) * dInt (ratMul p r)
      dInt p * dInt q * (dInt p * dInt r)
      nzToIntMul (nzMul (den p) (den q)) (nzMul (den p) (den r))
      intMulCong2 _ _ _ _ (nzToIntMul (den p) (den q)) (nzToIntMul (den p) (den r))
    trans
      _
      _
      _
      mulHoist (dInt p) (dInt q) (dInt p) (dInt r)
      mulCongR (dInt p) _ _ (sym _ _ (dIntMul3 p q r))

-- six joins, midpoints once, congruences spelled, explicit trans
-- (see qAddWDInner: strict replay rejects chain steps under quot-elim
-- scrutinees); sym supplies the orientations the chain engine used
-- to pick silently
distribNum : (p q r : Rat)
  → num (ratAdd (ratMul p q) (ratMul p r)) ≡ dInt p * num (ratMul p (ratAdd q r))
  using (Int.Int.unfold,
    Int.mul.*.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzNeg.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    Rat.dInt.eq,
    Rat.ratMul.eq)
distribNum =
  λp q r. trans
    _
    _
    _
    ratAddNumMul (ratMul p q) (ratMul p r)
    trans
      _
      _
      _
      intAddCong2
        dInt (ratMul p r) * num (ratMul p q)
        dInt (ratMul p q) * num (ratMul p r)
        dInt p * dInt r * (num p * num q)
        dInt p * dInt q * (num p * num r)
        mulCongL (dInt (ratMul p r)) (dInt p * dInt r) (num p * num q) (nzToIntMul (den p) (den r))
        mulCongL (dInt (ratMul p q)) (dInt p * dInt q) (num p * num r) (nzToIntMul (den p) (den q))
      trans
        _
        _
        _
        intAddCong2
          _
          _
          _
          _
          mulHoist (dInt p) (dInt r) (num p) (num q)
          mulHoist (dInt p) (dInt q) (num p) (num r)
        trans
          _
          _
          _
          sym _ _ (intMulDistribL (dInt p) (num p * (dInt r * num q)) (num p * (dInt q * num r)))
          trans
            _
            _
            _
            sym
              _
              _
              mulCongR (dInt p) _ _ (intMulDistribL (num p) (dInt r * num q) (dInt q * num r))
            sym
              dInt p * num (ratMul p (ratAdd q r))
              dInt p * (num p * (dInt r * num q + dInt q * num r))
              mulCongR (dInt p) _ _ (mulCongR (num p) _ _ (ratAddNumMul q r))

qDistribRel : (p q r : Rat)
  → num (ratMul p (ratAdd q r)) * dInt (ratAdd (ratMul p q) (ratMul p r))
    ≡ num (ratAdd (ratMul p q) (ratMul p r)) * dInt (ratMul p (ratAdd q r))
  using (distribNum)
qDistribRel =
  λp q r. trans
    _
    _
    _
    mulCongR (num (ratMul p (ratAdd q r))) _ _ (distribDen p q r)
    trans
      num (ratMul p (ratAdd q r)) * (dInt p * dInt (ratMul p (ratAdd q r)))
      _
      _
      mulShiftL
      mulCongL _ _ (dInt (ratMul p (ratAdd q r))) (sym _ _ (distribNum p q r))

qDistribL : (u v w : Q) → u * (v + w) ≡ u * v + u * w
  using (distribNum,
    Int.Int.eq,
    Int.Int.unfold,
    Int.mul.*.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.num.eq,
    Rat.frac.ratAdd.eq,
    Rat.Q.unfold,
    Rat.RatR.eq,
    Rat.RatR.unfold,
    Rat.dInt.eq,
    Rat.+.eq,
    Rat.*.eq,
    Rat.ratMul.eq)
qDistribL =
  λu v w. quot-elim
    p. quot-elim
      q. quot-elim
        r. clsEqOfRel (ratMul p (ratAdd q r)) (ratAdd (ratMul p q) (ratMul p r)) (qDistribRel p q r)
        w
      v
    u

qDistribR : (u v w : Q) → (v + w) * u ≡ v * u + w * u
qDistribR =
  λu v w. trans
    _
    _
    _
    qMulComm (v + w) u
    trans
      _
      _
      _
      qDistribL u v w
      trans
        _
        _
        _
        cong (λx. Q) (λx. x + u * w) (qMulComm u v)
        cong (λx. Q) (λx. v * u + x) (qMulComm u w)

-- ===== zero and reciprocals =====
-- 0 · u = 0. On Rat this is 0/d, which only the quotient identifies
-- with 0/1
ratMulZeroRel : (p : Rat)
  → num (ratMul ratZero p) * dInt ratZero ≡ num ratZero * dInt (ratMul ratZero p)
  using (intMulZeroL,
    Int.Int.unfold,
    Int.intZero.eq,
    Int.mul.*.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzToInt.eq,
    Rat.frac.ratOfInt.eq,
    Rat.frac.ratZero.eq,
    Rat.dInt.eq,
    Rat.ratMul.eq)
ratMulZeroRel =
  λp. trans
    _
    _
    _
    trans
      _
      _
      _
      mulCongL (num (ratMul ratZero p)) intZero (dInt ratZero) (intMulZeroL (num p))
      intMulZeroL (dInt ratZero)
    sym _ _ (intMulZeroL (dInt (ratMul ratZero p)))

qMulZeroL : {u : Q} → qZero * u ≡ qZero
  using (intMulZeroL,
    Int.Int.eq,
    Int.Int.unfold,
    Int.intZero.eq,
    Int.mul.*.eq,
    nzMulOneL,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.ratOfInt.eq,
    Rat.frac.ratZero.eq,
    Rat.Q.unfold,
    Rat.RatR.eq,
    Rat.RatR.unfold,
    Rat.dInt.eq,
    Rat.*.eq,
    Rat.qZero.eq,
    Rat.qcls.eq,
    Rat.ratMul.eq)
qMulZeroL = λu. quot-elim (p. clsEqOfRel (ratMul ratZero p) ratZero (ratMulZeroRel p)) u

qMulZeroR : (u : Q) → u * qZero ≡ qZero using (qMulZeroL)
qMulZeroR = λu. trans _ _ _ (qMulComm u qZero) qMulZeroL

-- Reciprocals. A rational has an inverse exactly when its NUMERATOR is
-- non-zero, and — as with denominators — that cannot be carried as a
-- proof: has no 𝕌-code, realizers are irrelevant, so no function
-- could dispatch on such a proof to build the inverse. So the non-zero
-- rationals get their own code, with BOTH components drawn from NZ;
-- inversion is then total, and is just the swap.
NZQ : 𝕌
NZQ = NZ × NZ

nzqToRat : NZQ → Rat using (Rat.frac.Rat.unfold, Rat.NZQ.unfold)
nzqToRat = λx. mkRat (nzToInt (x .π₁)) (x .π₂)

qOfNzq : NZQ → Q using (Rat.Q.unfold)
qOfNzq = λx. qcls (nzqToRat x)

nzqInv : NZQ → NZQ using (Rat.NZQ.unfold)
nzqInv = λx. x .π₂, x .π₁

nzqInvInv : (x : NZQ) → nzqInv (nzqInv x) ≡ x
  using (Rat.frac.NZ.unfold, Rat.NZQ.unfold, Rat.nzqInv.eq)
nzqInvInv = λx. paireta x

-- x · x⁻¹ = 1: the product is (N·D)/(d·n), and cross-multiplying
-- against 1/1 leaves exactly N·D ≡ D·N
nzqInvRel : (x : NZQ)
  → num (ratMul (nzqToRat x) (nzqToRat (nzqInv x))) * dInt ratOne
    ≡ num ratOne * dInt (ratMul (nzqToRat x) (nzqToRat (nzqInv x)))
  using (Int.intOne.eq,
    Int.mul.*.eq,
    nzToIntMul,
    Rat.frac.NZ.unfold,
    Rat.frac.den.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzNeg.eq,
    Rat.frac.nzOne.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    Rat.frac.ratOfInt.eq,
    Rat.frac.ratOne.eq,
    Rat.NZQ.unfold,
    Rat.dInt.eq,
    Rat.nzqInv.eq,
    Rat.nzqToRat.eq,
    Rat.ratMul.eq)
nzqInvRel =
  λx. trans
    _
    _
    _
    intMulOneR (nzToInt (x .π₁) * nzToInt (x .π₂))
    trans
      _
      _
      _
      intMulComm (nzToInt (x .π₁)) (nzToInt (x .π₂))
      trans
        nzToInt (x .π₂) * nzToInt (x .π₁)
        dInt (ratMul (nzqToRat x) (nzqToRat (nzqInv x)))
        num ratOne * dInt (ratMul (nzqToRat x) (nzqToRat (nzqInv x)))
        sym _ _ (nzToIntMul (x .π₂) (x .π₁))
        sym _ _ (intMulOneL (dInt (ratMul (nzqToRat x) (nzqToRat (nzqInv x)))))

qMulInv : {x : NZQ} → qOfNzq x * qOfNzq (nzqInv x) ≡ qOne
  using (Int.Int.eq,
    Int.intOne.eq,
    Int.mul.*.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.den.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzToInt.eq,
    Rat.frac.ratOfInt.eq,
    Rat.frac.ratOne.eq,
    Rat.NZQ.unfold,
    Rat.RatR.eq,
    Rat.dInt.eq,
    Rat.nzqInv.eq,
    Rat.nzqToRat.eq,
    Rat.*.eq,
    Rat.qOfNzq.eq,
    Rat.qOne.eq,
    Rat.qcls.eq,
    Rat.ratMul.eq)
qMulInv = λx. clsEqOfRel (ratMul (nzqToRat x) (nzqToRat (nzqInv x))) ratOne (nzqInvRel x)

qMulInvL : (x : NZQ) → qOfNzq (nzqInv x) * qOfNzq x ≡ qOne
qMulInvL = λx. trans _ _ _ (qMulComm (qOfNzq (nzqInv x)) (qOfNzq x)) qMulInv

-- ⅓ as a non-zero rational, and 3 = (⅓)⁻¹
nzqThird : NZQ using (Rat.NZQ.unfold)
nzqThird = nzPos Z, nzPos 2

nzqThirdIsThird : qOfNzq nzqThird ≡ qcls third
  using (Int.intOne.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    Rat.frac.third.eq,
    Rat.Q.unfold,
    Rat.nzqThird.eq,
    Rat.nzqToRat.eq,
    Rat.qOfNzq.eq,
    Rat.qcls.eq)
nzqThirdIsThird = ⋆

nzqInvThird : qOfNzq (nzqInv nzqThird) ≡ qcls (mkRat (class (3, Z)) nzOne)
  using (Int.Int.unfold,
    Rat.frac.mkRat.eq,
    Rat.frac.nzOne.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    Rat.Q.unfold,
    Rat.nzqInv.eq,
    Rat.nzqThird.eq,
    Rat.nzqToRat.eq,
    Rat.qOfNzq.eq,
    Rat.qcls.eq)
nzqInvThird = ⋆

qMulInvThird : qOfNzq nzqThird * qOfNzq (nzqInv nzqThird) ≡ qOne
  using (clsEqOfRel, Rat.Q.unfold, Rat.qMulInv)
qMulInvThird = ⋆