Rat.order

-- Order on ℚ via the SIGN: a three-valued small code, computed for an
-- integer by intNonZero's decision (an honest function — no new
-- well-definedness), for a raw fraction as the sign of num·den, and
-- for a class by quot-elim whose well-definedness is the one real
-- theorem here: multiplying by a nonzero SQUARE preserves sign.

import Natural (+, *, plusComm, plusAssoc, swapLeft, zeroPlusId, plusZeroId)
import Int (Int, intZero, intNeg, intNegZero)
import Int.add (+)
import Int.mul (*, intMulComm, intMulAssoc, intMulZeroL, intMulZeroR)
import Rat.frac (NZ, nzPos, nzNeg, nzToInt, nzMul, Rat, mkRat, num, den, denInt, ratNeg, ratZero, ratAdd, intScale)
import Rat (Q, RatR, qcls, +, qNeg, qZero, qAddComm, qAddAssoc, qAddZeroL, qAddZeroR, qAddNegL, qAddNegR, qNegNeg, nzToIntMul, *, qMulComm, qMulZeroL, qDistribR, ratMul, intScaleIsMul)
import Int.nonZero (nzOfInt, nzToIntNonZero, intNoZeroDiv)
import Int.order (intMulDistribR)
import Core.equality (trans, sym, cong, transport)
import Rat.inv (ratZeroOfNumZero)
import Core.id (Id, idToEq, eqToId)

Sign : 𝕌
Sign = 𝟙 ⊎ 𝟙 ⊎ 𝟙

sZero : Sign using (Rat.order.Sign.unfold)
sZero = inj₁ ()

sPos : Sign using (Rat.order.Sign.unfold)
sPos = inj₂ (inj₁ ())

sNeg : Sign using (Rat.order.Sign.unfold)
sNeg = inj₂ (inj₂ ())

sgnFlip : Sign → Sign using (Rat.order.Sign.unfold)
sgnFlip = λs. ⊎-elim (u. sZero) (v. ⊎-elim (u. sNeg) (u. sPos) v) s

nzSgn : NZ → Sign using (Rat.frac.NZ.unfold, Rat.order.Sign.unfold)
nzSgn = λe. ⊎-elim (n. sPos) (n. sNeg) e

intSgn : Int → Sign using (Rat.order.Sign.unfold)
intSgn = λz. ⊎-elim (u. nzSgn (u .π₁)) (u. sZero) (nzOfInt z)

-- computation: intSgn evaluates on the three shapes, magnitude open
intSgnZero : intSgn intZero ≡ sZero
  using (Int.eq.classNormPairEq.eq,
    Int.eq.intCanon.eq,
    Int.eq.intCanonClass.eq,
    Core.equality.sym.eq,
    Core.equality.trans.eq,
    Int.nonZero.nzOfInt.eq,
    Int.nonZero.nzOfIntAt.eq,
    Int.nonZero.nzOfPairD.eq,
    Int.Int.eq,
    Int.intZero.eq,
    Int.mul.classPairEta.eq,
    Int.normalize.normPair.eq,
    Rat.frac.nzToInt.eq,
    Rat.inv.intCanonProdZero.eq,
    Rat.inv.normProdZero.eq,
    Rat.order.Sign.unfold,
    Rat.order.intSgn.eq,
    Rat.order.nzSgn.eq,
    Rat.order.sNeg.eq,
    Rat.order.sPos.eq,
    Rat.order.sZero.eq)
intSgnZero = ⋆

intSgnPos : (k : ℕ) → intSgn (nzToInt (nzPos k)) ≡ sPos
  using (Int.eq.classNormPairEq.eq,
    Int.eq.intCanon.eq,
    Int.eq.intCanonClass.eq,
    Core.equality.sym.eq,
    Core.equality.trans.eq,
    Int.nonZero.nzOfInt.eq,
    Int.nonZero.nzOfIntAt.eq,
    Int.nonZero.nzOfPairD.eq,
    Int.Int.eq,
    Int.intZero.eq,
    Int.mul.classPairEta.eq,
    Int.normalize.normPair.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    Rat.inv.intCanonProdZero.eq,
    Rat.inv.normProdZero.eq,
    Rat.order.Sign.unfold,
    Rat.order.intSgn.eq,
    Rat.order.nzSgn.eq,
    Rat.order.sNeg.eq,
    Rat.order.sPos.eq,
    Rat.order.sZero.eq)
intSgnPos = λk. ⋆

intSgnNeg : {k : ℕ} → intSgn (nzToInt (nzNeg k)) ≡ sNeg
  using (Int.eq.classNormPairEq.eq,
    Int.eq.intCanon.eq,
    Int.eq.intCanonClass.eq,
    Core.equality.sym.eq,
    Core.equality.trans.eq,
    Int.nonZero.nzOfInt.eq,
    Int.nonZero.nzOfIntAt.eq,
    Int.nonZero.nzOfPairD.eq,
    Int.Int.eq,
    Int.intZero.eq,
    Int.mul.classPairEta.eq,
    Int.normalize.normPair.eq,
    Rat.frac.nzNeg.eq,
    Rat.frac.nzToInt.eq,
    Rat.inv.intCanonProdZero.eq,
    Rat.inv.normProdZero.eq,
    Rat.order.Sign.unfold,
    Rat.order.intSgn.eq,
    Rat.order.nzSgn.eq,
    Rat.order.sNeg.eq,
    Rat.order.sPos.eq,
    Rat.order.sZero.eq)
intSgnNeg = λk. ⋆

intSgnNz : (e : NZ) → intSgn (nzToInt e) ≡ nzSgn e
  using (Rat.frac.NZ.unfold,
    Rat.frac.nzNeg.eq,
    Rat.frac.nzPos.eq,
    Rat.order.nzSgn.eq,
    Rat.order.sNeg.eq,
    Rat.order.sPos.eq)
intSgnNz = λe. ⊎-elim (n. intSgnPos n) (n. intSgnNeg) e

