Real.ring

-- THE RING LAWS for ℝ, on top of Real/mul.nova's product.
--
-- The two unit laws split cleanly. `u · 0 = 0` is POINTWISE: whatever
-- depth the product samples at, every value is x·0 = 0, so the two
-- sequences are literally equal and rseqEq closes it. `u · 1 = u` is
-- not pointwise — the product still samples at depth φ m ≥ m, so it
-- is p DEEPENED, and a deepening is only REq to the original. That is
-- the one estimate this half of the file needs, and it comes down to
--
--   1/(φ m + 1) ≤ 1/(m + 1)   whenever   φ m = mulIdx c m
--
-- which Real/mul.nova already proved as an EQUATION: the factor S c
-- turns 1/(φ m + 1) into 1/(m + 1) exactly (qMulInvIdx). Multiplying a
-- nonnegative by S c ≥ 1 only grows it, so the inequality follows
-- without any new arithmetic on fractions.
-- ===== the two constant representatives =====

import Natural (+, *)
import Rat (Q, +, *, qNeg, qZero, qOne, qAddComm, qAddAssoc, qMulComm, qMulAssoc, qMulZeroR, qMulOneR, qMulOneL, qDistribL, qDistribR)
import Rat.order (≤, leQPlusMono, leQPlusMonoL, leQTrans, qSubSplit, qPairSwap, qNegAdd)
import Rat.bound (Bnd, bndAdd, bndEq, bndEqB, bndWeaken, bndVia, leQAdd, leQSelfAdd, leQSelfAddL)
import Rat.abs (bndMul, leQZeroMul)
import Rat.nat (qOfNat, qOfNatAdd, qOfNatMul, qOfNatOne, qOfNatSuc, qMulSucNat)
import Rat.ceil (leQZeroNat)
import Rat.arch (bndOfArch)
import Rat.half (dbl, leQZeroInvNat, leQInvDbl)
import Real (qInvNat, rBound, leQZeroBound, Regular, RSeq, REq, Real, constReg, realOfQ, realZero, realOne)
import Real.neg (seqOf, regOf, regBnd, bndReg, reqOf, realEqOfREq, realEqOfPointwise, realNeg)
import Real.seq (rseqEq, realEqOfSeqEq)
import Real.mul (mulIdx, mulPred, mulSeq, rMul, qMulInvIdx, qRearr5, bndMulSub, qMulSumBound, bndMulSubQ, *, realMulCls, realMulComm)
import Real.add (rAdd, +, realAddCls, realAddComm, realAddNegR)
import Real.group (realAddGroup, realNegUnique)
import Algebra.ring (IsCommRing)
import Core.id (eqToId)
import Real.bound (seqBound, bndSeqBound, seqBoundPos)
import Core.equality (trans, sym, cong, transport)

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

rOne : RSeq using (Real.RSeq.unfold)
rOne = (λn. qOne), constReg

-- ===== u · 0 = 0, pointwise =====
rMulZeroR : {p : RSeq} → rMul p rZero ≡ rZero
  using (rZero.eq, Real.mul.mulSeq.eq, Real.mul.rMul.eq, Real.neg.seqOf.eq)
rMulZeroR = λp. rseqEq (λn. qMulZeroR (seqOf p (mulIdx (mulPred p rZero) n)))

realMulZeroR : {u : Real} → u * realZero ≡ realZero
  using (rZero.eq, Real.Real.unfold, Real.realOfQ.eq, Real.realZero.eq)
realMulZeroR =
  λu. quot-elim
    p. trans
      _
      class (rMul p rZero)
      _
      realMulCls rZero
      cong (λw. Real) (λw. class w) {rMul p rZero} {rZero} rMulZeroR
    u

realMulZeroL : {u : Real} → realZero * u ≡ realZero
realMulZeroL = λu. trans _ _ _ (realMulComm realZero u) realMulZeroR

-- ===== the deepening inequality =====
-- multiplying a nonnegative by S c ≥ 1 only grows it
leQSelfMulNat : {c : ℕ} {x : Q} → qZero ≤ x → x ≤ qOfNat (S c) * x
leQSelfMulNat =
  λc x hx. transport
    {Q}
    λw. x ≤ w
    {qOfNat c * x + x}
    sym _ _ (qMulSucNat c x)
    leQSelfAddL (leQZeroMul (leQZeroNat c) hx)

