Real.sqrt

-- THE SQUARE ROOT of a NONNEGATIVE real.
--
--   realSqrt : (x : Real) → (NonNegR x) → Real
--
-- No total √, and no truncation inside it. The witness is
-- Real.pos.NonNegR — x together with a POINTWISE NONNEGATIVE
-- representative, bracketed — and that is exactly what the floor
-- estimate needs, at every sample, with no clamping and no modulus.
--
-- Nonnegativity rather than positivity is the right hypothesis here.
-- √ never needs separation from zero; it needs its samples to be
-- nonnegative, and a nonnegative presentation says precisely that.
-- Strict positivity (Real.pos.PosR) would also do it — deepen the
-- sample by the modulus and p_j ≥ 1/(2(k+1)) — but it excludes 0,
-- which is in √'s domain. PosR is kept for division, where 0 really
-- is outside and the modulus really is needed.
--
-- On a nonnegative representative:
--
--   (√p)_n = qSqrtAt (p_{φ n}) (D n),  D n = 2n+1,  φ n = mulIdx (D n) (D n)
--
-- The approximation depth is DOUBLE the index and the sampling depth
-- is its SQUARE. Both are forced, and exactly:
--
--   * 1/(D n + 1) = 1/(2(n+1)), so two of them make 1/(n+1) — qInvHalf.
--     The comparison spends one on each side, and rBound m n has
--     exactly two to give.
--   * (φ n + 1) = (D n + 1)², so the gap between two samples of p,
--     scaled by (D m + 1)²(D n + 1)², is the natural
--     (D n + 1)² + (D m + 1)². That is the T fed to isqrt, and
--     sqSumStrict gives isqrt T + 1 ≤ (D n + 1) + (D m + 1), which is
--     precisely the remaining budget.
--
-- The quadratic sampling is the price of √ not being Lipschitz: its
-- modulus of continuity is √.
--
-- Regularity and well-definedness are instances of ONE estimate
-- (sqrtDirGen). The second is the obligation brElim charges for
-- reaching into data: any two nonnegative presentations of x give the
-- same root.

import Natural (+, *)
import Natural.order (≤)
import Natural.sqrt (isqrt, isqrtLtOfLt, sqSumStrict)
import Rat (Q, +, *, qNeg, qZero, qOne, qMulZeroL, qAddComm, qAddAssoc, qMulComm, qMulAssoc, qMulOneL, qMulOneR, qDistribR)
import Rat.order (≤, leQRefl, leQTrans, leQOfEq, leQMulMono, leQPlusMonoL)
import Rat.bound (Bnd, bndOfBothLe, bndSubSym, leQSelfAddL, leQAdd)
import Rat.half (dbl, qInvHalf, leQZeroInvNat)
import Rat.arch (leQSubShift)
import Rat.max (leQAddOfBnd, qMax, qMaxSelf)
import Rat.abs (leQZeroMul)
import Rat.nat (qOfNat, qOfNatAdd, qOfNatMul, qOfNatZero, leQOfNat)
import Rat.ceil (leQZeroNat, qFloor)
import Rat.sqrt (sqNat, qSqrtAt, qMulInvNat, qInvNatMulIdx, leQSqrtStep, qMulSwap3, qMulLeftComm)
import Natural.sqrt (isqrtAux)
import Real (qInvNat, rBound, leQZeroBound, Regular, RSeq, REq, Real, constReg, realZero, realOfQ)
import Real.neg (seqOf, regOf, regBnd, bndReg, reqOf, rBoundSym, realEqOfREq)
import Real.mul (mulIdx)
import Real.ring (leQInvIdx)
import Real.pos (NonNegR, NonNegPayload, nonNegMk, nnRep, nnAt, nnRepEq, reqOfClassEq)
import Core.bracket (Br, br, brElim, brIsProp)
import Real.seq (rseqEq)
import Real.order (≤)
import Real.eq (reqTrans)
import Core.equality (trans, sym, cong, transport, transportP)
import Core.prelude (funext)

sqrtDepth : ℕ → ℕ
sqrtDepth = λk. dbl k

sqrtIdx : ℕ → ℕ
sqrtIdx = λk. mulIdx (dbl k) (dbl k)

sqrtT : ℕ → ℕ → ℕ
sqrtT = λm n. sqNat (sqrtDepth n) + sqNat (sqrtDepth m)

