Rat.arch

-- THE ARCHIMEDEAN PROPERTY of ℚ: every positive rational dominates
-- one of the unit fractions 1/(k+1). Normalize the denominator to be
-- positive, read the numerator's sign off intNonZero's decision, and
-- the index is the denominator's own magnitude — (a+1)/(b+1) is at
-- least 1/(b+1) because the difference is ((b+1)·a)/(b+1)², whose
-- numerator is a NAT.
--
-- The index is SQUASHED: it depends on the representative (½ and 2/4
-- name 2 and 4), so a bare Σ would owe a well-definedness proof it
-- cannot have. The squash costs nothing downstream, because the fact
-- it is used to prove — leQOfArch — lands in a DECIDABLE type, and a
-- decidable goal can be reached from ⊥ (leQOfFalse).
--
-- leQOfArch is the closeness principle the constructive reals run on:
-- "a ≤ b + 1/(k+1) for every k" collapses to "a ≤ b".
-- ===== fractions with a natural numerator =====

import Natural (+, *, multZeroId, plusZeroId, zeroPlusId, sucPlus, multComm, zeroMult, multSucId)
import Int (Int, intZero, intOne, intNeg)
import Int.add (+)
import Int.mul (*, intMulZeroL, intMulNegL, intMulNegR, intNegNeg)
import Int.order (intOfNat, intOfNatMul)
import Int.nonZero (nzOfInt)
import Rat.frac (NZ, nzPos, nzNeg, nzToInt, nzMul, Rat, mkRat, num, den, denInt, ratNeg, ratEta, intScale)
import Rat (Q, qcls, +, qNeg, qZero, RatR, clsEqOfRel, nzToIntMul, dInt, qAddAssoc, qAddComm, qAddZeroR, qAddNegR, qAddNegL)
import Rat.order (Sign, sZero, sPos, sNeg, sgnFlip, sgnQ, ratSgn, intSgn, intSgnZero, intSgnPos, intSgnNeg, NonNegS, ≤, sgnQCls, sgnQZero, sgnCases, sgnQNegFlip, qSubNeg, leQTrans, leQAntisym, sZeroNotPos, sZeroNotNeg, sNegNotPos, leQPlusMono, leQPlusMonoL, qNegAdd, qPairSwap)
import Rat.bound (Bnd, qSubFlip, leQSelfAdd, nonNegNotNeg)
import Rat.half (dbl, qInvHalf, leQInvDbl, leQZeroInvNat)
import Real (qInvNat, qInvNatPos)
import Core.prop (⊥, absurdP)
import Core.equality (trans, sym, cong, transport)
import Core.id (Id, eqToId, idToEq)

qFrac : ℕ → ℕ → Q using (Rat.Q.unfold)
qFrac = λa b. qcls (mkRat (intOfNat a) (nzPos b))

-- 1/(b+1) is 1/(b+1) — the two spellings coincide on the nose
qFracOne : (b : ℕ) → qFrac (S Z) b ≡ qInvNat b
  using (Int.order.intOfNat.eq,
    Int.intOne.eq,
    Rat.arch.qFrac.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.nzPos.eq,
    Rat.Q.unfold,
    Rat.qcls.eq,
    Real.qInvNat.eq)
qFracOne = λb. ⋆

-- the sign of a natural is never negative
intSgnOfNatNonNeg : {k : ℕ} → NonNegS (intSgn (intOfNat k))
  using (Int.order.intOfNatZero,
    Int.Int.unfold,
    Rat.half.nzPosInt,
    Rat.order.NonNegS.unfold,
    Rat.order.Sign.unfold)
intSgnOfNatNonNeg =
  λk. ℕ-elim (inj₁ (eqToId _ _ intSgnZero)) (j ih. inj₂ (eqToId _ _ (intSgnPos j))) k

-- ...so a fraction with a natural numerator over a positive
-- denominator is never negative: its sign is that of the natural a·(b+1)
sgnQFrac : (a b : ℕ) → sgnQ (qFrac a b) ≡ intSgn (intOfNat (a * S b))
  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.order.intOfNat.eq,
    Int.Int.eq,
    Int.intZero.eq,
    Int.mul.classPairEta.eq,
    Int.mul.*.eq,
    Int.normalize.normPair.eq,
    Rat.arch.qFrac.eq,
    Rat.frac.denInt.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    Rat.inv.intCanonProdZero.eq,
    Rat.inv.normProdZero.eq,
    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.qcls.eq)