-- ...so sampling deeper gives a smaller harmonic bound. The EQUATION
-- qMulInvIdx is what makes this free: the factor is exact, so the
-- inequality is just "times S c is not smaller".
leQInvIdx : (c m : ℕ) → qInvNat (mulIdx c m) ≤ qInvNat m
leQInvIdx =
  λc m. transport
    {Q}
    λw. qInvNat (mulIdx c m) ≤ w
    {qOfNat (S c) * qInvNat (mulIdx c m)}
    {qInvNat m}
    qMulInvIdx
    leQSelfMulNat (leQZeroInvNat (mulIdx c m))

leQRBoundIdx : (c m : ℕ) → rBound (mulIdx c m) m ≤ rBound m m using (Real.rBound.eq)
leQRBoundIdx = λc m. leQPlusMono (qInvNat m) (leQInvIdx c m)

-- ===== u · 1 = u =====
-- the product's value at the deep index IS the original's, since the
-- second factor is 1 at every index
mulOneAt : (x y : Q) → x + qNeg y ≡ x * qOne + qNeg y
mulOneAt = λx y. cong (λw. Q) (λw. w + qNeg y) (sym _ _ (qMulOneR x))

rMulOneWD : (p : RSeq) → REq (rMul p rOne) p
  using (rOne.eq, Real.mul.mulSeq.eq, Real.mul.rMul.eq, Real.neg.seqOf.eq)
rMulOneWD =
  λp. reqOf
    _
    _
    λn. bndWeaken
      _
      _
      mulSeq p rOne n + qNeg (seqOf p n)
      leQRBoundIdx (mulPred p rOne) n
      bndEq
        seqOf p (mulIdx (mulPred p rOne) n) + qNeg (seqOf p n)
        mulSeq p rOne n + qNeg (seqOf p n)
        mulOneAt (seqOf p (mulIdx (mulPred p rOne) n)) (seqOf p n)
        regBnd _ (regOf p) (mulIdx (mulPred p rOne) n) n

realMulOneR : (u : Real) → u * realOne ≡ u
  using (rOne.eq, Real.Real.unfold, Real.realOfQ.eq, Real.realOne.eq)
realMulOneR =
  λu. quot-elim
    p. trans _ (class (rMul p rOne)) _ (realMulCls rOne) (realEqOfREq _ _ (rMulOneWD p))
    u

realMulOneL : (u : Real) → realOne * u ≡ u
realMulOneL = λu. trans _ _ _ (realMulComm realOne u) (realMulOneR u)

-- ===== the closeness criterion =====
--
-- THE tool for the remaining laws. Two representatives name the same
-- real as soon as they are within K·rBound n n at every index — for
-- ANY constant K, not just K = 1. That is much weaker than REq itself
-- and it is what a ring law can actually deliver: the two sides sample
-- at different depths, so the honest estimate carries a constant built
-- from the factors' bounds.
--
-- The slack is removed once, here, instead of once per law. Chaining
-- through a deep index N gives
--
--   |u_n − v_n| ≤ rBound n N + K·rBound N N + rBound N n
--               = rBound n n + (2K + 2)/(N + 1)
--
-- and (2K + 2)/(N + 1) is EXACTLY 1/(l + 1) at N = mulIdx (S (K+K)) l,
-- because the factor S (S (K+K)) is 2K + 2 and qMulInvIdx makes it exact.
-- Written S (K + K) rather than dbl K on purpose: citing dbl.eq to see
-- through the abbreviation unfolds the goal past the point where
-- qMulSucNat still matches (the poison rule).
-- No inequality between fractions is needed anywhere — only that one
-- equation.
kkY : (K : ℕ) (y : Q) → qOfNat (K + K) * y ≡ qOfNat K * (y + y)
kkY =
  λK y. qOfNat (K + K) * y
    ≡⟨ cong (λv. Q) (λv. v * y) (sym _ _ (qOfNatAdd K K)) ⟩ (qOfNat K + qOfNat K) * y
    ≡⟨ qDistribR y (qOfNat K) (qOfNat K) ⟩ qOfNat K * y + qOfNat K * y
    ≡⟨ sym _ _ (qDistribL (qOfNat K) y y) ⟩ qOfNat K * (y + y)