-- ===== the scaling is exact =====
qMulSq : (x y : Q) → x * y * (x * y) ≡ x * x * (y * y)
qMulSq =
  λx y. x * y * (x * y)
    ≡⟨ qMulAssoc x y (x * y) ⟩ x * (y * (x * y))
    ≡⟨ cong (λw. Q) (λw. x * w) (qMulLeftComm y x y) ⟩ x * (x * (y * y))
    ≡⟨ sym _ _ (qMulAssoc x x (y * y)) ⟩ x * x * (y * y)

invNatOne : (a : ℕ) → qInvNat a * qOfNat (S a) ≡ qOne
invNatOne = λa. trans _ _ _ (qMulComm (qInvNat a) (qOfNat (S a))) qMulInvNat

qOfNatSq : (a : ℕ) → qOfNat (sqNat a) ≡ qOfNat (S a) * qOfNat (S a) using (Rat.sqrt.sqNat.eq)
qOfNatSq = λa. sym _ (qOfNat (S a * S a)) (qOfNatMul (S a) (S a))

-- 1/(D+1)² · (D+1)² is one
invSqCancel : (a : ℕ) → qInvNat (mulIdx a a) * qOfNat (sqNat a) ≡ qOne
invSqCancel =
  λa. qInvNat (mulIdx a a) * qOfNat (sqNat a)
    ≡⟨ cong
      λw. Q
      λw. w * qOfNat (sqNat a)
      {qInvNat (mulIdx a a)}
      {qInvNat a * qInvNat a}
      qInvNatMulIdx ⟩
      qInvNat a * qInvNat a * qOfNat (sqNat a)
    ≡⟨ cong (λw. Q) (λw. qInvNat a * qInvNat a * w) (qOfNatSq a) ⟩
      qInvNat a * qInvNat a * (qOfNat (S a) * qOfNat (S a))
    ≡⟨ sym _ _ (qMulSq (qInvNat a) (qOfNat (S a))) ⟩
      qInvNat a * qOfNat (S a) * (qInvNat a * qOfNat (S a))
    ≡⟨ cong (λw. Q) (λw. w * (qInvNat a * qOfNat (S a))) (invNatOne a) ⟩
      qOne * (qInvNat a * qOfNat (S a))
    ≡⟨ qMulOneL (qInvNat a * qOfNat (S a)) ⟩ qInvNat a * qOfNat (S a)
    ≡⟨ invNatOne a ⟩ qOne

-- the gap between two samples, scaled, is exactly the natural T
scaleEq : (a b : ℕ)
  → rBound (mulIdx a a) (mulIdx b b) * qOfNat (sqNat a) * qOfNat (sqNat b)
    ≡ qOfNat (sqNat b + sqNat a)
scaleEq =
  λa b. (qInvNat (mulIdx a a) + qInvNat (mulIdx b b)) * qOfNat (sqNat a) * qOfNat (sqNat b)
    ≡⟨ cong
      λw. Q
      λw. w * qOfNat (sqNat b)
      qDistribR (qOfNat (sqNat a)) (qInvNat (mulIdx a a)) (qInvNat (mulIdx b b)) ⟩
      (qInvNat (mulIdx a a) * qOfNat (sqNat a) + qInvNat (mulIdx b b) * qOfNat (sqNat a))
        * qOfNat (sqNat b)
    ≡⟨ qDistribR
      qOfNat (sqNat b)
      qInvNat (mulIdx a a) * qOfNat (sqNat a)
      qInvNat (mulIdx b b) * qOfNat (sqNat a) ⟩
      qInvNat (mulIdx a a) * qOfNat (sqNat a) * qOfNat (sqNat b)
        + qInvNat (mulIdx b b) * qOfNat (sqNat a) * qOfNat (sqNat b)
    ≡⟨ cong
      λw. Q
      λw. w * qOfNat (sqNat b) + qInvNat (mulIdx b b) * qOfNat (sqNat a) * qOfNat (sqNat b)
      invSqCancel a ⟩
      qOne * qOfNat (sqNat b) + qInvNat (mulIdx b b) * qOfNat (sqNat a) * qOfNat (sqNat b)
    ≡⟨ cong
      λw. Q
      λw. w + qInvNat (mulIdx b b) * qOfNat (sqNat a) * qOfNat (sqNat b)
      qMulOneL (qOfNat (sqNat b)) ⟩
      qOfNat (sqNat b) + qInvNat (mulIdx b b) * qOfNat (sqNat a) * qOfNat (sqNat b)
    ≡⟨ cong
      λw. Q
      λw. qOfNat (sqNat b) + w
      qMulSwap3 (qInvNat (mulIdx b b)) (qOfNat (sqNat a)) (qOfNat (sqNat b)) ⟩
      qOfNat (sqNat b) + qInvNat (mulIdx b b) * qOfNat (sqNat b) * qOfNat (sqNat a)
    ≡⟨ cong (λw. Q) (λw. qOfNat (sqNat b) + w * qOfNat (sqNat a)) (invSqCancel b) ⟩
      qOfNat (sqNat b) + qOne * qOfNat (sqNat a)
    ≡⟨ cong (λw. Q) (λw. qOfNat (sqNat b) + w) (qMulOneL (qOfNat (sqNat a))) ⟩
      qOfNat (sqNat b) + qOfNat (sqNat a)
    ≡⟨ qOfNatAdd (sqNat b) (sqNat a) ⟩ qOfNat (sqNat b + sqNat a)