-- ===== sign multiplicativity: the well-definedness core =====
-- squares in NZ are positive, so scaling by one preserves the sign —
-- all four constructor cases compute (nzMul's sign table is its body)
nzSgnMulSq : {a b : NZ} → nzSgn (nzMul a (nzMul b b)) ≡ nzSgn a
  using (Rat.frac.NZ.unfold,
    Rat.frac.nzMul.eq,
    Rat.frac.nzNeg.eq,
    Rat.frac.nzPos.eq,
    Rat.order.Sign.unfold,
    Rat.order.nzSgn.eq,
    Rat.order.sNeg.eq,
    Rat.order.sPos.eq)
nzSgnMulSq =
  λa b. ⊎-elim
    m. ⊎-elim (v. nzSgn (nzMul (nzPos m) (nzMul v v)) ≡ nzSgn (nzPos m)) (k. ⋆) (k. ⋆) b
    m. ⊎-elim (v. nzSgn (nzMul (nzNeg m) (nzMul v v)) ≡ nzSgn (nzNeg m)) (k. ⋆) (k. ⋆) b
    a

-- multiplying an integer by a nonzero square preserves its sign:
-- decide z, then either both sides are sZero or everything lands in
-- NZ where nzSgnMulSq computes
intSgnMulSq : (z : Int) (e : NZ) → intSgn (z * (nzToInt e * nzToInt e)) ≡ intSgn z
intSgnMulSq =
  λz e. ⊎-elim
    u. trans
      _
      _
      _
      cong (λv. Sign) (λv. intSgn (v * (nzToInt e * nzToInt e))) (sym _ _ (u .π₂))
      trans
        _
        _
        _
        trans
          _
          _
          _
          cong (λv. Sign) (λv. intSgn (nzToInt (u .π₁) * v)) (sym _ _ (nzToIntMul e e))
          cong (λv. Sign) (λv. intSgn v) (sym _ _ (nzToIntMul (u .π₁) (nzMul e e)))
        trans
          _
          _
          _
          trans _ _ (nzSgn (u .π₁)) (intSgnNz (nzMul (u .π₁) (nzMul e e))) nzSgnMulSq
          trans _ _ _ (sym _ _ (intSgnNz (u .π₁))) (cong (λv. Sign) (λv. intSgn v) (u .π₂))
    hz. trans
      _
      _
      _
      trans
        _
        _
        _
        cong (λv. Sign) (λv. intSgn (v * (nzToInt e * nzToInt e))) hz
        trans
          _
          _
          _
          cong (λv. Sign) (λv. intSgn v) (intMulZeroL (nzToInt e * nzToInt e))
          intSgnZero
      sym _ _ (trans _ _ _ (cong (λv. Sign) (λv. intSgn v) hz) intSgnZero)
    nzOfInt z

-- ===== interchange, hypothesis-free =====
mulLeftSwap : (b c d : Int) → b * (c * d) ≡ c * (b * d) using (Int.Int.unfold)
mulLeftSwap =
  λb c d. b * (c * d)
    ≡⟨ sym _ _ (intMulAssoc b c d) ⟩ b * c * d
    ≡⟨ cong (λv. Int) (λv. v * d) (intMulComm b c) ⟩ c * b * d
    ≡⟨ intMulAssoc c b d ⟩ c * (b * d)

mulPairSwap : (a b c d : Int) → a * b * (c * d) ≡ a * c * (b * d) using (Int.Int.unfold)
mulPairSwap =
  λa b c d. a * b * (c * d)
    ≡⟨ intMulAssoc a b (c * d) ⟩ a * (b * (c * d))
    ≡⟨ cong (λv. Int) (λv. a * v) (mulLeftSwap b c d) ⟩ a * (c * (b * d))
    ≡⟨ sym _ _ (intMulAssoc a c (b * d)) ⟩ a * c * (b * d)

mulPairSwapR : (a b c d : Int) → a * b * (c * d) ≡ a * d * (c * b) using (Int.Int.unfold)
mulPairSwapR =
  λa b c d. a * b * (c * d)
    ≡⟨ cong (λv. Int) (λv. a * b * v) (intMulComm c d) ⟩ a * b * (d * c)
    ≡⟨ mulPairSwap a b d c ⟩ a * d * (b * c)
    ≡⟨ cong (λv. Int) (λv. a * d * v) (intMulComm b c) ⟩ a * d * (c * b)

-- ===== the sign of a fraction, and its well-definedness =====
ratSgn : Rat → Sign using (Rat.order.Sign.unfold)
ratSgn = λp. intSgn (num p * denInt p)

-- RatR p q cross-multiplies; scale each side's num·den by the OTHER
-- side's den², interchange, and rewrite across the relation — signs
-- survive because squares do (intSgnMulSq)
ratSgnWD : (p q : Rat) → RatR p q → ratSgn p ≡ ratSgn 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.denInt.eq,
    Rat.frac.num.eq,
    Rat.frac.nzToInt.eq,
    Rat.order.intSgn.eq,
    Rat.order.ratSgn.eq,
    Rat.RatR.eq,
    Rat.RatR.unfold,
    Rat.dInt.eq)
ratSgnWD =
  λp q h. trans
    intSgn (num p * denInt p)
    _
    intSgn (num q * denInt q)
    sym
      intSgn (num p * denInt p * (denInt q * denInt q))
      intSgn (num p * denInt p)
      intSgnMulSq (num p * denInt p) (den q)
    trans
      _
      _
      _
      cong (λv. Sign) (λv. intSgn v) (mulPairSwap (num p) (denInt p) (denInt q) (denInt q))
      trans
        _
        _
        _
        cong
          λv. Sign
          λv. intSgn (v * (denInt p * denInt q))
          {num p * denInt q}
          {num q * denInt p}
          h
        trans
          _
          _
          intSgn (num q * denInt q)
          cong (λv. Sign) (λv. intSgn v) (mulPairSwapR (num q) (denInt p) (denInt p) (denInt q))
          intSgnMulSq (num q * denInt q) (den p)

-- the sign of a rational: quot-elim, well-defined by ratSgnWD
sgnQ : Q → Sign
  using (Int.Int.unfold,
    ratSgnWD,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.order.Sign.unfold,
    Rat.Q.unfold,
    Rat.RatR.unfold)
sgnQ = λu. quot-elim (p. ratSgn p) u

sgnQCls : (p : Rat) → sgnQ (qcls p) ≡ ratSgn p
  using (Int.Int.unfold,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.order.Sign.unfold,
    Rat.order.ratSgn.eq,
    Rat.order.sgnQ.eq,
    Rat.qcls.eq)
sgnQCls = λp. ⋆

sgnQZero : sgnQ qZero ≡ sZero
  using (intMulZeroL.rw,
    intSgnZero.rw,
    Rat.frac.denInt.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.ratOfInt.eq,
    Rat.frac.ratZero.eq,
    Rat.order.Sign.unfold,
    Rat.order.ratSgn.eq,
    Rat.qZero.eq,
    sgnQCls.rw)