-- y + (K·(y + y) + y) is (2K + 2)·y
twoKTwo : (K : ℕ) (y : Q) → y + (qOfNat K * (y + y) + y) ≡ qOfNat (S (S (K + K))) * y
twoKTwo =
  λK y. y + (qOfNat K * (y + y) + y)
    ≡⟨ qAddComm y (qOfNat K * (y + y) + y) ⟩ qOfNat K * (y + y) + y + y
    ≡⟨ cong (λv. Q) (λv. v + y + y) (sym _ _ (kkY K y)) ⟩ qOfNat (K + K) * y + y + y
    ≡⟨ cong (λv. Q) (λv. v + y) (sym _ _ (qMulSucNat (K + K) y)) ⟩ qOfNat (S (K + K)) * y + y
    ≡⟨ sym _ _ (qMulSucNat (S (K + K)) y) ⟩ qOfNat (S (S (K + K))) * y

-- (x + y) + (K·(y + y) + (y + x)) ≡ (x + x) + w, given w = (2K + 2)·y.
-- The factor equation is an ARGUMENT: at the call site w is 1/(l + 1)
-- and the equation is qMulInvIdx, so the deep index never has to be
-- looked at (B-16).
closeBoundEq : (x : Q)
  {y : Q}
  {K : ℕ}
  {w : Q}
  → (qOfNat (S (S (K + K))) * y ≡ w) → x + y + (qOfNat K * (y + y) + (y + x)) ≡ x + x + w
closeBoundEq =
  λx y K w hw. x + y + (qOfNat K * (y + y) + (y + x))
    ≡⟨ qRearr5 x y (qOfNat K * (y + y)) y ⟩ x + x + (y + (qOfNat K * (y + y) + y))
    ≡⟨ cong (λv. Q) (λv. x + x + v) (twoKTwo K y) ⟩ x + x + qOfNat (S (S (K + K))) * y
    ≡⟨ cong (λv. Q) (λv. x + x + v) hw ⟩ x + x + w

-- the three-leg chain, abstract in the sequences and the deep index
closeStepGen : (f g : ℕ → Q)
  (K n N : ℕ)
  (w : Q)
  → Bnd (rBound n N) (f n + qNeg (f N))
    → Bnd (qOfNat K * rBound N N) (f N + qNeg (g N))
      → Bnd (rBound N n) (g N + qNeg (g n))
        → (qOfNat (S (S (K + K))) * qInvNat N ≡ w) → Bnd (rBound n n + w) (f n + qNeg (g n))
  using (Real.rBound.eq)
closeStepGen =
  λf g K n N w h1 h2 h3 hw. bndEqB
    rBound n N + (qOfNat K * rBound N N + rBound N n)
    _
    _
    closeBoundEq (qInvNat n) hw
    bndVia _ _ _ _ _ h1 (bndVia _ _ _ _ _ h2 h3)

reqOfClose : {u v : RSeq}
  (K : ℕ)
  → ((n : ℕ) → Bnd (qOfNat K * rBound n n) (seqOf u n + qNeg (seqOf v n))) → REq u v
reqOfClose =
  λu v K h. reqOf
    _
    _
    λn. bndOfArch
      seqOf u n + qNeg (seqOf v n)
      λl. closeStepGen
        seqOf u
        seqOf v
        _
        _
        _
        qInvNat l
        regBnd _ (regOf u) n (mulIdx (S (K + K)) l)
        h (mulIdx (S (K + K)) l)
        regBnd _ (regOf v) (mulIdx (S (K + K)) l) n
        qMulInvIdx

-- ===== distributivity =====
--
-- With reqOfClose the law is a POINTWISE estimate and nothing more.
-- At index m the two sides read
--
--   left   =  p_i · (q_{2i} + r_{2i})
--   right  =  p_j · q_j  +  p_k · r_k
--
-- with i, 2i, j, k four different depths, all of them at least m.
-- Split the difference into two product-differences, bound each by
-- bndMulSub at the COMMON modulus rBound m m, and add. The constant
-- that comes out is (A + B) + (A + C), which is exactly what
-- reqOfClose is willing to absorb.
qSubPair : (a b c d : Q) → a + qNeg c + (b + qNeg d) ≡ a + b + qNeg (c + d)
qSubPair =
  λa b c d. a + qNeg c + (b + qNeg d)
    ≡⟨ qPairSwap a (qNeg c) b (qNeg d) ⟩ a + b + (qNeg c + qNeg d)
    ≡⟨ cong (λv. Q) (λv. a + b + v) (sym _ _ (qNegAdd c d)) ⟩ a + b + qNeg (c + d)