sgnQFrac = λa b. cong (λv. Sign) (λv. intSgn v) (intOfNatMul a (S b))

nonNegSgnFrac : {a b : ℕ} → NonNegS (sgnQ (qFrac a b)) using (Rat.order.NonNegS.unfold)
nonNegSgnFrac = λa b. transport NonNegS (sym _ _ (sgnQFrac a b)) intSgnOfNatNonNeg

-- ===== 1/(b+1) ≤ (a+1)/(b+1) =====
-- the difference is ((b+1)·a) / (b+1)²: the denominators are literally
-- equal (nzMul computes), so only the numerators have to be matched
fracNumEq : {a b : ℕ}
  → intScale (nzPos b) (intOfNat (S a)) + intScale (nzPos b) (intNeg intOne) ≡ intOfNat (S b * a)
  using (multZeroId.rw,
    zeroPlusId.rw,
    plusZeroId.rw,
    multSucId.rw,
    Int.Int.eq,
    Int.IntR.eq,
    Int.intNeg.eq,
    Int.intOne.eq,
    Int.add.+.eq,
    Int.order.intOfNat.eq,
    Rat.frac.intScale.eq,
    Rat.frac.intScaleN.eq,
    Rat.frac.nzPos.eq)
fracNumEq = λa b. ⋆

qDiffFracInv : (a b : ℕ) → qFrac (S a) b + qNeg (qInvNat b) ≡ qFrac (S b * a) (b * b + b + b)
  using (Int.order.intOfNat.eq,
    Int.intNeg.eq,
    Int.intOne.eq,
    Int.add.+.eq,
    Rat.arch.qFrac.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.ratAdd.eq,
    Rat.frac.ratNeg.eq,
    Rat.+.eq,
    Rat.qNeg.eq,
    Rat.qcls.eq,
    Real.qInvNat.eq)
qDiffFracInv =
  λa b. cong
    λv. Q
    λv. qcls (mkRat v (nzPos (b * b + b + b)))
    {intScale (nzPos b) (intOfNat (S a)) + intScale (nzPos b) (intNeg intOne)}
    {intOfNat (S b * a)}
    fracNumEq

leQInvFrac : {a b : ℕ} → qInvNat b ≤ qFrac (S a) b
  using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold)
leQInvFrac = λa b. transport (λw. NonNegS (sgnQ w)) (sym _ _ (qDiffFracInv a b)) nonNegSgnFrac

-- ===== normalizing the denominator's sign =====
-- the cross-multiplication behind qNegDen, in folded vocabulary
negDenCross : (N : Int) (b : ℕ) → intNeg N * intNeg (nzToInt (nzPos b)) ≡ N * nzToInt (nzPos b)
  using (Int.Int.unfold)
negDenCross =
  λN b. intNeg N * intNeg (nzToInt (nzPos b))
    ≡⟨ intMulNegL N (intNeg (nzToInt (nzPos b))) ⟩ intNeg (N * intNeg (nzToInt (nzPos b)))
    ≡⟨ cong (λv. Int) (λv. intNeg v) (intMulNegR N (nzToInt (nzPos b))) ⟩
      intNeg (intNeg (N * nzToInt (nzPos b)))
    ≡⟨ intNegNeg (N * nzToInt (nzPos b)) ⟩ N * nzToInt (nzPos b)

-- N/(−(b+1)) and (−N)/(b+1) are the same rational
qNegDen : (N : Int) (b : ℕ) → qcls (mkRat (intNeg N) (nzPos b)) ≡ qcls (mkRat N (nzNeg b))
  using (Int.Int.unfold,
    Int.intNeg.eq,
    Rat.frac.den.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzNeg.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    Rat.RatR.eq,
    Rat.dInt.eq,
    Rat.qcls.eq)
qNegDen = λN b. clsEqOfRel (mkRat (intNeg N) (nzPos b)) (mkRat N (nzNeg b)) (negDenCross N b)