sgnQZero = ⋆

-- ===== negation and the sign flip =====
-- (−z)·w ≡ −(z·w): both sides compute on classes to plusComm-related
-- pairs
intMulNegL : {z w : Int} → intNeg z * w ≡ intNeg (z * w)
  using (Int.effective.intRRefl,
    Int.Int.unfold,
    Int.mul.distribBackR,
    Int.mul.intMulNegL,
    Int.mul.sum4Distrib,
    plusAssoc,
    Rat.frac.plusSwapRight)
intMulNegL = λz w. quot-elim (u. quot-elim (v. ⋆) w) z

-- negating flips the decided sign, shape by shape
intSgnNegNz : {e : NZ} → intSgn (intNeg (nzToInt e)) ≡ sgnFlip (nzSgn e)
  using (Int.eq.classNormPairEq.eq,
    Int.eq.intCanon.eq,
    Int.eq.intCanonClass.eq,
    Core.equality.sym.eq,
    Core.equality.trans.eq,
    Int.nonZero.nzOfInt.eq,
    Int.nonZero.nzOfIntAt.eq,
    Int.nonZero.nzOfPairD.eq,
    Int.Int.eq,
    Int.intNeg.eq,
    Int.intZero.eq,
    Int.mul.classPairEta.eq,
    Int.normalize.normPair.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.nzNeg.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    Rat.inv.intCanonProdZero.eq,
    Rat.inv.normProdZero.eq,
    Rat.order.Sign.unfold,
    Rat.order.intSgn.eq,
    Rat.order.nzSgn.eq,
    Rat.order.sNeg.eq,
    Rat.order.sPos.eq,
    Rat.order.sZero.eq,
    Rat.order.sgnFlip.eq)
intSgnNegNz = λe. ⊎-elim (n. ⋆) (n. ⋆) e

intSgnNegFlip : (z : Int) → intSgn (intNeg z) ≡ sgnFlip (intSgn z)
  using (Int.Int.unfold, Rat.order.Sign.unfold, Rat.order.sZero.eq, Rat.order.sgnFlip.eq)
intSgnNegFlip =
  λz. ⊎-elim
    u. trans
      _
      _
      _
      cong (λv. Sign) (λv. intSgn (intNeg v)) (sym _ _ (u .π₂))
      trans
        intSgn (intNeg (nzToInt (u .π₁)))
        _
        _
        intSgnNegNz
        trans
          _
          _
          _
          cong (λv. Sign) (λv. sgnFlip v) (sym _ _ (intSgnNz (u .π₁)))
          cong (λv. Sign) (λv. sgnFlip (intSgn v)) (u .π₂)
    hz. trans
      _
      _
      _
      trans
        _
        _
        _
        cong (λv. Sign) (λv. intSgn (intNeg v)) hz
        trans _ _ _ (cong (λv. Sign) (λv. intSgn v) intNegZero) intSgnZero
      sym
        _
        _
        trans
          _
          _
          sZero
          cong
            λv. Sign
            λv. sgnFlip v
            trans _ _ _ (cong (λv. Sign) (λv. intSgn v) hz) intSgnZero
          ⋆
    nzOfInt z

-- ===== ℚ additive-group algebra, hypothesis-free =====
qLeftSwap : (b c d : Q) → b + (c + d) ≡ c + (b + d) using (Rat.Q.unfold)
qLeftSwap =
  λb c d. b + (c + d)
    ≡⟨ sym _ _ (qAddAssoc b c d) ⟩ b + c + d
    ≡⟨ cong (λv. Q) (λv. v + d) (qAddComm b c) ⟩ c + b + d
    ≡⟨ qAddAssoc c b d ⟩ c + (b + d)

qPairSwap : (a b c d : Q) → a + b + (c + d) ≡ a + c + (b + d) using (Rat.Q.unfold)
qPairSwap =
  λa b c d. a + b + (c + d)
    ≡⟨ qAddAssoc a b (c + d) ⟩ a + (b + (c + d))
    ≡⟨ cong (λv. Q) (λv. a + v) (qLeftSwap b c d) ⟩ a + (c + (b + d))
    ≡⟨ sym _ _ (qAddAssoc a c (b + d)) ⟩ a + c + (b + d)

-- −u + (u + v) ≡ v, then inverse uniqueness, then −(a+b) ≡ (−a)+(−b)
qNegPlusCancel : (u v : Q) → qNeg u + (u + v) ≡ v using (Rat.Q.unfold)
qNegPlusCancel =
  λu v. qNeg u + (u + v)
    ≡⟨ sym _ _ (qAddAssoc (qNeg u) u v) ⟩ qNeg u + u + v
    ≡⟨ cong (λw. Q) (λw. w + v) (qAddComm (qNeg u) u) ⟩ u + qNeg u + v
    ≡⟨ cong (λw. Q) (λw. w + v) (qAddNegR u) ⟩ qZero + v
    ≡⟨ qAddZeroL v ⟩ v

qNegUnique : {u v : Q} → (u + v ≡ qZero) → v ≡ qNeg u
qNegUnique =
  λu v h. trans
    _
    _
    _
    sym _ _ (qNegPlusCancel u v)
    trans
      _
      _
      _
      cong (λw. Q) (λw. qNeg u + w) h
      trans _ _ _ (qAddComm (qNeg u) qZero) (qAddZeroL (qNeg u))

qNegAdd : (a b : Q) → qNeg (a + b) ≡ qNeg a + qNeg b
qNegAdd =
  λa b. sym
    _
    _
    qNegUnique
      trans
        _
        _
        _
        qPairSwap a b (qNeg a) (qNeg b)
        trans
          _
          _
          _
          cong (λw. Q) (λw. w + (b + qNeg b)) (qAddNegR a)
          trans _ _ _ (qAddZeroL (b + qNeg b)) (qAddNegR b)

qSubNeg : {x y : Q} → x + qNeg y ≡ qNeg (y + qNeg x)
qSubNeg =
  λx y. sym
    _
    _
    trans
      _
      _
      _
      qNegAdd y (qNeg x)
      trans _ _ _ (cong (λw. Q) (λw. qNeg y + w) (qNegNeg x)) (qAddComm (qNeg y) x)