-- two samples of one regular sequence, both at least as deep as m,
-- differ by at most rBound m m
bndDeep : (f : ℕ → Q)
  → ((a b : ℕ) → Bnd (rBound a b) (f a + qNeg (f b)))
    → (a b m : ℕ)
      → qInvNat a ≤ qInvNat m → qInvNat b ≤ qInvNat m → Bnd (rBound m m) (f a + qNeg (f b))
  using (Real.rBound.eq)
bndDeep = λf hf a b m ha hb. bndWeaken (rBound a b) _ _ (leQAdd _ _ _ _ ha hb) (hf a b)

distribStepGen : (f g h : ℕ → Q)
  (A B C m i t j k : ℕ)
  → ((a : ℕ) → Bnd (qOfNat A) (f a))
    → ((a : ℕ) → Bnd (qOfNat B) (g a))
      → ((a : ℕ) → Bnd (qOfNat C) (h a))
        → ((a b : ℕ) → Bnd (rBound a b) (f a + qNeg (f b)))
          → ((a b : ℕ) → Bnd (rBound a b) (g a + qNeg (g b)))
            → ((a b : ℕ) → Bnd (rBound a b) (h a + qNeg (h b)))
              → qInvNat i ≤ qInvNat m
                → qInvNat t ≤ qInvNat m
                  → qInvNat j ≤ qInvNat m
                    → qInvNat k ≤ qInvNat m
                      → qZero ≤ qOfNat A
                        → qZero ≤ qOfNat B
                          → qZero ≤ qOfNat C
                            → Bnd
                              qOfNat (A + B + (A + C)) * rBound m m
                              f i * (g t + h t) + qNeg (f j * g j + f k * h k)
distribStepGen =
  λf g h A B C m i t j k hfB hgB hhB hfR hgR hhR di dt dj dk hA hB hC. bndEq
    _
    _
    f i * g t + qNeg (f j * g j) + (f i * h t + qNeg (f k * h k))
      ≡⟨ qSubPair (f i * g t) (f i * h t) (f j * g j) (f k * h k) ⟩
        f i * g t + f i * h t + qNeg (f j * g j + f k * h k)
      ≡⟨ cong
        λv. Q
        λv. v + qNeg (f j * g j + f k * h k)
        sym _ _ (qDistribL (f i) (g t) (h t)) ⟩
        f i * (g t + h t) + qNeg (f j * g j + f k * h k)
    bndEqB
      _
      _
      _
      qMulSumBound (A + B) (A + C) (rBound m m)
      bndAdd
        bndMulSub
          hfB i
          hgB j
          bndDeep g hgR _ _ _ dt dj
          bndDeep f hfR _ _ _ di dj
          hA
          hB
          leQZeroBound m m
        bndMulSub
          hfB i
          hhB k
          bndDeep h hhR _ _ _ dt dk
          bndDeep f hfR _ _ _ di dk
          hA
          hC
          leQZeroBound m m

rDistrib : (p q r : RSeq) → REq (rMul p (rAdd q r)) (rAdd (rMul p q) (rMul p r))
  using (Real.add.addSeq.eq,
    Real.add.rAdd.eq,
    Real.mul.mulSeq.eq,
    Real.mul.rMul.eq,
    Real.neg.seqOf.eq)
rDistrib =
  λp q r. reqOfClose
    seqBound p + seqBound q + (seqBound p + seqBound r)
    λm. distribStepGen
      seqOf p
      seqOf q
      seqOf r
      _
      _
      _
      _
      _
      _
      _
      _
      bndSeqBound p
      bndSeqBound q
      bndSeqBound r
      regBnd _ (regOf p)
      regBnd _ (regOf q)
      regBnd _ (regOf r)
      leQInvIdx (mulPred p (rAdd q r)) m
      leQTrans
        _
        _
        _
        leQInvDbl (mulIdx (mulPred p (rAdd q r)) m)
        leQInvIdx (mulPred p (rAdd q r)) m
      leQTrans _ _ _ (leQInvIdx (mulPred p q) (dbl m)) (leQInvDbl m)
      leQTrans _ _ _ (leQInvIdx (mulPred p r) (dbl m)) (leQInvDbl m)
      seqBoundPos
      seqBoundPos
      seqBoundPos

realDistribL : (u v w : Real) → u * (v + w) ≡ u * v + u * w
  using (Real.Real.unfold, Real.add.+.eq, Real.mul.*.eq)
realDistribL =
  λu v w. quot-elim (p. quot-elim (q. quot-elim (r. realEqOfREq _ _ (rDistrib p q r)) w) v) u