-- ===== the slack fits =====
cancelMid : (D : ℕ) (e : Q) → qOfNat (S D) * (e * qInvNat D) ≡ e
cancelMid =
  λD e. qOfNat (S D) * (e * qInvNat D)
    ≡⟨ qMulLeftComm (qOfNat (S D)) e (qInvNat D) ⟩ e * (qOfNat (S D) * qInvNat D)
    ≡⟨ cong (λw. Q) (λw. e * w) {qOfNat (S D) * qInvNat D} {qOne} qMulInvNat ⟩ e * qOne
    ≡⟨ qMulOneR e ⟩ e

-- ((Dn+1) + (Dm+1))·(1/(Dm+1)·1/(Dn+1)) is 1/(Dm+1) + 1/(Dn+1)
slackEq : {Dm Dn : ℕ} → qOfNat (S Dn + S Dm) * (qInvNat Dm * qInvNat Dn) ≡ qInvNat Dm + qInvNat Dn
slackEq =
  λDm Dn. qOfNat (S Dn + S Dm) * (qInvNat Dm * qInvNat Dn)
    ≡⟨ cong (λw. Q) (λw. w * (qInvNat Dm * qInvNat Dn)) (sym _ _ (qOfNatAdd (S Dn) (S Dm))) ⟩
      (qOfNat (S Dn) + qOfNat (S Dm)) * (qInvNat Dm * qInvNat Dn)
    ≡⟨ qDistribR (qInvNat Dm * qInvNat Dn) (qOfNat (S Dn)) (qOfNat (S Dm)) ⟩
      qOfNat (S Dn) * (qInvNat Dm * qInvNat Dn) + qOfNat (S Dm) * (qInvNat Dm * qInvNat Dn)
    ≡⟨ cong
      λw. Q
      λw. w + qOfNat (S Dm) * (qInvNat Dm * qInvNat Dn)
      cancelMid Dn (qInvNat Dm) ⟩
      qInvNat Dm + qOfNat (S Dm) * (qInvNat Dm * qInvNat Dn)
    ≡⟨ cong (λw. Q) (λw. qInvNat Dm + qOfNat (S Dm) * w) (qMulComm (qInvNat Dm) (qInvNat Dn)) ⟩
      qInvNat Dm + qOfNat (S Dm) * (qInvNat Dn * qInvNat Dm)
    ≡⟨ cong (λw. Q) (λw. qInvNat Dm + w) (cancelMid Dm (qInvNat Dn)) ⟩ qInvNat Dm + qInvNat Dn

sqrtSlack : (m n : ℕ)
  → qOfNat (S (isqrt (sqrtT m n))) * (qInvNat (sqrtDepth m) * qInvNat (sqrtDepth n))
    ≤ qInvNat (sqrtDepth m) + qInvNat (sqrtDepth n)
  using (Rat.sqrt.sqNat.eq, sqrtT.eq)
sqrtSlack =
  λm n. transport
    λw. qOfNat (S (isqrt (sqrtT m n))) * (qInvNat (sqrtDepth m) * qInvNat (sqrtDepth n)) ≤ w
    {qOfNat (S (sqrtDepth n) + S (sqrtDepth m)) * (qInvNat (sqrtDepth m) * qInvNat (sqrtDepth n))}
    {qInvNat (sqrtDepth m) + qInvNat (sqrtDepth n)}
    slackEq
    leQMulMono
      _
      _
      leQOfNat (isqrtLtOfLt (sqrtT m n) (sqSumStrict (sqrtDepth n) (sqrtDepth m)))
      leQZeroMul (leQZeroInvNat (sqrtDepth m)) (leQZeroInvNat (sqrtDepth n))