-- every rational has a representative with a POSITIVE denominator
PosDenView : Q → 𝕌
PosDenView = λu. (M : Int) (b : ℕ) × Id _ (qcls (mkRat M (nzPos b))) u

qPosDenView : (N : Int) (d : NZ) → PosDenView (qcls (mkRat N d))
  using (Core.id.Id.eq,
    Int.Int.unfold,
    Int.intNeg.eq,
    Rat.arch.PosDenView.unfold,
    Rat.frac.NZ.unfold,
    Rat.frac.mkRat.eq,
    Rat.frac.nzNeg.eq,
    Rat.frac.nzPos.eq,
    Rat.Q.eq,
    Rat.qcls.eq)
qPosDenView =
  λN d. ⊎-elim
    b. N, b, eqToId _ (qcls (mkRat N (nzPos b))) ⋆
    b. intNeg N, b, eqToId _ (qcls (mkRat N (nzNeg b))) (qNegDen N b)
    d

-- ===== the sign of a fraction with a decided numerator =====
-- a negative numerator over a positive denominator is negative
sgnNegOverPos : {a b : ℕ} → sgnQ (qcls (mkRat (nzToInt (nzNeg a)) (nzPos b))) ≡ sNeg
  using (Int.eq.intCanon.eq,
    Int.eq.intCanonClass.eq,
    Int.nonZero.nzOfInt.eq,
    Int.nonZero.nzOfIntAt.eq,
    Int.mul.*.eq,
    Rat.frac.denInt.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.inv.intCanonProdZero.eq,
    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.qcls.eq)
sgnNegOverPos =
  λa b. trans
    intSgn (nzToInt (nzNeg a) * nzToInt (nzPos b))
    _
    _
    cong (λv. Sign) (λv. intSgn v) (sym _ _ (nzToIntMul (nzNeg a) (nzPos b)))
    intSgnNeg

-- a zero numerator makes the fraction zero
sgnZeroOverPos : {b : ℕ} → sgnQ (qcls (mkRat intZero (nzPos b))) ≡ sZero
  using (Int.eq.intCanon.eq,
    Int.eq.intCanonClass.eq,
    Int.nonZero.nzOfInt.eq,
    Int.nonZero.nzOfIntAt.eq,
    Int.intZero.eq,
    Int.mul.*.eq,
    Rat.frac.denInt.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    Rat.inv.intCanonProdZero.eq,
    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.qcls.eq)
sgnZeroOverPos =
  λb. trans
    intSgn (intZero * nzToInt (nzPos b))
    _
    _
    cong (λv. Sign) (λv. intSgn v) (intMulZeroL (nzToInt (nzPos b)))
    intSgnZero

-- ===== the theorem =====
ArchWit : Q → 𝕌
ArchWit = λu. (k : ℕ) × qInvNat k ≤ u

-- with a positive denominator fixed, decide the numerator: positive
-- gives the index, zero and negative contradict positivity
qArchPos : {M : Int}
  {b : ℕ}
  → (sgnQ (qcls (mkRat M (nzPos b))) ≡ sPos) → ArchWit (qcls (mkRat M (nzPos b)))
  using (Int.order.intOfNat.eq,
    Int.Int.unfold,
    Rat.arch.ArchWit.unfold,
    Rat.arch.qFrac.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.mkRat.eq,
    Rat.frac.nzNeg.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    Rat.qcls.eq)
qArchPos =
  λM b hp. ⊎-elim
    u. ⊎-elim
      w. (nzToInt w ≡ M) → ArchWit (qcls (mkRat M (nzPos b)))
      a. λhe. (,)
        b
        transport
          λv. qInvNat b ≤ v
          {qFrac (S a) b}
          {qcls (mkRat M (nzPos b))}
          cong (λv. Q) (λv. qcls (mkRat v (nzPos b))) {nzToInt (nzPos a)} he
          leQInvFrac
      a. λhe. 𝟘-elim
        sNegNotPos
          trans
            _
            _
            _
            sym
              _
              _
              trans
                _
                _
                sNeg
                cong (λv. Sign) (λv. sgnQ (qcls (mkRat v (nzPos b)))) (sym (nzToInt (nzNeg a)) _ he)
                sgnNegOverPos
            hp
      u .π₁
      u .π₂
    hz. 𝟘-elim
      sZeroNotPos
        trans
          _
          _
          _
          sym
            _
            _
            trans
              _
              _
              sZero
              cong (λv. Sign) (λv. sgnQ (qcls (mkRat v (nzPos b)))) hz
              sgnZeroOverPos
          hp
    nzOfInt M