-- ===== associativity =====
--
-- At index m the two sides read
--
--   left   =  (p_a · q_a) · r_i
--   right  =  p_j · (q_b · r_b)
--
-- with a nested under i and b nested under j, so FOUR depths again,
-- all at least m. Reassociate the right side and it is one outer
-- product-difference whose left factor is itself a product:
--
--   |p_a q_a| ≤ A·B          (a product of ceilings, not a sum)
--   |p_a q_a − p_j q_b| ≤ A·rBound m m + B·rBound m m
--
-- so the outer estimate needs the two moduli to differ — bndMulSubQ.
-- The constant that falls out is A·B + C·(A + B), a natural, which is
-- all reqOfClose asks for.
leQZeroAdd : {u v : Q} → qZero ≤ u → qZero ≤ v → qZero ≤ u + v
leQZeroAdd = λu v hu hv. leQTrans _ _ _ hu (leQSelfAdd u hv)

-- α·β + γ·(α + β), as a rational, is the natural A·B + C·(A + B)
kappaEq : (A B C : ℕ)
  → qOfNat A * qOfNat B + qOfNat C * (qOfNat A + qOfNat B) ≡ qOfNat (A * B + C * (A + B))
kappaEq =
  λA B C. qOfNat A * qOfNat B + qOfNat C * (qOfNat A + qOfNat B)
    ≡⟨ cong (λv. Q) (λv. qOfNat A * qOfNat B + qOfNat C * v) (qOfNatAdd A B) ⟩
      qOfNat A * qOfNat B + qOfNat C * qOfNat (A + B)
    ≡⟨ cong (λv. Q) (λv. v + qOfNat C * qOfNat (A + B)) (qOfNatMul A B) ⟩
      qOfNat (A * B) + qOfNat C * qOfNat (A + B)
    ≡⟨ cong (λv. Q) (λv. qOfNat (A * B) + v) (qOfNatMul C (A + B)) ⟩
      qOfNat (A * B) + qOfNat (C * (A + B))
    ≡⟨ qOfNatAdd (A * B) (C * (A + B)) ⟩ qOfNat (A * B + C * (A + B))

-- (αβ)d + γ(αd + βd) ≡ κ·d, with κ = αβ + γ(α + β) given as an
-- argument (the factor, parameterised — B-16 again)
assocBoundEq : {al be ga : Q}
  (d : Q)
  {kp : Q}
  → (al * be + ga * (al + be) ≡ kp) → al * be * d + ga * (al * d + be * d) ≡ kp * d
assocBoundEq =
  λal be ga d kp hk. al * be * d + ga * (al * d + be * d)
    ≡⟨ cong (λv. Q) (λv. al * be * d + ga * v) (sym _ _ (qDistribR d al be)) ⟩
      al * be * d + ga * ((al + be) * d)
    ≡⟨ cong (λv. Q) (λv. al * be * d + v) (sym _ _ (qMulAssoc ga (al + be) d)) ⟩
      al * be * d + ga * (al + be) * d
    ≡⟨ sym _ _ (qDistribR d (al * be) (ga * (al + be))) ⟩ (al * be + ga * (al + be)) * d
    ≡⟨ cong (λv. Q) (λv. v * d) hk ⟩ kp * d

assocStepGen : (f g h : ℕ → Q)
  (A B C m a i j b : ℕ)
  → ((z : ℕ) → Bnd (qOfNat A) (f z))
    → ((z : ℕ) → Bnd (qOfNat B) (g z))
      → ((z : ℕ) → Bnd (qOfNat C) (h z))
        → ((z w : ℕ) → Bnd (rBound z w) (f z + qNeg (f w)))
          → ((z w : ℕ) → Bnd (rBound z w) (g z + qNeg (g w)))
            → ((z w : ℕ) → Bnd (rBound z w) (h z + qNeg (h w)))
              → qInvNat a ≤ qInvNat m
                → qInvNat i ≤ qInvNat m
                  → qInvNat j ≤ qInvNat m
                    → qInvNat b ≤ qInvNat m
                      → qZero ≤ qOfNat A
                        → qZero ≤ qOfNat B
                          → qZero ≤ qOfNat C
                            → Bnd
                              qOfNat (A * B + C * (A + B)) * rBound m m
                              f a * g a * h i + qNeg (f j * (g b * h b))