-- y + (x + y) ≤ (x + x) + (y + y), for nonnegative x
slackFits : {x y : Q} → qZero ≤ x → y + (x + y) ≤ x + x + (y + y)
slackFits =
  λx y hx. transport
    λw. w ≤ x + x + (y + y)
    sym
      _
      _
      trans
        _
        _
        _
        sym _ _ (qAddAssoc y x y)
        trans _ _ _ (cong (λw. Q) (λw. w + y) (qAddComm y x)) (qAddAssoc x y y)
    transport
      {Q}
      λw. x + (y + y) ≤ w
      {x + (x + (y + y))}
      sym _ _ (qAddAssoc x x (y + y))
      leQSelfAddL hx

-- ===== regularity =====
rBoundHalves : {m n : ℕ}
  → qInvNat (sqrtDepth m) + qInvNat (sqrtDepth m) + (qInvNat (sqrtDepth n) + qInvNat (sqrtDepth n))
    ≡ rBound m n
  using (Real.rBound.eq, sqrtDepth.eq)
rBoundHalves =
  λm n. trans
    qInvNat (dbl m) + qInvNat (dbl m) + (qInvNat (dbl n) + qInvNat (dbl n))
    _
    qInvNat m + qInvNat n
    cong (λw. Q) (λw. w + (qInvNat (dbl n) + qInvNat (dbl n))) (qInvHalf m)
    cong (λw. Q) (λw. qInvNat m + w) (qInvHalf n)