-- the flip, lifted to ℚ (representative abstract: D-3)
sgnQNegFlip : {u : Q} → sgnQ (qNeg u) ≡ sgnFlip (sgnQ u)
  using (Int.eq.intCanon.eq,
    Int.eq.intCanonClass.eq,
    Int.nonZero.nzOfInt.eq,
    Int.nonZero.nzOfIntAt.eq,
    Int.Int.unfold,
    Int.intNeg.eq,
    Int.mul.*.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.denInt.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzToInt.eq,
    Rat.frac.ratNeg.eq,
    Rat.inv.intCanonProdZero.eq,
    Rat.order.Sign.unfold,
    Rat.order.intSgn.eq,
    Rat.order.nzSgn.eq,
    Rat.order.ratSgn.eq,
    Rat.order.sNeg.eq,
    Rat.order.sPos.eq,
    Rat.order.sZero.eq,
    Rat.order.sgnQ.eq,
    Rat.Q.unfold,
    Rat.RatR.unfold,
    Rat.qNeg.eq)
sgnQNegFlip =
  λu. quot-elim
    p. trans
      _
      _
      _
      trans
        sgnQ (qNeg (class p))
        _
        _
        ⋆
        cong
          λv. Sign
          λv. intSgn v
          {intNeg (num p) * denInt p}
          {intNeg (num p * denInt p)}
          intMulNegL
      intSgnNegFlip (num p * denInt p)
    u

-- ===== the order =====
NonNegS : Sign → 𝕌
NonNegS = λs. Id _ s sZero ⊎ Id _ s sPos

infixl 4 ≤
≤ : Q → Q → 𝕌
(≤) = λx y. NonNegS (sgnQ (y + qNeg x))

leQRefl : (x : Q) → x ≤ x using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold)
leQRefl = λx. inj₁ (eqToId _ _ (trans _ _ _ (cong (λu. Sign) (λu. sgnQ u) (qAddNegR x)) sgnQZero))

leQOfEq : (x y : Q) → (x ≡ y) → x ≤ y using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold)
leQOfEq =
  λx y h. inj₁
    eqToId
      _
      _
      trans
        _
        _
        _
        cong (λu. Sign) (λu. sgnQ u) (trans _ _ _ (cong (λu. Q) (λu. y + qNeg u) h) (qAddNegR y))
        sgnQZero

-- every sign is nonneg or negative — the DECISION, as data
sgnCases : (s : Sign) → NonNegS s ⊎ Id _ s sNeg
  using (Sign.eq, Rat.order.NonNegS.unfold, Rat.order.Sign.unfold, sNeg.eq, sPos.eq, sZero.eq)
sgnCases =
  λs. ⊎-elim
    u. inj₁ (inj₁ (eqToId _ _ ⋆))
    v. ⊎-elim (u. inj₁ (inj₂ (eqToId _ _ ⋆))) (u. inj₂ (eqToId _ _ ⋆)) v
    s

-- totality: decide the difference's sign; a negative difference flips
leQTotal : (x y : Q) → x ≤ y ⊎ y ≤ x
  using (Core.id.Id.unfold,
    Rat.order.≤.unfold,
    Rat.order.NonNegS.unfold,
    Rat.order.Sign.unfold,
    Rat.order.sNeg.eq,
    Rat.order.sPos.eq,
    Rat.order.sgnFlip.eq,
    Rat.Q.unfold)
leQTotal =
  λx y. ⊎-elim
    nn. inj₁ nn
    hneg. inj₂
      inj₂
        eqToId
          _
          _
          trans
            _
            _
            _
            trans
              _
              _
              sgnFlip (sgnQ (y + qNeg x))
              cong (λu. Sign) (λu. sgnQ u) {x + qNeg y} {qNeg (y + qNeg x)} qSubNeg
              sgnQNegFlip
            trans _ _ sPos (cong (λu. Sign) (λu. sgnFlip u) (idToEq _ _ _ hneg)) ⋆
    sgnCases (sgnQ (y + qNeg x))

-- ===== sign discrimination (transport along a discriminating family) =====
sIsNeg : Sign → 𝕌 using (Rat.order.Sign.unfold)
sIsNeg = λs. ⊎-elim (u. 𝟘) (v. ⊎-elim (u. 𝟘) (u. 𝟙) v) s

sIsPos : Sign → 𝕌 using (Rat.order.Sign.unfold)
sIsPos = λs. ⊎-elim (u. 𝟘) (v. ⊎-elim (u. 𝟙) (u. 𝟘) v) s

sZeroNotNeg : (sZero ≡ sNeg) → 𝟘
  using (Rat.order.sIsNeg.unfold, Rat.order.sNeg.unfold, Rat.order.sZero.unfold)
sZeroNotNeg = λh. transport sIsNeg (sym _ _ h) ()

sPosNotNeg : (sPos ≡ sNeg) → 𝟘
  using (Rat.order.sIsNeg.unfold, Rat.order.sNeg.unfold, Rat.order.sPos.unfold)
sPosNotNeg = λh. transport sIsNeg (sym _ _ h) ()

sZeroNotPos : (sZero ≡ sPos) → 𝟘
  using (Rat.order.sIsPos.unfold, Rat.order.sPos.unfold, Rat.order.sZero.unfold)
sZeroNotPos = λh. transport sIsPos (sym _ _ h) ()

sNegNotPos : (sNeg ≡ sPos) → 𝟘
  using (Rat.order.sIsPos.unfold, Rat.order.sNeg.unfold, Rat.order.sPos.unfold)
sNegNotPos = λh. transport sIsPos (sym _ _ h) ()

-- ===== views: a sign verdict names the integer's shape =====
intSgnPosView : (z : Int) → (intSgn z ≡ sPos) → (k : ℕ) × nzToInt (nzPos k) ≡ z
  using (Int.Int.unfold, Rat.frac.NZ.unfold, Rat.frac.nzNeg.eq, Rat.frac.nzPos.eq)
intSgnPosView =
  λz h. ⊎-elim
    u. ⊎-elim
      w. (nzToInt w ≡ z) → (k : ℕ) × nzToInt (nzPos k) ≡ z
      k. λhe. k, he
      k. λhe. 𝟘-elim
        sNegNotPos
          trans
            _
            _
            _
            sym
              _
              _
              trans
                _
                _
                sNeg
                cong (λv. Sign) (λv. intSgn v) (sym (nzToInt (nzNeg k)) _ he)
                intSgnNeg
            h
      u .π₁
      u .π₂
    hz. 𝟘-elim
      sZeroNotPos
        trans _ _ _ (sym _ _ (trans _ _ _ (cong (λv. Sign) (λv. intSgn v) hz) intSgnZero)) h
    nzOfInt z