assocStepGen =
  λf g h A B C m a i j b hfB hgB hhB hfR hgR hhR da di dj db hA hB hC. bndEq
    _
    _
    cong (λv. Q) (λv. f a * g a * h i + qNeg v) (qMulAssoc (f j) (g b) (h b))
    bndEqB
      _
      _
      _
      assocBoundEq (rBound m m) (kappaEq A B C)
      bndMulSubQ
        bndMul hA hB (hfB a) (hgB a)
        hhB b
        bndDeep h hhR _ _ _ di db
        bndMulSubQ
          hfB a
          hgB b
          bndDeep g hgR _ _ _ da db
          bndDeep f hfR _ _ _ da dj
          hA
          hB
          leQZeroBound m m
          leQZeroBound m m
        leQZeroMul hA hB
        hC
        leQZeroBound m m
        leQZeroAdd (leQZeroMul hA (leQZeroBound m m)) (leQZeroMul hB (leQZeroBound m m))

rAssoc : (p q r : RSeq) → REq (rMul (rMul p q) r) (rMul p (rMul q r))
  using (Real.mul.mulSeq.eq, Real.mul.rMul.eq, Real.neg.seqOf.eq)
rAssoc =
  λp q r. reqOfClose
    seqBound p * seqBound q + seqBound r * (seqBound p + seqBound q)
    λm. assocStepGen
      seqOf p
      seqOf q
      seqOf r
      _
      _
      _
      _
      _
      _
      _
      _
      bndSeqBound p
      bndSeqBound q
      bndSeqBound r
      regBnd _ (regOf p)
      regBnd _ (regOf q)
      regBnd _ (regOf r)
      leQTrans
        _
        _
        _
        leQInvIdx (mulPred p q) (mulIdx (mulPred (rMul p q) r) m)
        leQInvIdx (mulPred (rMul p q) r) m
      leQInvIdx (mulPred (rMul p q) r) m
      leQInvIdx (mulPred p (rMul q r)) m
      leQTrans
        _
        _
        _
        leQInvIdx (mulPred q r) (mulIdx (mulPred p (rMul q r)) m)
        leQInvIdx (mulPred p (rMul q r)) m
      seqBoundPos
      seqBoundPos
      seqBoundPos

realMulAssoc : (u v w : Real) → u * v * w ≡ u * (v * w) using (Real.Real.unfold, Real.mul.*.eq)
realMulAssoc =
  λu v w. quot-elim (p. quot-elim (q. quot-elim (r. realEqOfREq _ _ (rAssoc p q r)) w) v) u

-- ===== the remaining laws, and the structure =====
-- right distributivity, by commuting into the left one
realDistribR : (u v w : Real) → (v + w) * u ≡ v * u + w * u
realDistribR =
  λu v w. trans
    _
    _
    _
    realMulComm (v + w) u
    trans
      _
      _
      _
      realDistribL u v w
      trans
        _
        _
        _
        cong (λz. Real) (λz. z + u * w) (realMulComm u v)
        cong (λz. Real) (λz. v * u + z) (realMulComm u w)

-- (−u)·v = −(u·v), a RING consequence: (−u)·v is an additive inverse
-- of u·v, and inverses are unique. No estimate, no representatives.
realMulNeg : {u v : Real} → realNeg u * v ≡ realNeg (u * v)
realMulNeg =
  λu v. realNegUnique
    _
    _
    trans
      _
      _
      _
      sym _ _ (realDistribR v u (realNeg u))
      trans _ _ realZero (cong (λz. Real) (λz. z * v) (realAddNegR u)) realMulZeroL

realMulNegR : (u v : Real) → u * realNeg v ≡ realNeg (u * v)
realMulNegR =
  λu v. trans
    _
    _
    _
    realMulComm u (realNeg v)
    trans (realNeg v * u) _ _ realMulNeg (cong (λz. Real) (λz. realNeg z) (realMulComm v u))

-- ...so ℝ is a commutative ring, and the laws above are exactly its
-- components
realCommRing : IsCommRing Real using (Real.group.realAddGroup.eq, Algebra.ring.IsCommRing.unfold)
realCommRing =
  (,)
    realAddGroup
    (*)
    realOne
    λx y z. eqToId _ _ (realMulAssoc x y z)
    λx y. eqToId _ _ (realMulComm x y)
    λx. eqToId _ _ (realMulOneR x)
    λx y. eqToId (x + y) (y + x) (realAddComm x y)
    λx y z. eqToId (x * (y + z)) (x * y + x * z) (realDistribL x y z)