-- at a raw fraction: normalize the denominator, then decide
qArchAt : (N : Int) (d : NZ) → (sgnQ (qcls (mkRat N d)) ≡ sPos) → ArchWit (qcls (mkRat N d))
  using (Rat.arch.ArchWit.unfold, Rat.arch.PosDenView.unfold)
qArchAt =
  λN d hp. let v = qPosDenView N d
               e : qcls (mkRat (v .π₁) (nzPos (v .π₂ .π₁))) ≡ qcls (mkRat N d)
                 = idToEq _ _ _ (v .π₂ .π₂)
               transport ArchWit e (qArchPos (trans _ _ _ (cong (λw. Sign) (λw. sgnQ w) e) hp))

-- every positive rational dominates a unit fraction. The witness is
-- squashed: a bare Σ would ask the class to determine the index
qArch : (u : Q) → (sgnQ u ≡ sPos) → ∥ArchWit u∥
  using (Core.id.Id.eq,
    Int.Int.unfold,
    Rat.arch.ArchWit.unfold,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.order.≤.unfold,
    Rat.order.NonNegS.unfold,
    Rat.order.Sign.eq,
    Rat.order.sPos.eq,
    Rat.order.sZero.eq,
    Rat.order.sgnQ.eq,
    Rat.Q.unfold,
    Rat.+.eq,
    Rat.qNeg.eq,
    Rat.qcls.eq,
    Real.qInvNat.eq)
qArch =
  λu. quot-elim
    p. λhp. ⋆
      transport
        λr. ArchWit (qcls r)
        {mkRat (num p) (den p)}
        {p}
        ratEta
        qArchAt
          _
          _
          trans _ _ sPos (cong (λr. Sign) (λr. sgnQ (qcls r)) {mkRat (num p) (den p)} {p} ratEta) hp
    u

-- ===== the closeness principle =====
-- a decidable goal is reachable from ⊥ : an order fact is a SIGN
-- verdict, and ⊥ proves the equation that verdict needs
leQOfFalse : {x y : Q} → ⊥ → x ≤ y using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold)
leQOfFalse = λx y f. inj₁ (eqToId _ _ (absurdP (sgnQ (y + qNeg x) ≡ sZero) f))

-- the difference's sign flips with the difference (leQTotal's core,
-- named)
sgnQSubFlip : {x y : Q} → sgnQ (x + qNeg y) ≡ sgnFlip (sgnQ (y + qNeg x))
sgnQSubFlip =
  λx y. trans
    _
    _
    _
    cong (λw. Sign) (λw. sgnQ w) {x + qNeg y} {qNeg (y + qNeg x)} qSubNeg
    sgnQNegFlip

-- (b + q) − a ≡ q − (a − b): moving a subtraction across the ≤
qShiftEq : (a b q : Q) → b + q + qNeg a ≡ q + qNeg (a + qNeg b) using (Rat.Q.unfold)
qShiftEq =
  λa b q. b + q + qNeg a
    ≡⟨ cong (λw. Q) (λw. w + qNeg a) (qAddComm b q) ⟩ q + b + qNeg a
    ≡⟨ qAddAssoc q b (qNeg a) ⟩ q + (b + qNeg a)
    ≡⟨ cong (λw. Q) (λw. q + w) (sym _ _ (qSubFlip a b)) ⟩ q + qNeg (a + qNeg b)

leQSubShift : (a b : Q) {q : Q} → a ≤ b + q → a + qNeg b ≤ q
  using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold, Rat.Q.unfold)
leQSubShift = λa b q. transport (λw. NonNegS (sgnQ w)) (qShiftEq a b q)