intSgnZeroView : (z : Int) → (intSgn z ≡ sZero) → z ≡ intZero
  using (Int.Int.unfold, Rat.frac.NZ.unfold, Rat.frac.nzNeg.eq, Rat.frac.nzPos.eq)
intSgnZeroView =
  λz h. ⊎-elim
    u. ⊎-elim
      w. (nzToInt w ≡ z) → z ≡ intZero
      k. λhe. 𝟘-elim
        sZeroNotPos
          trans
            _
            _
            _
            sym _ _ h
            trans
              _
              _
              _
              cong (λv. Sign) (λv. intSgn v) (sym (nzToInt (nzPos k)) _ he)
              intSgnPos k
      k. λhe. 𝟘-elim
        sZeroNotNeg
          trans
            _
            _
            _
            sym _ _ h
            trans _ _ sNeg (cong (λv. Sign) (λv. intSgn v) (sym (nzToInt (nzNeg k)) _ he)) intSgnNeg
      u .π₁
      u .π₂
    hz. hz
    nzOfInt z

-- ===== positivity algebra =====
-- positives multiply to a positive: view both, drop to the NZ layer,
-- where nzMul computes its own sign table
intSgnPosMul : {a b : Int} → (intSgn a ≡ sPos) → (intSgn b ≡ sPos) → intSgn (a * b) ≡ sPos
  using (Int.Int.unfold,
    Rat.frac.nzMul.eq,
    Rat.frac.nzPos.eq,
    Rat.order.Sign.unfold,
    Rat.order.nzSgn.eq,
    Rat.order.sPos.eq)
intSgnPosMul =
  λa b ha hb. let va = intSgnPosView _ ha
                  vb = intSgnPosView _ hb
                  trans
                    _
                    _
                    _
                    cong
                      λv. Sign
                      λv. intSgn v
                      trans
                        _
                        _
                        _
                        cong (λv. Int) (λv. v * b) (sym _ _ (va .π₂))
                        cong (λv. Int) (λv. nzToInt (nzPos (va .π₁)) * v) (sym _ _ (vb .π₂))
                    trans
                      _
                      _
                      _
                      cong
                        λv. Sign
                        λv. intSgn v
                        sym _ _ (nzToIntMul (nzPos (va .π₁)) (nzPos (vb .π₁)))
                      trans _ _ sPos (intSgnNz (nzMul (nzPos (va .π₁)) (nzPos (vb .π₁)))) ⋆

-- positives add to a positive: both views land on class (S j , Z)
-- forms, whose sum computes to another one
intSgnPosAdd : {a b : Int} → (intSgn a ≡ sPos) → (intSgn b ≡ sPos) → intSgn (a + b) ≡ sPos
  using (Int.eq.classNormPairEq.eq,
    Int.eq.intCanon.eq,
    Int.eq.intCanonClass.eq,
    Core.equality.sym.eq,
    Core.equality.trans.eq,
    Int.nonZero.nzOfInt.eq,
    Int.nonZero.nzOfIntAt.eq,
    Int.nonZero.nzOfPairD.eq,
    Int.Int.eq,
    Int.Int.unfold,
    Int.intZero.eq,
    Int.add.+.eq,
    Int.mul.classPairEta.eq,
    Int.normalize.normPair.eq,
    Natural.+.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    Rat.inv.intCanonProdZero.eq,
    Rat.inv.normProdZero.eq,
    Rat.order.Sign.unfold,
    Rat.order.intSgn.eq,
    Rat.order.nzSgn.eq,
    Rat.order.sNeg.eq,
    Rat.order.sPos.eq,
    Rat.order.sZero.eq)
intSgnPosAdd =
  λa b ha hb. let va = intSgnPosView _ ha
                  vb = intSgnPosView _ hb
                  trans
                    _
                    _
                    _
                    cong
                      λv. Sign
                      λv. intSgn v
                      trans
                        _
                        _
                        _
                        cong (λv. Int) (λv. v + b) (sym _ _ (va .π₂))
                        cong (λv. Int) (λv. nzToInt (nzPos (va .π₁)) + v) (sym _ _ (vb .π₂))
                    ⋆

-- ratSgn, spelled in the nzToInt∘den vocabulary the shuffling lemmas
-- speak (denInt is its definitional alias)
ratSgnIs : (p : Rat) → ratSgn p ≡ intSgn (num p * nzToInt (den p))
  using (Int.Int.unfold,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.denInt.eq,
    Rat.order.Sign.unfold,
    Rat.order.ratSgn.eq)
ratSgnIs = λp. ⋆

-- the two cross terms of a fraction sum, scaled by the common
-- denominator, carry their fraction's sign: shuffle to
-- (num·den)·(den'·den') and drop the square
ratCrossPosL : {p : Rat}
  (q : Rat)
  → (ratSgn p ≡ sPos) → intSgn (intScale (den q) (num p) * nzToInt (nzMul (den p) (den q))) ≡ sPos
  using (Int.Int.unfold,
    ratSgnIs.rw,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.order.Sign.unfold)
ratCrossPosL =
  λp q hp. trans
    _
    _
    _
    cong
      λv. Sign
      λv. intSgn v
      {intScale (den q) (num p) * nzToInt (nzMul (den p) (den q))}
      {num p * nzToInt (den p) * (nzToInt (den q) * nzToInt (den q))}
      intScale (den q) (num p) * nzToInt (nzMul (den p) (den q))
        ≡⟨ cong
          λv. Int
          λv. v * nzToInt (nzMul (den p) (den q))
          intScaleIsMul (den q) (num p) ⟩
          nzToInt (den q) * num p * nzToInt (nzMul (den p) (den q))
        ≡⟨ cong (λv. Int) (λv. nzToInt (den q) * num p * v) (nzToIntMul (den p) (den q)) ⟩
          nzToInt (den q) * num p * (nzToInt (den p) * nzToInt (den q))
        ≡⟨ cong
          λv. Int
          λv. v * (nzToInt (den p) * nzToInt (den q))
          intMulComm (nzToInt (den q)) (num p) ⟩
          num p * nzToInt (den q) * (nzToInt (den p) * nzToInt (den q))
        ≡⟨ mulPairSwap (num p) (nzToInt (den q)) (nzToInt (den p)) (nzToInt (den q)) ⟩
          num p * nzToInt (den p) * (nzToInt (den q) * nzToInt (den q))
    trans _ _ sPos (intSgnMulSq (num p * nzToInt (den p)) (den q)) hp