-- ===== one comparison, three uses =====
--
-- Regularity, well-definedness in the representative, and
-- independence of the modulus are the SAME estimate: two samples, of
-- possibly different representatives, each at least as deep as φ of
-- its index. Stating it once with the sample indices abstract covers
-- all three, and is why the modulus costs so little.
sqrtDirGen : {p : RSeq}
  (p' : RSeq)
  {a b m n : ℕ}
  → qZero ≤ seqOf p a
    → qInvNat a ≤ qInvNat (sqrtIdx m)
      → qInvNat b ≤ qInvNat (sqrtIdx n)
        → Bnd (rBound a b) (seqOf p a + qNeg (seqOf p' b))
          → qSqrtAt (seqOf p a) (sqrtDepth m) ≤ qSqrtAt (seqOf p' b) (sqrtDepth n) + rBound m n
  using (Real.rBound.eq, sqrtDepth.eq, sqrtIdx.eq, sqrtT.eq)
sqrtDirGen =
  λp p' a b m n nn da db gap. leQTrans
    _
    _
    _
    leQSqrtStep
      _
      nn
      leQAddOfBnd gap
      leQTrans
        _
        _
        _
        leQMulMono
          _
          _
          leQMulMono
            rBound a b
            rBound (sqrtIdx m) (sqrtIdx n)
            leQAdd _ _ _ _ da db
            leQZeroNat (sqNat (sqrtDepth m))
          leQZeroNat (sqNat (sqrtDepth n))
        leQOfEq
          rBound (sqrtIdx m) (sqrtIdx n) * qOfNat (sqNat (sqrtDepth m))
            * qOfNat (sqNat (sqrtDepth n))
          qOfNat (sqrtT m n)
          scaleEq (sqrtDepth m) (sqrtDepth n)
    leQTrans
      _
      _
      _
      leQPlusMonoL _ _ (qSqrtAt (seqOf p' b) (sqrtDepth n) + qInvNat (sqrtDepth n)) (sqrtSlack m n)
      transport
        λw. w ≤ qSqrtAt (seqOf p' b) (sqrtDepth n) + rBound m n
        sym
          _
          _
          qAddAssoc
            qSqrtAt (seqOf p' b) (sqrtDepth n)
            qInvNat (sqrtDepth n)
            qInvNat (sqrtDepth m) + qInvNat (sqrtDepth n)
        leQPlusMonoL
          _
          _
          qSqrtAt (seqOf p' b) (sqrtDepth n)
          transport
            {Q}
            λw. qInvNat (sqrtDepth n) + (qInvNat (sqrtDepth m) + qInvNat (sqrtDepth n)) ≤ w
            {qInvNat (sqrtDepth m) + qInvNat (sqrtDepth m)
              + (qInvNat (sqrtDepth n) + qInvNat (sqrtDepth n))}
            {rBound m n}
            rBoundHalves
            slackFits (leQZeroInvNat (sqrtDepth m))

-- ===== use 1: regularity =====
sqrtSeqNN : RSeq → ℕ → Q
sqrtSeqNN = λp n. qSqrtAt (seqOf p (sqrtIdx n)) (sqrtDepth n)

sqrtRegAtNN : (p : RSeq)
  (nn : (n : ℕ) → qZero ≤ seqOf p n)
  (m n : ℕ)
  → Bnd (rBound m n) (sqrtSeqNN p m + qNeg (sqrtSeqNN p n))
  using (sqrtSeqNN.eq)
sqrtRegAtNN =
  λp nn m n. bndOfBothLe
    _
    _
    leQSubShift
      sqrtSeqNN p m
      sqrtSeqNN p n
      sqrtDirGen
        _
        nn (sqrtIdx m)
        leQRefl (qInvNat (sqrtIdx m))
        leQRefl (qInvNat (sqrtIdx n))
        regBnd _ (regOf p) (sqrtIdx m) (sqrtIdx n)
    transport
      λw. sqrtSeqNN p n + qNeg (sqrtSeqNN p m) ≤ w
      rBoundSym n m
      leQSubShift
        sqrtSeqNN p n
        sqrtSeqNN p m
        sqrtDirGen
          _
          nn (sqrtIdx n)
          leQRefl (qInvNat (sqrtIdx n))
          leQRefl (qInvNat (sqrtIdx m))
          regBnd _ (regOf p) (sqrtIdx n) (sqrtIdx m)

rSqrtNN : (p : RSeq) → ((n : ℕ) → qZero ≤ seqOf p n) → RSeq using (Real.RSeq.unfold)
rSqrtNN = λp nn. sqrtSeqNN p, bndReg (sqrtRegAtNN _ nn)

-- ===== use 2: any two nonnegative presentations agree =====
--
-- This is the whole of brElim's obligation now. With the modulus gone
-- there is nothing else to be independent of.
rSqrtWDNN : {p p' : RSeq}
  (nn : (n : ℕ) → qZero ≤ seqOf p n)
  (nn' : (n : ℕ) → qZero ≤ seqOf p' n)
  → REq p p' → REq (rSqrtNN _ nn) (rSqrtNN _ nn')
  using (Real.REq.unfold,
    Real.RSeq.unfold,
    Real.Regular.unfold,
    Rat.bound.Bnd.unfold,
    Real.neg.seqOf.eq,
    rSqrtNN.eq,
    sqrtSeqNN.eq)
rSqrtWDNN =
  λp p' nn nn' h. squash-elim
    h
    u. reqOf
      _
      _
      λn. bndOfBothLe
        sqrtSeqNN p n
        sqrtSeqNN p' n
        leQSubShift
          sqrtSeqNN p n
          sqrtSeqNN p' n
          sqrtDirGen
            p'
            nn (sqrtIdx n)
            leQRefl (qInvNat (sqrtIdx n))
            leQRefl (qInvNat (sqrtIdx n))
            u (sqrtIdx n)
        leQSubShift
          sqrtSeqNN p' n
          sqrtSeqNN p n
          sqrtDirGen
            _
            nn' (sqrtIdx n)
            leQRefl (qInvNat (sqrtIdx n))
            leQRefl (qInvNat (sqrtIdx n))
            bndSubSym
              rBound (sqrtIdx n) (sqrtIdx n)
              seqOf p (sqrtIdx n)
              seqOf p' (sqrtIdx n)
              u (sqrtIdx n)

-- ===== the descent =====
sqrtFromNN : (x : Real) → NonNegPayload x → Real
  using (Real.Real.unfold, Real.RSeq.unfold, Real.Regular.unfold)
sqrtFromNN = λx d. class (rSqrtNN _ (nnAt _ d))

sqrtNNConst : (x : Real) (d d' : NonNegPayload x) → sqrtFromNN _ d ≡ sqrtFromNN _ d'
  using (Real.Real.unfold, Real.RSeq.unfold, Real.Regular.unfold, sqrtFromNN.eq)
sqrtNNConst =
  λx d d'. realEqOfREq
    _
    _
    rSqrtWDNN
      nnAt _ d
      nnAt _ d'
      reqOfClassEq (trans _ _ _ (nnRepEq _ d) (sym _ _ (nnRepEq _ d')))

realSqrt : (x : Real) → NonNegR x → Real using (NonNegR.eq)
realSqrt = λx w. brElim (sqrtFromNN x) (sqrtNNConst x) w

realSqrtRep : {x : Real} {d : NonNegPayload x} → realSqrt _ (br d) ≡ class (rSqrtNN _ (nnAt _ d))
  using (Real.Real.unfold,
    Real.RSeq.unfold,
    Real.Regular.unfold,
    NonNegR.eq,
    Core.bracket.br.eq,
    Core.bracket.brElim.eq,
    sqrtFromNN.eq,
    Real.sqrt.realSqrt.eq)
realSqrtRep = λx d. ⋆

-- ===== it computes: √0 = 0 =====
--
-- Statable again, because 0 is in the domain: it has a nonnegative
-- presentation (the zero sequence) even though it has no modulus.
-- Stated for an ARBITRARY witness — brIsProp makes them all equal, so
-- there is nothing to choose.
qFloorZero : qFloor qZero ≡ Z
  using (Rat.ceil.qFloor.eq,
    Rat.qZero.eq,
    Rat.qcls.eq,
    Rat.frac.ratZero.eq,
    Rat.frac.ratOfInt.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.den.eq,
    Int.intZero.eq,
    Int.abs.intMag.eq,
    Int.abs.magPair.eq,
    Int.abs.nzMag.eq,
    Rat.frac.nzOne.eq,
    Rat.frac.nzPos.eq,
    Natural.div.divN.eq,
    Natural.div.dmAux.eq,
    Natural.div.natCase.eq,
    Natural.more.∸.eq,
    Natural.+.eq)
qFloorZero = ⋆

isqrtZero : isqrt Z ≡ Z using (Natural.sqrt.isqrt.eq, Natural.sqrt.isqrtAux.eq)
isqrtZero = ⋆

qSqrtAtZero : {D : ℕ} → qSqrtAt qZero D ≡ qZero
  using (Rat.sqrt.qSqrtAt.eq, Rat.sqrt.qSqrtNum.eq, Rat.sqrt.qFl.eq, Rat.sqrt.qScaled.eq)
qSqrtAtZero =
  λD. trans
    qOfNat (isqrt (qFloor (qZero * qOfNat (sqNat D)))) * qInvNat D
    _
    _
    cong
      λw. Q
      λw. qOfNat w * qInvNat D
      trans
        _
        _
        _
        cong
          λw. ℕ
          λw. isqrt w
          trans
            _
            _
            _
            cong (λw. ℕ) (λw. qFloor w) {qZero * qOfNat (sqNat D)} {qZero} qMulZeroL
            qFloorZero
        isqrtZero
    trans _ _ qZero (cong (λw. Q) (λw. w * qInvNat D) qOfNatZero) qMulZeroL

zeroRep : RSeq using (Real.RSeq.unfold)
zeroRep = (λn. qZero), constReg

zeroNN : (n : ℕ) → qZero ≤ seqOf zeroRep n using (Real.RSeq.unfold, zeroRep.eq, Real.neg.seqOf.eq)
zeroNN = λn. leQRefl qZero

rSqrtZeroSeq : rSqrtNN _ zeroNN ≡ zeroRep
  using (Real.RSeq.unfold, rSqrtNN.eq, sqrtSeqNN.eq, zeroRep.eq, Real.neg.seqOf.eq)
rSqrtZeroSeq = rseqEq (λn. qSqrtAtZero)

clsZeroRep : class zeroRep ≡ realZero
  using (Real.Real.unfold,
    Real.RSeq.unfold,
    Real.Regular.unfold,
    Real.realZero.eq,
    Real.realOfQ.eq,
    zeroRep.eq)
clsZeroRep = ⋆

realSqrtZero : (w : NonNegR realZero) → realSqrt _ w ≡ realZero
  using (Real.Real.unfold,
    Real.RSeq.unfold,
    Real.Regular.unfold,
    NonNegR.eq,
    Core.bracket.Br.unfold,
    Core.bracket.br.eq)
realSqrtZero =
  λw. quot-elim
    d. trans
      realSqrt _ (br d)
      _
      _
      realSqrtRep
      trans
        _
        _
        _
        realEqOfREq
          _
          _
          rSqrtWDNN
            nnAt _ d
            zeroNN
            reqOfClassEq (trans _ _ _ (nnRepEq _ d) (sym _ _ clsZeroRep))
        trans {Real} _ _ _ (cong (λw. Real) (λw. class w) rSqrtZeroSeq) clsZeroRep
    w