-- h + h ≡ h forces h ≡ 0
qAddSelfCancel : (h : Q) → (h + h ≡ h) → h ≡ qZero
qAddSelfCancel =
  λh e. trans
    _
    _
    _
    sym
      _
      _
      trans
        _
        _
        _
        qAddAssoc h h (qNeg h)
        trans _ _ _ (cong (λw. Q) (λw. h + w) (qAddNegR h)) (qAddZeroR h)
    trans _ _ _ (cong (λw. Q) (λw. w + qNeg h) e) (qAddNegR h)

-- no unit fraction is zero
qInvNatNotZero : (k : ℕ) → (qInvNat k ≡ qZero) → 𝟘
qInvNatNotZero =
  λk e. sZeroNotPos
    trans _ _ _ (sym _ _ (trans _ _ _ (cong (λw. Sign) (λw. sgnQ w) e) sgnQZero)) (qInvNatPos k)

-- a < b would give an index k with 1/(k+1) ≤ a − b ≤ 1/(2k+2), and
-- those two unit fractions are equal only if the smaller is zero
archContra : (a b : Q) → ((k : ℕ) → a ≤ b + qInvNat k) → Id _ (sgnQ (b + qNeg a)) sNeg → ⊥
  using (Core.equality.cong.eq,
    Core.equality.trans.eq,
    hyp.rw,
    Core.id.Id.eq,
    Core.id.Id.unfold,
    Core.id.idToEq.eq,
    Core.prop.⊥.unfold,
    Rat.arch.ArchWit.unfold,
    Rat.order.≤.eq,
    Rat.order.≤.unfold,
    Rat.order.NonNegS.unfold,
    Rat.order.Sign.eq,
    Rat.order.sNeg.eq,
    Rat.order.sPos.eq,
    Rat.order.sZero.eq,
    Rat.order.sgnFlip.eq,
    Rat.order.sgnQ.eq,
    Rat.Q.eq,
    Rat.Q.unfold,
    Rat.+.eq,
    Rat.qNeg.eq,
    Real.qInvNat.eq,
    sgnQSubFlip.eq)
archContra =
  λa b hyp hneg. let hpos : sgnQ (a + qNeg b) ≡ sPos
                       = trans
                         _
                         _
                         _
                         sgnQSubFlip
                         trans _ _ sPos (cong (λw. Sign) (λw. sgnFlip w) (idToEq _ _ _ hneg)) ⋆
                     squash-elim
                       qArch _ hpos
                       w. let hup : qInvNat (w .π₁) ≡ qInvNat (dbl (w .π₁))
                                = leQAntisym
                                  leQTrans _ _ _ (w .π₂) (leQSubShift _ _ (hyp (dbl (w .π₁))))
                                  leQInvDbl (w .π₁)
                              ⋆
                                qInvNatNotZero
                                  _
                                  qAddSelfCancel _ (trans _ _ _ (qInvHalf (w .π₁)) hup)

-- ...so "a ≤ b + 1/(k+1) for every k" collapses to "a ≤ b"
leQOfArch : (a b : Q) → ((k : ℕ) → a ≤ b + qInvNat k) → a ≤ b
  using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold, Rat.Q.unfold)
leQOfArch =
  λa b hyp. ⊎-elim
    nn. nn
    hneg. leQOfFalse (archContra _ _ hyp hneg)
    sgnCases (sgnQ (b + qNeg a))

-- ===== closeness, in Bnd form =====
-- −(b + h) + h ≡ −b : the ε moves back out of a negated bound
qNegAddCancel : {b h : Q} → qNeg (b + h) + h ≡ qNeg b using (Rat.Q.unfold)
qNegAddCancel =
  λb h. qNeg (b + h) + h
    ≡⟨ cong (λw. Q) (λw. w + h) (qNegAdd b h) ⟩ qNeg b + qNeg h + h
    ≡⟨ qAddAssoc (qNeg b) (qNeg h) h ⟩ qNeg b + (qNeg h + h)
    ≡⟨ cong (λw. Q) (λw. qNeg b + w) (qAddNegL h) ⟩ qNeg b + qZero
    ≡⟨ qAddZeroR (qNeg b) ⟩ qNeg b