ratCrossPosR : (p : Rat)
  {q : Rat}
  → (ratSgn q ≡ sPos) → intSgn (intScale (den p) (num q) * nzToInt (nzMul (den p) (den q))) ≡ sPos
  using (Int.Int.unfold,
    ratSgnIs.rw,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.order.Sign.unfold)
ratCrossPosR =
  λp q hq. trans
    _
    _
    _
    cong
      λv. Sign
      λv. intSgn v
      {intScale (den p) (num q) * nzToInt (nzMul (den p) (den q))}
      {num q * nzToInt (den q) * (nzToInt (den p) * nzToInt (den p))}
      intScale (den p) (num q) * nzToInt (nzMul (den p) (den q))
        ≡⟨ cong
          λv. Int
          λv. v * nzToInt (nzMul (den p) (den q))
          intScaleIsMul (den p) (num q) ⟩
          nzToInt (den p) * num q * nzToInt (nzMul (den p) (den q))
        ≡⟨ cong (λv. Int) (λv. nzToInt (den p) * num q * v) (nzToIntMul (den p) (den q)) ⟩
          nzToInt (den p) * num q * (nzToInt (den p) * nzToInt (den q))
        ≡⟨ cong
          λv. Int
          λv. v * (nzToInt (den p) * nzToInt (den q))
          intMulComm (nzToInt (den p)) (num q) ⟩
          num q * nzToInt (den p) * (nzToInt (den p) * nzToInt (den q))
        ≡⟨ mulPairSwapR (num q) (nzToInt (den p)) (nzToInt (den p)) (nzToInt (den q)) ⟩
          num q * nzToInt (den q) * (nzToInt (den p) * nzToInt (den p))
    trans _ _ sPos (intSgnMulSq (num q * nzToInt (den q)) (den p)) hq

-- positive fractions add to a positive fraction
ratAddPos : {p q : Rat} → (ratSgn p ≡ sPos) → (ratSgn q ≡ sPos) → ratSgn (ratAdd p q) ≡ sPos
  using (Int.nonZero.nzOfInt.eq,
    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.denInt.eq,
    Rat.frac.intScale.eq,
    Rat.frac.intScaleN.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.order.intSgn.eq,
    Rat.order.nzSgn.eq,
    Rat.order.ratSgn.eq,
    Rat.order.sZero.eq)
ratAddPos =
  λp q hp hq. trans
    _
    _
    _
    cong
      λv. Sign
      λv. intSgn v
      intMulDistribR
        intScale (den q) (num p)
        intScale (den p) (num q)
        nzToInt (nzMul (den p) (den q))
    intSgnPosAdd (ratCrossPosL q hp) (ratCrossPosR p hq)

-- ===== lifting to ℚ =====
-- positivity adds (representatives abstract, hypotheses as Π's in the
-- motive — the qMulInvR pattern)
sgnQAddPos : (u v : Q) → (sgnQ u ≡ sPos) → (sgnQ v ≡ sPos) → sgnQ (u + v) ≡ sPos
  using (Core.equality.cong.eq,
    Core.equality.trans.eq,
    Int.order.intMulDistribR.eq,
    Int.Int.eq,
    Int.Int.unfold,
    Int.add.+.eq,
    Int.mul.*.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.intScale.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzToInt.eq,
    Rat.frac.ratAdd.eq,
    Rat.order.Sign.eq,
    Rat.order.intSgn.eq,
    Rat.order.intSgnPosAdd.eq,
    Rat.order.ratAddPos.eq,
    Rat.order.ratCrossPosL.eq,
    Rat.order.ratCrossPosR.eq,
    Rat.order.ratSgn.eq,
    Rat.order.sPos.eq,
    Rat.order.sgnQ.eq,
    Rat.Q.unfold,
    Rat.RatR.unfold,
    Rat.+.eq)
sgnQAddPos = λu v. quot-elim (p. quot-elim (q. λhp hq. ratAddPos hp hq) v) u

-- a zero sign names the zero class
sgnQZeroView : (u : Q) → (sgnQ u ≡ sZero) → u ≡ qZero
  using (Natural.eq.zNotS.eq,
    Core.equality.cong.eq,
    Core.equality.sym.eq,
    Core.equality.trans.eq,
    Int.nonZero.intNeqOfNotRel.eq,
    Int.nonZero.intNoZeroDiv.eq,
    Int.nonZero.nzOfInt.eq,
    Int.nonZero.nzToIntNonZero.eq,
    Int.Int.eq,
    Int.Int.unfold,
    Int.intZero.eq,
    Int.mul.*.eq,
    Int.mul.intMulCong2.eq,
    Int.mul.intMulOneR.eq,
    Int.mul.intMulZeroL.eq,
    Core.prop.absurdP.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.denInt.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzNeg.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    Rat.frac.ratZero.eq,
    Rat.inv.notApply.eq,
    Rat.inv.ratZeroOfNumZero.eq,
    Rat.order.Sign.eq,
    Rat.order.intSgn.eq,
    Rat.order.intSgnNeg.eq,
    Rat.order.intSgnPos.eq,
    Rat.order.intSgnZeroView.eq,
    Rat.order.nzSgn.eq,
    Rat.order.ratSgn.eq,
    Rat.order.sNeg.eq,
    Rat.order.sPos.eq,
    Rat.order.sZero.eq,
    Rat.order.sZeroNotNeg.eq,
    Rat.order.sZeroNotPos.eq,
    Rat.order.sgnQ.eq,
    Rat.Q.unfold,
    Rat.RatR.unfold,
    Rat.clsEqOfRel.eq,
    Rat.dInt.eq,
    Rat.nzToIntMul.eq)
sgnQZeroView =
  λu. quot-elim
    p. λh. ratZeroOfNumZero
      _
      intNoZeroDiv _ (intSgnZeroView (num p * denInt p) h) (nzToIntNonZero (den p))
    u

-- (z − y) + (y − x) ≡ z − x
qSubSplit : (x y z : Q) → z + qNeg y + (y + qNeg x) ≡ z + qNeg x using (Rat.Q.unfold)
qSubSplit =
  λx y z. z + qNeg y + (y + qNeg x)
    ≡⟨ qAddAssoc z (qNeg y) (y + qNeg x) ⟩ z + (qNeg y + (y + qNeg x))
    ≡⟨ cong (λw. Q) (λw. z + w) (qNegPlusCancel y (qNeg x)) ⟩ z + qNeg x