-- a bound that holds with EVERY slack 1/(k+1) holds without slack.
-- Both halves are leQOfArch; the lower one first moves the ε across
-- the negation
bndOfArch : {b : Q} (d : Q) → ((k : ℕ) → Bnd (b + qInvNat k) d) → Bnd b d
  using (Rat.bound.Bnd.unfold)
bndOfArch =
  λb d h. (,)
    leQOfArch
      _
      _
      λk. transport
        λw. w ≤ d + qInvNat k
        {qNeg (b + qInvNat k) + qInvNat k}
        {qNeg b}
        qNegAddCancel
        leQPlusMono (qInvNat k) (h k .π₁)
    leQOfArch _ _ (λk. h k .π₂)

-- ===== the four-leg sum a triangle chain produces =====
-- ((a+b) + y) + (b+a) ≡ (a+a) + ((b+b) + y): the two outer indices
-- collect, the two inner ones collect, and the middle stays put
qFourSum : (a b y : Q) → a + b + y + (b + a) ≡ a + a + (b + b + y) using (Rat.Q.unfold)
qFourSum =
  λa b y. a + b + y + (b + a)
    ≡⟨ qAddAssoc (a + b) y (b + a) ⟩ a + b + (y + (b + a))
    ≡⟨ cong (λw. Q) (λw. a + b + w) (qAddComm y (b + a)) ⟩ a + b + (b + a + y)
    ≡⟨ sym _ _ (qAddAssoc (a + b) (b + a) y) ⟩ a + b + (b + a) + y
    ≡⟨ cong
      λw. Q
      λw. w + y
      trans _ _ _ (cong (λw. Q) (λw. a + b + w) (qAddComm b a)) (qPairSwap a b a b) ⟩
      a + a + (b + b) + y
    ≡⟨ qAddAssoc (a + a) (b + b) y ⟩ a + a + (b + b + y)

-- three copies sit under four
leQTripleQuad : {h : Q} → qZero ≤ h → h + (h + h) ≤ h + h + (h + h)
  using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold)
leQTripleQuad =
  λh nn. transport
    λw. w ≤ h + h + (h + h)
    qAddAssoc h h h
    leQPlusMonoL _ _ (h + h) (leQSelfAdd h nn)

-- ...so three quarter-fractions fit inside one: 3/(4k+4) ≤ 1/(k+1)
leQTripleInv : (k : ℕ)
  → qInvNat (dbl (dbl k)) + (qInvNat (dbl (dbl k)) + qInvNat (dbl (dbl k))) ≤ qInvNat k
  using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold)
leQTripleInv =
  λk. transport
    λw. qInvNat (dbl (dbl k)) + (qInvNat (dbl (dbl k)) + qInvNat (dbl (dbl k))) ≤ w
    trans _ _ _ (cong (λw. Q) (λw. w + w) (qInvHalf (dbl k))) (qInvHalf k)
    leQTripleQuad (leQZeroInvNat (dbl (dbl k)))

-- the converse of leQSubShift: a bound on the difference is a shifted ≤
leQAddShift : (a : Q) {b q : Q} → a + qNeg b ≤ q → a ≤ b + q
  using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold, Rat.Q.unfold)
leQAddShift = λa b q. transport (λw. NonNegS (sgnQ w)) (sym _ _ (qShiftEq a b q))

-- ===== ≤ is decidable, so its squash is faithful =====
--
-- A `quot-elim` landing in `(LeQ x y)` owes a well-definedness
-- proof between two order verdicts, and no `using` candidate can
-- supply it: a subsingleton lemma's type-index is not determined by
-- the two sides, so matching leaves it unsolved (E-1). Landing in the
-- SQUASH instead makes the descent free — proof irrelevance closes it
-- — and this recovers the datum, by deciding and refuting.
leQUnsquash : (x : Q) {y : Q} → ∥x ≤ y∥ → x ≤ y
  using (Core.id.Id.unfold,
    Core.prop.⊥.unfold,
    Rat.order.≤.unfold,
    Rat.order.NonNegS.unfold,
    Rat.Q.unfold)
leQUnsquash =
  λx y h. ⊎-elim
    nn. nn
    hneg. leQOfFalse (squash-elim h (le. ⋆ (nonNegNotNeg _ le hneg)))
    sgnCases (sgnQ (y + qNeg x))