-- (a − b) + b ≡ a, hypothesis-free
qPlusNegCancelR : (a b : Q) → a + qNeg b + b ≡ a using (Rat.Q.unfold)
qPlusNegCancelR =
  λa b. a + qNeg b + b
    ≡⟨ qAddAssoc a (qNeg b) b ⟩ a + (qNeg b + b)
    ≡⟨ cong (λw. Q) (λw. a + w) (qAddNegL b) ⟩ a + qZero
    ≡⟨ qAddZeroR a ⟩ a

-- a zero difference names an equality
qDiffZero : {a b : Q} → (a + qNeg b ≡ qZero) → a ≡ b
qDiffZero =
  λa b h. trans
    _
    _
    _
    sym _ _ (qPlusNegCancelR a b)
    trans _ _ _ (cong (λw. Q) (λw. w + b) h) (qAddZeroL b)

-- ===== transitivity and antisymmetry =====
leQTrans : (x y z : Q) → x ≤ y → y ≤ z → x ≤ z
  using (Core.id.Id.unfold, Rat.order.≤.unfold, Rat.order.NonNegS.unfold, Rat.Q.unfold)
leQTrans =
  λx y z l1 l2. let comb : sgnQ (z + qNeg x) ≡ sgnQ (z + qNeg y + (y + qNeg x))
                      = cong (λw. Sign) (λw. sgnQ w) (sym _ _ (qSubSplit x y z))
                    ⊎-elim
                      h10. let e0 = sgnQZeroView _ (idToEq _ _ _ h10)
                               eq : sgnQ (z + qNeg x) ≡ sgnQ (z + qNeg y)
                                 = trans
                                   _
                                   _
                                   _
                                   comb
                                   cong
                                     λw. Sign
                                     λw. sgnQ w
                                     trans
                                       _
                                       _
                                       _
                                       cong (λw. Q) (λw. z + qNeg y + w) e0
                                       qAddZeroR (z + qNeg y)
                               transport NonNegS (sym _ _ eq) l2
                      h1p. ⊎-elim
                        h20. let e0 = sgnQZeroView _ (idToEq _ _ _ h20)
                                 eq : sgnQ (z + qNeg x) ≡ sgnQ (y + qNeg x)
                                   = trans
                                     _
                                     _
                                     _
                                     comb
                                     cong
                                       λw. Sign
                                       λw. sgnQ w
                                       trans
                                         _
                                         _
                                         _
                                         cong (λw. Q) (λw. w + (y + qNeg x)) e0
                                         qAddZeroL (y + qNeg x)
                                 transport NonNegS (sym _ _ eq) (inj₂ h1p)
                        h2p. inj₂
                          eqToId
                            _
                            _
                            trans _ _ _ comb (sgnQAddPos _ _ (idToEq _ _ _ h2p) (idToEq _ _ _ h1p))
                        l2
                      l1

leQAntisym : {x y : Q} → x ≤ y → y ≤ x → x ≡ y
  using (Core.id.Id.unfold,
    Rat.order.≤.unfold,
    Rat.order.NonNegS.unfold,
    Rat.order.Sign.unfold,
    Rat.order.sNeg.eq,
    Rat.order.sPos.eq,
    Rat.order.sgnFlip.eq,
    Rat.Q.unfold)
leQAntisym =
  λx y l1 l2. let fl : sgnQ (x + qNeg y) ≡ sgnFlip (sgnQ (y + qNeg x))
                    = trans
                      _
                      _
                      _
                      cong (λw. Sign) (λw. sgnQ w) {x + qNeg y} {qNeg (y + qNeg x)} qSubNeg
                      sgnQNegFlip
                  ⊎-elim
                    h10. sym _ _ (qDiffZero (sgnQZeroView _ (idToEq _ _ _ h10)))
                    h1p. let en : sgnQ (x + qNeg y) ≡ sNeg
                               = trans
                                 _
                                 _
                                 _
                                 fl
                                 trans
                                   _
                                   _
                                   sNeg
                                   cong (λw. Sign) (λw. sgnFlip w) (idToEq _ _ _ h1p)
                                   ⋆
                             ⊎-elim
                               h20. 𝟘-elim
                                 sZeroNotNeg (trans _ _ _ (sym _ _ (idToEq _ _ _ h20)) en)
                               h2p. 𝟘-elim
                                 sPosNotNeg (trans _ _ _ (sym _ _ (idToEq _ _ _ h2p)) en)
                               l2
                    l1

-- ===== compatibility with the operations =====
-- (y + w) − (x + w) ≡ y − x, hypothesis-free
qSubPlusCancel : (x y w : Q) → y + w + qNeg (x + w) ≡ y + qNeg x using (Rat.Q.unfold)
qSubPlusCancel =
  λx y w. y + w + qNeg (x + w)
    ≡⟨ cong (λv. Q) (λv. y + w + v) (qNegAdd x w) ⟩ y + w + (qNeg x + qNeg w)
    ≡⟨ qPairSwap y w (qNeg x) (qNeg w) ⟩ y + qNeg x + (w + qNeg w)
    ≡⟨ cong (λv. Q) (λv. y + qNeg x + v) (qAddNegR w) ⟩ y + qNeg x + qZero
    ≡⟨ qAddZeroR (y + qNeg x) ⟩ y + qNeg x

-- monotonicity of + : one transport along the cancelled difference
leQPlusMono : {x y : Q} (w : Q) → x ≤ y → x + w ≤ y + w
  using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold, Rat.Q.unfold)
leQPlusMono =
  λx y w le. transport NonNegS (sym _ _ (cong (λv. Sign) (λv. sgnQ v) (qSubPlusCancel x y w))) le

leQPlusMonoL : (x y w : Q) → x ≤ y → w + x ≤ w + y
  using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold)
leQPlusMonoL =
  λx y w le. transport
    λv. v ≤ w + y
    qAddComm x w
    transport (λv. x + w ≤ v) (qAddComm y w) (leQPlusMono w le)

-- the sign of a product, spelled on the components
ratSgnMulIs : (p q : Rat)
  → ratSgn (ratMul p q) ≡ intSgn (num p * num q * nzToInt (nzMul (den p) (den q)))
  using (Int.Int.unfold,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.denInt.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.order.Sign.unfold,
    Rat.order.ratSgn.eq,
    Rat.ratMul.eq)
ratSgnMulIs = λp q. ⋆

-- positive fractions multiply to a positive fraction: interchange
-- num·num · den·den into (num·den)·(num·den)
ratMulPos : {p q : Rat} → (ratSgn p ≡ sPos) → (ratSgn q ≡ sPos) → ratSgn (ratMul p q) ≡ sPos
  using (Int.Int.unfold,
    ratSgnIs.rw,
    ratSgnMulIs,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.order.Sign.unfold)
ratMulPos =
  λp q hp hq. trans
    _
    intSgn (num p * nzToInt (den p) * (num q * nzToInt (den q)))
    _
    cong
      λv. Sign
      λv. intSgn v
      {num p * num q * nzToInt (nzMul (den p) (den q))}
      {num p * nzToInt (den p) * (num q * nzToInt (den q))}
      num p * num q * nzToInt (nzMul (den p) (den q))
        ≡⟨ cong (λv. Int) (λv. num p * num q * v) (nzToIntMul (den p) (den q)) ⟩
          num p * num q * (nzToInt (den p) * nzToInt (den q))
        ≡⟨ mulPairSwap (num p) (num q) (nzToInt (den p)) (nzToInt (den q)) ⟩
          num p * nzToInt (den p) * (num q * nzToInt (den q))
    intSgnPosMul hp hq

sgnQMulPos : {u v : Q} → (sgnQ u ≡ sPos) → (sgnQ v ≡ sPos) → sgnQ (u * v) ≡ sPos
  using (Core.equality.cong.eq,
    Core.equality.trans.eq,
    Int.Int.eq,
    Int.Int.unfold,
    Int.mul.*.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.denInt.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzToInt.eq,
    Rat.order.Sign.eq,
    Rat.order.intSgn.eq,
    Rat.order.intSgnPosMul.eq,
    Rat.order.ratMulPos.eq,
    Rat.order.ratSgn.eq,
    Rat.order.sPos.eq,
    Rat.order.sgnQ.eq,
    Rat.Q.unfold,
    Rat.RatR.unfold,
    Rat.*.eq,
    Rat.ratMul.eq)
sgnQMulPos = λu v. quot-elim (p. quot-elim (q. λhp hq. ratMulPos hp hq) v) u

-- (−x)·c ≡ −(x·c) on ℚ, by inverse uniqueness
qNegMulL : (x c : Q) → qNeg x * c ≡ qNeg (x * c)
qNegMulL =
  λx c. qNegUnique
    trans
      _
      _
      _
      sym _ _ (qDistribR c x (qNeg x))
      trans _ _ qZero (cong (λv. Q) (λv. v * c) (qAddNegR x)) qMulZeroL

-- (y − x)·c ≡ y·c − x·c, hypothesis-free
qSubDistribR : (x y c : Q) → (y + qNeg x) * c ≡ y * c + qNeg (x * c) using (Rat.Q.unfold)
qSubDistribR =
  λx y c. (y + qNeg x) * c
    ≡⟨ qDistribR c y (qNeg x) ⟩ y * c + qNeg x * c
    ≡⟨ cong (λv. Q) (λv. y * c + v) (qNegMulL x c) ⟩ y * c + qNeg (x * c)

-- monotonicity of · by a NONNEGATIVE scalar: case the scalar's sign —
-- a zero scalar collapses both sides, a positive one cases the
-- difference's own sign
-- c ≡ 0: both products are zero, difference too
-- c positive: case the difference's sign
-- y − x ≡ 0: products differ by zero
leQMulMono : (x y : Q) {c : Q} → x ≤ y → qZero ≤ c → x * c ≤ y * c
  using (Int.intNeg.eq,
    Int.intZero.eq,
    Rat.frac.den.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.ratNeg.eq,
    Rat.frac.ratOfInt.eq,
    Rat.frac.ratZero.eq,
    Rat.order.≤.unfold,
    Rat.order.NonNegS.unfold,
    Rat.Q.unfold,
    Rat.qNeg.eq,
    Rat.qZero.eq,
    Rat.qcls.eq)
leQMulMono =
  λx y c le lc. let dEq : sgnQ (y * c + qNeg (x * c)) ≡ sgnQ ((y + qNeg x) * c)
                      = cong (λv. Sign) (λv. sgnQ v) (sym _ _ (qSubDistribR x y c))
                    cEq : sgnQ (c + qNeg qZero) ≡ sgnQ c
                      = cong
                        λv. Sign
                        λv. sgnQ v
                        trans _ _ _ (cong (λv. Q) (λv. c + v) {qNeg qZero} {qZero} ⋆) (qAddZeroR c)
                    ⊎-elim
                      hc0. let c0 : c ≡ qZero
                                 = sgnQZeroView _ (trans _ _ _ (sym _ _ cEq) (idToEq _ _ _ hc0))
                               inj₁
                                 eqToId
                                   _
                                   _
                                   trans
                                     _
                                     _
                                     _
                                     dEq
                                     trans
                                       _
                                       _
                                       _
                                       cong
                                         λv. Sign
                                         λv. sgnQ v
                                         trans
                                           _
                                           _
                                           _
                                           cong (λv. Q) (λv. (y + qNeg x) * v) c0
                                           trans _ _ qZero (qMulComm (y + qNeg x) qZero) qMulZeroL
                                       sgnQZero
                      hcp. let hcs : sgnQ c ≡ sPos = trans _ _ _ (sym _ _ cEq) (idToEq _ _ _ hcp)
                               ⊎-elim
                                 hd0. let d0 : y + qNeg x ≡ qZero
                                            = sgnQZeroView _ (idToEq _ _ _ hd0)
                                          inj₁
                                            eqToId
                                              _
                                              _
                                              trans
                                                _
                                                _
                                                _
                                                dEq
                                                trans
                                                  _
                                                  _
                                                  _
                                                  cong
                                                    λv. Sign
                                                    λv. sgnQ v
                                                    trans
                                                      _
                                                      _
                                                      qZero
                                                      cong (λv. Q) (λv. v * c) d0
                                                      qMulZeroL
                                                  sgnQZero
                                 hdp. inj₂
                                   eqToId _ _ (trans _ _ _ dEq (sgnQMulPos (idToEq _ _ _ hdp) hcs))
                                 le
                      lc