-- Ring structure of the Dedekind real numbers
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Real.Ring
import PositiveMultiplication
import Algebra.OrderedAdditive

-- Distributivity for arbitrary nonnegative cuts.  Linear order leaves only
-- the zero boundary cases and the genuinely positive case proved by the
-- approximation argument in PositiveMultiplication.
theorem realPosMulCut.distributive_of_nonnegative (A B C : Real)
  requires nonnegativeA : realZero ⊆ A
  requires nonnegativeB : realZero ⊆ B
  requires nonnegativeC : realZero ⊆ C
  shows realPosMulCut(A, realAddCut(B, C)) =
    realAddCut(realPosMulCut(A, B), realPosMulCut(A, C))
proof
  have casesA := Real.nonnegative_cases with nonnegativeA
  have casesB := Real.nonnegative_cases with nonnegativeB
  have casesC := Real.nonnegative_cases with nonnegativeC
  cases casesA with zeroA | positiveA
  . simp [zeroA, realPosMulCut.zero_left,
      realAddCut.zero_left, realAddCut.zero_right]
  . cases casesB with zeroB | positiveB
    . simp [zeroB, realPosMulCut.zero_left, realPosMulCut.zero_right,
        realAddCut.zero_left, realAddCut.zero_right]
    . cases casesC with zeroC | positiveC
      . simp [zeroC, realPosMulCut.zero_left, realPosMulCut.zero_right,
          realAddCut.zero_left, realAddCut.zero_right]
      . exact realPosMulCut.distributive_of_positive at A, B, C with
          *{3},
          positiveA, positiveB, positiveC

-- Non-strict translation laws for the cut order.  The strict versions live in
-- Negation; these forms are the convenient boundary for sign arithmetic.
theorem realAddValue.subset_right (A B C : Real)
  requires subset : A ⊆ B
  shows A + C ⊆ B + C
proof
  have cutSubset := realAddCut.subset_left at A, B, C with
    *{3}, subset
  have leftCut := realAddValue.cut at A, C with *
  have rightCut := realAddValue.cut at B, C with *
  rwa [← leftCut, ← rightCut] at cutSubset

theorem realAddValue.subset_left (A B C : Real)
  requires subset : A ⊆ B
  shows C + A ⊆ C + B
proof
  have translated := realAddValue.subset_right at A, B, C with
    *{3}, subset
  have leftCommutative := realAddValue.commutative at A, C with
    *{2}
  have rightCommutative := realAddValue.commutative at B, C with
    *{2}
  rwa [leftCommutative, rightCommutative] at translated

-- The typed non-strict order inherits its familiar algebraic laws directly
-- from inclusion of Dedekind cuts.
theorem realLe.reflexive (A : Real)
  shows A ≤ A
proof
  exact realLe.of_subset at A, A with
    *{2}, Subset.reflexive at A

theorem realLe.transitive (A B C : Real)
  requires ab : A ≤ B
  requires bc : B ≤ C
  shows A ≤ C
proof
  have subsetAB := realLe.subset at A, B with *
  have subsetBC := realLe.subset at B, C with *
  have subsetAC := Subset.transitive with subsetAB, subsetBC
  exact realLe.of_subset with *

theorem realLe.add_right (A B C : Real)
  requires le : A ≤ B
  shows A + C ≤ B + C
proof
  have subset := realLe.subset with *
  have translated := realAddValue.subset_right at A, B, C with
    *{3}, subset
  exact realLe.of_subset with translated

theorem realLe.add_left (A B C : Real)
  requires le : A ≤ B
  shows C + A ≤ C + B
proof
  have subset := realLe.subset with *
  have translated := realAddValue.subset_left at A, B, C with
    *{3}, subset
  exact realLe.of_subset with translated

theorem realLe.add (A B C D : Real)
  requires ab : A ≤ B
  requires cd : C ≤ D
  shows A + C ≤ B + D
proof
  have first := realLe.add_right at A, B, C with
    *{3}, ab
  have second := realLe.add_left at C, D, B with
    *{3}, cd
  exact realLe.transitive with first, second

theorem realSubValue.le_left (X Y Z : Real)
  requires le : X ≤ Y
  shows X - Z ≤ Y - Z
proof
  have negative := realNegValue.real at Z
  have shifted := realLe.add_right at X, Y, -Z with
    *{2}, negative, le
  unfold realSubValue
  exact shifted

theorem realSubValue.lt_left (X Y Z : Real)
  requires lt : X < Y
  shows X - Z < Y - Z
proof
  have negative := realNegValue.real at Z
  have shifted := realLess.add_right at X, Y, -Z with
    *{2}, negative, lt
  unfold realSubValue
  exact shifted

theorem realAddValue.four_shuffle (A B C D : Real)
  shows (A + B) + (C + D) = (A + C) + (B + D)
proof
  have cdReal := realAddValue.real at C, D with *
  have bdReal := realAddValue.real at B, D with *
  have outerLeft := realAddValue.associative at A, B, C + D with
    *{2}, cdReal
  have middleLeft := realAddValue.associative at B, C, D with
    *{3}
  have swap := realAddValue.commutative at B, C with *
  have middleRight := realAddValue.associative at C, B, D with
    *{3}
  have outerRight := realAddValue.associative at A, C, B + D with
    *{2}, bdReal
  cc

theorem realLess.implies_le (A B : Real)
  requires less : A < B
  shows A ≤ B
proof
  obtain ⟨realA, realB, proper⟩ := realLess.characterization.forward with less
  have subset := ProperSubset.subset with proper
  exact realLe.of_subset with subset

theorem realLess.of_not_le (A B : Real)
  requires notLe : ¬(A ≤ B)
  shows B < A
proof
  have distinct : A ≠ B
    intro equal
    apply notLe
    rw equal
    exact realLe.reflexive with assumption
  have connected := realLess.connected_on
  have alternatives := connected with A, B, distinct
  cases alternatives with forward | reverse
  . exfalso
    apply notLe
    exact realLess.implies_le with forward
  . exact reverse

theorem realLe.transitive_less (A B C : Real)
  requires ab : A ≤ B
  requires bc : B < C
  shows A < C
proof
  have subsetAB := realLe.subset with *
  obtain ⟨realB, realC, properBC⟩ := realLess.characterization.forward with bc
  have subsetBC := ProperSubset.subset with properBC
  have subsetAC := Subset.transitive with subsetAB, subsetBC
  have properAC : A ⊂ C
    constructor
    . exact subsetAC
    . intro equalAC
      apply ProperSubset.ne with properBC
      apply Subset.antisymmetric
      . exact subsetBC
      . rw ← equalAC
        exact subsetAB
  apply realLess.characterization.backward
  unfold RealLess
  tauto

theorem realLe.neg_reverse (A B : Real)
  requires ordered : A ≤ B
  shows -B ≤ -A
proof
  by_contra notOrdered
  have strictNeg := realLess.of_not_le with notOrdered
  have strictNegView := realLess.characterization.forward with strictNeg
  have reversedView := RealLess.neg_reverse with strictNegView
  have reversed := realLess.characterization.backward with reversedView
  have involutiveA := realNegValue.involutive at A
  have involutiveB := realNegValue.involutive at B
  rw [involutiveA, involutiveB] at reversed
  have cycle := realLe.transitive_less with ordered, reversed
  have irreflexive := realLess.irreflexive_on
  exact irreflexive with A, cycle

theorem realSubValue.le (A B C D : Real)
  requires left : A ≤ C
  requires right : D ≤ B
  shows A - B ≤ C - D
proof
  have reversed := realLe.neg_reverse with right
  have combined := realLe.add at A, C, -B, -D with
    *{2},
    realNegValue.real at B with assumption,
    realNegValue.real at D with assumption,
    left, reversed
  unfold realSubValue
  exact combined

theorem realLess.transitive_le (A B C : Real)
  requires ab : A < B
  requires bc : B ≤ C
  shows A < C
proof
  obtain ⟨realA, realB, properAB⟩ := realLess.characterization.forward with ab
  have subsetAB := ProperSubset.subset with properAB
  have subsetBC := realLe.subset with *
  have subsetAC := Subset.transitive with subsetAB, subsetBC
  have properAC : A ⊂ C
    constructor
    . exact subsetAC
    . intro equalAC
      apply ProperSubset.ne with properAB
      apply Subset.antisymmetric
      . exact subsetAB
      . rw equalAC
        exact subsetBC
  apply realLess.characterization.backward
  unfold RealLess
  tauto

theorem realAddValue.nonnegative (A B : Real)
  requires nonnegativeA : realZero ⊆ A
  requires nonnegativeB : realZero ⊆ B
  shows realZero ⊆ A + B
proof
  have translated := realAddValue.subset_left at realZero, B, A with
    realZero.real, *{2}, nonnegativeB
  rw realAddValue.zero_right at translated
  exact Subset.transitive with nonnegativeA, translated

theorem realSubValue.add_right_cancel (A B : Real)
  shows (A - B) + B = A
proof
  unfold realSubValue
  have negBReal := realNegValue.real at B
  calc
    (A + (-B)) + B = A + ((-B) + B) :=
      realAddValue.associative at A, -B, B with
        assumption, negBReal, assumption
    _ = A + 0 := by simp [realAddValue.neg_left]
    _ = A := realAddValue.zero_right at A with assumption

theorem realSubValue.nonnegative_of_subset (A B : Real)
  requires subset : A ⊆ B
  shows realZero ⊆ B - A
proof
  have negAReal := realNegValue.real at A
  have translated := realAddValue.subset_right at A, B, -A with
    *{2}, negAReal, subset
  rw realAddValue.neg_right at translated
  unfold realSubValue
  exact translated

theorem realSubValue.nonnegative_of_le (X Y : Real)
  requires le : X ≤ Y
  shows (0:R) ≤ Y - X
proof
  have subset := realLe.subset with *
  have nonnegative := realSubValue.nonnegative_of_subset with subset
  exact realLe.of_subset with realZero.real, nonnegative

instance reals.ordered_additive_group
  shows OrderedAdditiveGroup(ℝ, realAdd, realZero, realNeg, realLe)
proof
  constructor
  . exact realAdd.abelian_group
  . constructor
      intros x hx
      exact realLe.reflexive
    . constructor
        intros x hx y hy z hz xy yz
        exact realLe.transitive with xy, yz
      . constructor
        . intros x hx y hy z hz w hw xy zw
          exact realLe.add with xy, zw
        . constructor
          . intros x hx y hy xy
            exact realLe.neg_reverse with xy
          . intros x hx y hy xy
            have positive := realSubValue.nonnegative_of_le with xy
            unfold realSubValue at positive
            exact positive

theorem realMulValue.distributive_of_nonnegative (A B C : Real)
  requires nonnegativeA : realZero ⊆ A
  requires nonnegativeB : realZero ⊆ B
  requires nonnegativeC : realZero ⊆ C
  shows A * (B + C) = A * B + A * C
proof
  have sumReal := realAddValue.real at B, C with *
  have abReal := realMulValue.real at A, B with *
  have acReal := realMulValue.real at A, C with *
  have sumNonnegative := realAddValue.nonnegative with nonnegativeB, nonnegativeC
  have leftCut := realMulValue.cut at A, B + C with assumption, sumReal
  have sumCut := realAddValue.cut at B, C with *
  have abCut := realMulValue.cut at A, B with *
  have acCut := realMulValue.cut at A, C with *
  have rightCut := realAddValue.cut with abReal, acReal
  have leftReduction := realMulCut.of_nonnegative at A, B + C with
    assumption, sumReal, nonnegativeA, sumNonnegative
  have abReduction := realMulCut.of_nonnegative with nonnegativeA, nonnegativeB
  have acReduction := realMulCut.of_nonnegative with nonnegativeA, nonnegativeC
  have sumShape : realPosMulCut(A, B + C) =
      realPosMulCut(A, realAddCut(B, C))
    rw sumCut
    rfl
  have productsReduce : realAddCut(
      realPosMulCut(A, B), realPosMulCut(A, C)) =
      realAddCut(realMulCut(A, B), realMulCut(A, C))
    rw [abReduction, acReduction]
    rfl
  have productsShape : realAddCut(
      realMulCut(A, B), realMulCut(A, C)) =
      realAddCut(A * B, A * C)
    rw [abCut, acCut]
    rfl
  have resultShape : realAddCut(A * B, A * C) = A * B + A * C
    rw rightCut
    rfl
  calc
    A * (B + C) = realMulCut(A, B + C) := leftCut
    _ = realPosMulCut(A, B + C) := leftReduction
    _ = realPosMulCut(A, realAddCut(B, C)) := sumShape
    _ = realAddCut(realPosMulCut(A, B), realPosMulCut(A, C)) :=
      realPosMulCut.distributive_of_nonnegative at A, B, C with
        *{3},
        nonnegativeA, nonnegativeB, nonnegativeC
    _ = realAddCut(realMulCut(A, B), realMulCut(A, C)) := productsReduce
    _ = realAddCut(A * B, A * C) := productsShape
    _ = A * B + A * C := resultShape

-- Negation is additive.  We prove this through uniqueness of inverses in the
-- already established additive group; the calculation is the familiar
-- rearrangement (-A-B)+(A+B)=0.
theorem realNegValue.add (A B : Real)
  shows -(A + B) = (-A) + (-B)
proof
  have negAReal := realNegValue.real at A
  have negBReal := realNegValue.real at B
  have sumReal := realAddValue.real at A, B with *
  have negSumReal := realNegValue.real with sumReal
  have candidateReal := realAddValue.real with negAReal, negBReal
  have innerAssoc := realAddValue.associative at -B, A, B with
    negBReal, *{2}
  have innerComm := realAddValue.commutative at -B, A with
    negBReal, assumption
  have regroup := realAddValue.associative at A, -B, B with
    assumption, negBReal, assumption
  have candidateLeft : ((-A) + (-B)) + (A + B) = 0
    calc
      ((-A) + (-B)) + (A + B) =
          (-A) + ((-B) + (A + B)) :=
        realAddValue.associative at -A, -B, A + B with
          negAReal, negBReal, sumReal
      _ = (-A) + (((-B) + A) + B) := by cc
      _ = (-A) + ((A + (-B)) + B) := by cc
      _ = (-A) + (A + ((-B) + B)) := by cc
      _ = (-A) + (A + 0) := by simp [realAddValue.neg_left]
      _ = (-A) + A := by simp [realAddValue.zero_right]
      _ = 0 := realAddValue.neg_left at A with assumption
  have candidateRight : (A + B) + ((-A) + (-B)) = 0
    calc
      (A + B) + ((-A) + (-B)) = ((-A) + (-B)) + (A + B) :=
        realAddValue.commutative at A + B, (-A) + (-B) with
          sumReal, candidateReal
      _ = 0 := candidateLeft
  have monoid := realAdd.comm_monoid
  have sumInReals := sumReal
  have negSumInReals := negSumReal
  have candidateInReals := candidateReal
  apply IsInverse.unique at
    ℝ, realAdd, realZero, A + B, -(A + B), (-A) + (-B)
  . exact IsCommMonoid.monoid with monoid
  . unfold IsInverse
    refine ⟨sumInReals, negSumInReals, _, _⟩
    . exact realAddValue.neg_left with sumReal
    . exact realAddValue.neg_right with sumReal
  . unfold IsInverse
    refine ⟨sumInReals, candidateInReals, candidateLeft, candidateRight⟩

theorem realSubValue.neg_swap (A B : Real)
  shows B - A = -(A - B)
proof
  have negAReal := realNegValue.real at A
  have negBReal := realNegValue.real at B
  have involutiveB := realNegValue.involutive at B
  have negatedSum := realNegValue.add at A, -B with
    assumption, negBReal
  unfold realSubValue
  have commutative := realAddValue.commutative at B, -A with
    assumption, negAReal
  cc

theorem realSubValue.neg_neg (A B : Real)
  shows (-A) - (-B) = -(A - B)
proof
  have negAReal := realNegValue.real at A
  have involutiveB := realNegValue.involutive at B
  have swapped := realSubValue.neg_swap at A, B with *
  have commutes := realAddValue.commutative at -A, B with
    negAReal, assumption
  unfold realSubValue at swapped
  unfold realSubValue
  cc

theorem realSubValue.add_add (A B C D : Real)
  shows (A + B) - (C + D) = (A - C) + (B - D)
proof
  have negSum := realNegValue.add at C, D with *
  have negCReal := realNegValue.real at C
  have negDReal := realNegValue.real at D
  have sumABReal := realAddValue.real at A, B with *
  have aNegCReal := realAddValue.real at A, -C with assumption, negCReal
  have outerAssoc := realAddValue.associative with sumABReal, negCReal, negDReal
  have firstAssoc := realAddValue.associative at A, B, -C with
    *{2}, negCReal
  have middleComm := realAddValue.commutative at B, -C with
    assumption, negCReal
  have secondAssoc := realAddValue.associative at A, -C, B with
    assumption, negCReal, assumption
  have finalAssoc := realAddValue.associative at A + (-C), B, -D with
    aNegCReal, assumption, negDReal
  unfold realSubValue
  rw negSum
  calc
    (A + B) + ((-C) + (-D)) = ((A + B) + (-C)) + (-D) := by cc
    _ = (A + (B + (-C))) + (-D) := by cc
    _ = (A + ((-C) + B)) + (-D) := by cc
    _ = ((A + (-C)) + B) + (-D) := by cc
    _ = (A + (-C)) + (B + (-D)) := by cc

theorem realAddCut.neg_swap (A B : Real)
  shows realAddCut(B, realNegCut(A)) =
    realNegCut(realAddCut(A, realNegCut(B)))
proof
  have negAReal := realNegValue.real at A
  have negBReal := realNegValue.real at B
  have rightReal := realAddValue.real at A, -B with assumption, negBReal
  have swapped := realSubValue.neg_swap at A, B with *
  unfold realSubValue at swapped
  have negACut := realNegValue.cut at A
  have negBCut := realNegValue.cut at B
  have leftCut := realAddValue.cut at B, -A with assumption, negAReal
  have rightCut := realAddValue.cut at A, -B with assumption, negBReal
  have outerCut := realNegValue.cut with rightReal
  rwa [← negACut, ← negBCut, ← leftCut, ← rightCut, ← outerCut]

theorem realAddCut.neg_swap_commuted (A B : Real)
  shows realAddCut(realNegCut(A), B) =
    realNegCut(realAddCut(realNegCut(B), A))
proof
  have negAReal := realNegCut.real at A
  have negBReal := realNegCut.real at B
  have leftComm := realAddCut.commutative at B, realNegCut(A) with
    assumption, negAReal
  have rightComm := realAddCut.commutative at A, realNegCut(B) with
    assumption, negBReal
  have swapped := realAddCut.neg_swap at A, B with *
  cc

theorem realPositivePart.neg (A : Set)
  shows realPositivePart(realNegCut(A)) = realNegativePart(A)
proof
  unfold realNegativePart
  rfl

theorem realNegativePart.neg (A : Real)
  shows realNegativePart(realNegCut(A)) = realPositivePart(A)
proof
  have involutive := realNegCut.involutive at A
  unfold realNegativePart
  cc

-- Negating a nonnegative factor swaps its positive and negative parts.  The
-- signed product therefore reduces to the negative of the positive
-- product, as in elementary algebra.
theorem realMulCut.neg_left_of_nonnegative (A B : Real)
  requires nonnegativeA : realZero ⊆ A
  requires nonnegativeB : realZero ⊆ B
  shows realMulCut(realNegCut(A), B) = realNegCut(realMulCut(A, B))
proof
  have positiveA := realPositivePart.eq_of_nonnegative with nonnegativeA
  have positiveB := realPositivePart.eq_of_nonnegative with nonnegativeB
  have negativeA := realNegativePart.eq_zero_of_nonnegative with nonnegativeA
  have negativeB := realNegativePart.eq_zero_of_nonnegative with nonnegativeB
  have positiveNegA : realPositivePart(realNegCut(A)) = realZero
    calc
      realPositivePart(realNegCut(A)) = realNegativePart(A) :=
        realPositivePart.neg at A
      _ = realZero := negativeA
  have negativeNegA : realNegativePart(realNegCut(A)) = A
    calc
      realNegativePart(realNegCut(A)) = realPositivePart(A) :=
        realNegativePart.neg with assumption
      _ = A := positiveA
  have reduction := realMulCut.of_nonnegative with nonnegativeA, nonnegativeB
  simp [realMulCut, positiveNegA, negativeNegA, positiveB, negativeB,
    realPosMulCut.zero_left, realPosMulCut.zero_right,
    realAddCut.zero_left, realAddCut.zero_right, realNegCut.zero, reduction]

-- The canonical signed product changes sign when either factor is negated.
-- Negation swaps A⁺ and A⁻; commutativity aligns the two cross-term sums,
-- and `realAddCut.neg_swap` performs the final difference reversal.
theorem realMulCut.neg_left (A B : Real)
  shows realMulCut(realNegCut(A), B) = realNegCut(realMulCut(A, B))
proof
  have positiveAReal := realPositivePart.real at A
  have negativeAReal := realNegativePart.real at A
  have positiveBReal := realPositivePart.real at B
  have negativeBReal := realNegativePart.real at B
  have pp := realPosMulCut.real with positiveAReal, positiveBReal
  have nn := realPosMulCut.real with negativeAReal, negativeBReal
  have pn := realPosMulCut.real with positiveAReal, negativeBReal
  have np := realPosMulCut.real with negativeAReal, positiveBReal
  have positiveSum := realAddCut.real with pp, nn
  have negativeSum := realAddCut.real with pn, np
  have positiveSwap := realAddCut.commutative with np, pn
  have negativeSwap := realAddCut.commutative with nn, pp
  have swapped := realAddCut.neg_swap at
    realAddCut(
      realPosMulCut(realPositivePart(A), realPositivePart(B)),
      realPosMulCut(realNegativePart(A), realNegativePart(B))),
    realAddCut(
      realPosMulCut(realPositivePart(A), realNegativePart(B)),
      realPosMulCut(realNegativePart(A), realPositivePart(B))) with
      positiveSum, negativeSum
  simp [realMulCut, realPositivePart.neg, realNegativePart.neg]

theorem realMulCut.neg_right (A B : Real)
  shows realMulCut(A, realNegCut(B)) = realNegCut(realMulCut(A, B))
proof
  have negBReal := realNegCut.real at B
  have commutative := realMulCut.commutative at B, A with
    *{2}
  calc
    realMulCut(A, realNegCut(B)) = realMulCut(realNegCut(B), A) :=
      realMulCut.commutative with assumption, negBReal
    _ = realNegCut(realMulCut(B, A)) :=
      realMulCut.neg_left with *{2}
    _ = realNegCut(realMulCut(A, B)) := by cc

theorem realMulValue.neg_left (A B : Real)
  shows (-A) * B = -(A * B)
proof
  have negAReal := realNegValue.real at A
  have productReal := realMulValue.real at A, B with *
  have negACut := realNegValue.cut at A
  have leftCut := realMulValue.cut at -A, B with negAReal, assumption
  have productCut := realMulValue.cut at A, B with *
  have outerNegCut := realNegValue.cut with productReal
  have cutLaw := realMulCut.neg_left at A, B with *
  rwa [leftCut, negACut, outerNegCut, productCut]

theorem realMulValue.neg_right (A B : Real)
  shows A * (-B) = -(A * B)
proof
  have negBReal := realNegValue.real at B
  have productReal := realMulValue.real at A, B with *
  have negBCut := realNegValue.cut at B
  have leftCut := realMulValue.cut at A, -B with assumption, negBReal
  have productCut := realMulValue.cut at A, B with *
  have outerNegCut := realNegValue.cut with productReal
  have cutLaw := realMulCut.neg_right at A, B with *
  rwa [leftCut, negBCut, outerNegCut, productCut]

theorem realMulValue.neg_both (A B : Real)
  shows (-A) * (-B) = A * B
proof
  have negBReal := realNegValue.real at B
  have productReal := realMulValue.real at A, B with *
  have first := realMulValue.neg_left at A, -B with
    assumption, negBReal
  have second := realMulValue.neg_right at A, B with *
  have involutive := realNegValue.involutive with productReal
  cc

theorem realAddValue.solve_right (X Y Z : Real)
  requires equation : X = Y + Z
  shows Y = X + (-Z)
proof
  have negZReal := realNegValue.real at Z
  have associated := realAddValue.associative at Y, Z, -Z with
    *{2}, negZReal
  have inverse := realAddValue.neg_right at Z
  have identity := realAddValue.zero_right at Y
  cc

theorem realAddValue.subtract_sum (X Y Z : Real)
  requires equation : X = Y + Z
  shows Y + (-X) = -Z
proof
  have negYReal := realNegValue.real at Y
  have negZReal := realNegValue.real at Z
  have negativeSum := realNegValue.add at Y, Z with *
  have associated := realAddValue.associative at Y, -Y, -Z with
    assumption, negYReal, negZReal
  have inverse := realAddValue.neg_right at Y
  have identity := realAddValue.zero_left with negZReal
  cc

theorem realNegValue.nonnegative_of_nonpositive (A : Real)
  requires nonpositive : A ⊆ realZero
  shows realZero ⊆ -A
proof
  have reversed := realNegCut.subset_reverse at A, realZero with
    assumption, realZero.real, nonpositive
  rw realNegCut.zero at reversed
  have cut := realNegValue.cut at A
  rwa cut

theorem realMulValue.distributive_nonnegative_left_nonpositive_right (A B C : Real)
  requires nonnegativeA : realZero ⊆ A
  requires nonpositiveB : B ⊆ realZero
  requires nonpositiveC : C ⊆ realZero
  shows A * (B + C) = A * B + A * C
proof
  have negBReal := realNegValue.real at B
  have negCReal := realNegValue.real at C
  have negBNonnegative := realNegValue.nonnegative_of_nonpositive with nonpositiveB
  have negCNonnegative := realNegValue.nonnegative_of_nonpositive with nonpositiveC
  have base := realMulValue.distributive_of_nonnegative at A, -B, -C with
    assumption, negBReal, negCReal,
    nonnegativeA, negBNonnegative, negCNonnegative
  have sumReal := realAddValue.real at B, C with *
  have abReal := realMulValue.real at A, B with *
  have acReal := realMulValue.real at A, C with *
  have negatedSum := realNegValue.add at B, C with *
  have leftNegative := realMulValue.neg_right at A, B + C with
    assumption, sumReal
  have rightNegativeB := realMulValue.neg_right at A, B with
    *{2}
  have rightNegativeC := realMulValue.neg_right at A, C with
    *{2}
  have negatedRight := realNegValue.add with abReal, acReal
  have leftProductReal := realMulValue.real at A, B + C with assumption, sumReal
  have rightSumReal := realAddValue.real with abReal, acReal
  have leftInvolutive := realNegValue.involutive with leftProductReal
  have rightInvolutive := realNegValue.involutive with rightSumReal
  cc

theorem realMulValue.distributive_nonnegative_left_mixed (A B C : Real)
  requires nonnegativeA : realZero ⊆ A
  requires nonnegativeB : realZero ⊆ B
  requires nonpositiveC : C ⊆ realZero
  shows A * (B + C) = A * B + A * C
proof
  have negCReal := realNegValue.real at C
  have negCNonnegative := realNegValue.nonnegative_of_nonpositive with nonpositiveC
  have cutB := Real.characterization.forward at B with assumption
  have cutNegC := Real.characterization.forward with negCReal
  have comparison := DedekindCut.comparable with cutB, cutNegC
  have involutiveC := realNegValue.involutive at C
  have acNegative := realMulValue.neg_right at A, -C with
    assumption, negCReal
  cases comparison with bSubsetNegC | negCSubsetB
  . have differenceReal := realSubValue.real at -C, B with negCReal, assumption
    have differenceNonnegative := realSubValue.nonnegative_of_subset at B, -C with
      assumption, negCReal, bSubsetNegC
    have cancelled := realSubValue.add_right_cancel at -C, B with
      negCReal, assumption
    have base := realMulValue.distributive_of_nonnegative at
      A, (-C) - B, B with assumption, differenceReal, assumption,
      nonnegativeA, differenceNonnegative, nonnegativeB
    rw cancelled at base
    have atReal := realMulValue.real at A, (-C) - B with
      assumption, differenceReal
    have abReal := realMulValue.real at A, B with *
    have reordered : A * (-C) = A * B + A * ((-C) - B)
      have commutative := realAddValue.commutative with atReal, abReal
      cc
    have remainder := realAddValue.subtract_sum with reordered
    have negBReal := realNegValue.real at B
    have differenceShape : (-C) - B = (-C) + (-B)
      unfold realSubValue
      rfl
    have negatedDifference := realNegValue.add with negCReal, negBReal
    have involutiveB := realNegValue.involutive at B
    have sumCommutative := realAddValue.commutative at B, C with
      *{2}
    have sumShape : B + C = -((-C) - B) by cc
    have leftNegative := realMulValue.neg_right at A, (-C) - B with
      assumption, differenceReal
    have acShape : A * C = -(A * (-C)) by cc
    cc
  . have differenceReal := realSubValue.real at B, -C with assumption, negCReal
    have differenceNonnegative := realSubValue.nonnegative_of_subset with negCSubsetB
    have cancelled := realSubValue.add_right_cancel at B, -C with
      assumption, negCReal
    have base := realMulValue.distributive_of_nonnegative at
      A, B - (-C), -C with assumption, differenceReal, negCReal,
      nonnegativeA, differenceNonnegative, negCNonnegative
    rw cancelled at base
    have solved := realAddValue.solve_right with base
    have sumShape : B + C = B - (-C)
      unfold realSubValue
      cc
    have acShape : A * C = -(A * (-C)) by cc
    cc

theorem realMulValue.distributive_nonnegative_left_mixed_reverse (A B C : Real)
  requires nonnegativeA : realZero ⊆ A
  requires nonpositiveB : B ⊆ realZero
  requires nonnegativeC : realZero ⊆ C
  shows A * (B + C) = A * B + A * C
proof
  have base := realMulValue.distributive_nonnegative_left_mixed with
    *{3}, nonnegativeA, nonnegativeC, nonpositiveB
  have sumCommutative := realAddValue.commutative at B, C with
    *{2}
  have abReal := realMulValue.real at A, B with *
  have acReal := realMulValue.real at A, C with *
  have productCommutative := realAddValue.commutative with abReal, acReal
  cc

theorem Real.sign_cases (A : Real)
  shows A ⊆ realZero ∨ realZero ⊆ A
proof
  have cutA := Real.characterization.forward with assumption
  have cutZero := Real.characterization.forward with realZero.real
  exact DedekindCut.comparable with cutA, cutZero

theorem realMulValue.distributive_of_nonnegative_left (A B C : Real)
  requires nonnegativeA : realZero ⊆ A
  shows A * (B + C) = A * B + A * C
proof
  have signB := Real.sign_cases at B
  have signC := Real.sign_cases at C
  cases signB with nonpositiveB | nonnegativeB
  . cases signC with nonpositiveC | nonnegativeC
    . exact realMulValue.distributive_nonnegative_left_nonpositive_right at
        A, B, C with *{3},
        nonnegativeA, nonpositiveB, nonpositiveC
    . exact realMulValue.distributive_nonnegative_left_mixed_reverse at
        A, B, C with *{3},
        nonnegativeA, nonpositiveB, nonnegativeC
  . cases signC with nonpositiveC2 | nonnegativeC2
    . exact realMulValue.distributive_nonnegative_left_mixed at
        A, B, C with *{3},
        nonnegativeA, nonnegativeB, nonpositiveC2
    . exact realMulValue.distributive_of_nonnegative at A, B, C with
        *{3},
        nonnegativeA, nonnegativeB, nonnegativeC2

theorem realMulValue.distributive (A B C : Real)
  shows A * (B + C) = A * B + A * C
proof
  have signA := Real.sign_cases at A
  cases signA with nonpositiveA | nonnegativeA
  . have negAReal := realNegValue.real at A
    have negANonnegative := realNegValue.nonnegative_of_nonpositive with nonpositiveA
    have base := realMulValue.distributive_of_nonnegative_left at -A, B, C with
      negAReal, *{2}, negANonnegative
    have sumReal := realAddValue.real at B, C with *
    have abReal := realMulValue.real at A, B with *
    have acReal := realMulValue.real at A, C with *
    have leftNegative := realMulValue.neg_left at A, B + C with
      assumption, sumReal
    have rightNegativeB := realMulValue.neg_left at A, B with
      *{2}
    have rightNegativeC := realMulValue.neg_left at A, C with
      *{2}
    have rightNegative := realNegValue.add with abReal, acReal
    have leftReal := realMulValue.real at A, B + C with assumption, sumReal
    have rightReal := realAddValue.real with abReal, acReal
    have leftInvolutive := realNegValue.involutive with leftReal
    have rightInvolutive := realNegValue.involutive with rightReal
    cc
  . exact realMulValue.distributive_of_nonnegative_left at A, B, C with
      *{3}, nonnegativeA

-- Associativity is stable when the sign of any one input is reversed.  These
-- three small transport lemmas keep the signed lift below algebraic: they use
-- only the multiplication-negation laws and congruence.
theorem realMulValue.associative.neg_left (A B C : Real)
  requires associative : (A * B) * C = A * (B * C)
  shows ((-A) * B) * C = (-A) * (B * C)
proof
  have abReal := realMulValue.real at A, B with *
  have bcReal := realMulValue.real at B, C with *
  have inner := realMulValue.neg_left at A, B with *
  have outer := realMulValue.neg_left at A * B, C with abReal, assumption
  have right := realMulValue.neg_left at A, B * C with assumption, bcReal
  cc

theorem realMulValue.associative.neg_middle (A B C : Real)
  requires associative : (A * B) * C = A * (B * C)
  shows (A * (-B)) * C = A * ((-B) * C)
proof
  have abReal := realMulValue.real at A, B with *
  have bcReal := realMulValue.real at B, C with *
  have innerLeft := realMulValue.neg_right at A, B with *
  have outerLeft := realMulValue.neg_left at A * B, C with abReal, assumption
  have innerRight := realMulValue.neg_left at B, C with *
  have outerRight := realMulValue.neg_right at A, B * C with assumption, bcReal
  cc

theorem realMulValue.associative.neg_right (A B C : Real)
  requires associative : (A * B) * C = A * (B * C)
  shows (A * B) * (-C) = A * (B * (-C))
proof
  have abReal := realMulValue.real at A, B with *
  have bcReal := realMulValue.real at B, C with *
  have left := realMulValue.neg_right at A * B, C with abReal, assumption
  have inner := realMulValue.neg_right at B, C with *
  have right := realMulValue.neg_right at A, B * C with assumption, bcReal
  cc

theorem realMulValue.associative (A B C : Real)
  shows (A * B) * C = A * (B * C)
proof
  have signA := Real.sign_cases at A
  have signB := Real.sign_cases at B
  have signC := Real.sign_cases at C
  cases signA with nonpositiveA | nonnegativeA
  . have negAReal := realNegValue.real at A
    have nonnegativeNegA := realNegValue.nonnegative_of_nonpositive with nonpositiveA
    have involutiveA := realNegValue.involutive at A
    have negNegAReal := realNegValue.real with negAReal
    cases signB with nonpositiveB | nonnegativeB
    . have negBReal := realNegValue.real at B
      have nonnegativeNegB := realNegValue.nonnegative_of_nonpositive with nonpositiveB
      have involutiveB := realNegValue.involutive at B
      have negNegBReal := realNegValue.real with negBReal
      cases signC with nonpositiveCNNN | nonnegativeCNNP
      . have negCRealNNN := realNegValue.real at C
        have nonnegativeNegCNNN := realNegValue.nonnegative_of_nonpositive with nonpositiveCNNN
        have involutiveCNNN := realNegValue.involutive at C
        have associativeNNN := realMulValue.associative_of_nonnegative with
          negAReal, negBReal, negCRealNNN, nonnegativeNegA, nonnegativeNegB, nonnegativeNegCNNN
        have associativeNegANNN := realMulValue.associative.neg_left with
          negAReal, negBReal, negCRealNNN, associativeNNN
        have associativeNegABNNN := realMulValue.associative.neg_middle with
          negNegAReal, negBReal, negCRealNNN, associativeNegANNN
        have associativeNegABCNNN := realMulValue.associative.neg_right with
          negNegAReal, negNegBReal, negCRealNNN, associativeNegABNNN
        cc
      . have associativeNNP := realMulValue.associative_of_nonnegative at
          -A, -B, C with negAReal, negBReal, assumption,
          nonnegativeNegA, nonnegativeNegB, nonnegativeCNNP
        have associativeNegANNP := realMulValue.associative.neg_left with
          negAReal, negBReal, assumption, associativeNNP
        have associativeNegABNNP := realMulValue.associative.neg_middle with
          negNegAReal, negBReal, assumption, associativeNegANNP
        cc
    . cases signC with nonpositiveCNPN | nonnegativeCNPP
      . have negCRealNPN := realNegValue.real at C
        have nonnegativeNegCNPN := realNegValue.nonnegative_of_nonpositive with nonpositiveCNPN
        have involutiveCNPN := realNegValue.involutive at C
        have associativeNPN := realMulValue.associative_of_nonnegative at
          -A, B, -C with negAReal, assumption, negCRealNPN,
          nonnegativeNegA, nonnegativeB, nonnegativeNegCNPN
        have associativeNegANPN := realMulValue.associative.neg_left at
          -A, B, -C with negAReal, assumption, negCRealNPN, associativeNPN
        have associativeNegACNPN := realMulValue.associative.neg_right at
          -(-A), B, -C with negNegAReal, assumption, negCRealNPN,
          associativeNegANPN
        cc
      . have associativeNPP := realMulValue.associative_of_nonnegative at
          -A, B, C with negAReal, *{2},
          nonnegativeNegA, nonnegativeB, nonnegativeCNPP
        have associativeNegANPP := realMulValue.associative.neg_left with associativeNPP
        cc
  . cases signB with nonpositiveB | nonnegativeB
    . have negBReal := realNegValue.real at B
      have nonnegativeNegB := realNegValue.nonnegative_of_nonpositive with nonpositiveB
      have involutiveB := realNegValue.involutive at B
      have negNegBRealPN := realNegValue.real with negBReal
      cases signC with nonpositiveCPNN | nonnegativeCPNP
      . have negCRealPNN := realNegValue.real at C
        have nonnegativeNegCPNN := realNegValue.nonnegative_of_nonpositive with nonpositiveCPNN
        have involutiveCPNN := realNegValue.involutive at C
        have associativePNN := realMulValue.associative_of_nonnegative at
          A, -B, -C with assumption, negBReal, negCRealPNN,
          nonnegativeA, nonnegativeNegB, nonnegativeNegCPNN
        have associativeNegBPNN := realMulValue.associative.neg_middle at
          A, -B, -C with assumption, negBReal, negCRealPNN, associativePNN
        have associativeNegBCPNN := realMulValue.associative.neg_right at
          A, -(-B), -C with assumption, negNegBRealPN, negCRealPNN,
          associativeNegBPNN
        cc
      . have associativePNP := realMulValue.associative_of_nonnegative at
          A, -B, C with assumption, negBReal, assumption,
          nonnegativeA, nonnegativeNegB, nonnegativeCPNP
        have associativeNegBPNP := realMulValue.associative.neg_middle at
          A, -B, C with assumption, negBReal, assumption, associativePNP
        cc
    . cases signC with nonpositiveCPPN | nonnegativeCPPP
      . have negCRealPPN := realNegValue.real at C
        have nonnegativeNegCPPN := realNegValue.nonnegative_of_nonpositive with nonpositiveCPPN
        have involutiveCPPN := realNegValue.involutive at C
        have associativePPN := realMulValue.associative_of_nonnegative at
          A, B, -C with *{2}, negCRealPPN,
          nonnegativeA, nonnegativeB, nonnegativeNegCPPN
        have associativeNegCPPN := realMulValue.associative.neg_right at
          A, B, -C with *{2}, negCRealPPN, associativePPN
        cc
      . exact realMulValue.associative_of_nonnegative at A, B, C with
          *{3},
          nonnegativeA, nonnegativeB, nonnegativeCPPP

instance realMul.associative
  shows Associative(ℝ, realMul)
proof
  intros A realA B realB C realC
  have typedA : Real(A) by typecheck
  have typedB : Real(B) by typecheck
  have typedC : Real(C) by typecheck
  exact realMulValue.associative with typedA, typedB, typedC

instance realMul.monoid
  shows IsMonoid(ℝ, realMul, realOne)
proof
  constructor
    constructor
    . exact realMul.magma
    . exact realMul.associative
  . exact realMul.identity

instance realMul.comm_monoid
  shows IsCommMonoid(ℝ, realMul, realOne)
proof
  constructor
  . exact realMul.monoid
  . exact realMul.commutative

theorem realMulValue.distributive_right (A B C : Real)
  shows (A + B) * C = A * C + B * C
proof
  have sumReal := realAddValue.real at A, B with *
  have leftCommutative := realMulValue.commutative at A + B, C with
    sumReal, assumption
  have distributed := realMulValue.distributive at C, A, B with
    *{3}
  have firstCommutative := realMulValue.commutative at C, A with
    *{2}
  have secondCommutative := realMulValue.commutative at C, B with
    *{2}
  cc

instance realMul.distributive
  shows Distributive(ℝ, realAdd, realMul)
proof
  intros A realA B realB C realC
  have typedA : Real(A) by typecheck
  have typedB : Real(B) by typecheck
  have typedC : Real(C) by typecheck
  constructor
  . exact realMulValue.distributive with typedA, typedB, typedC
  . exact realMulValue.distributive_right with typedA, typedB, typedC

instance reals.comm_ring
  shows IsCommRing(ℝ, realAdd, realZero, realNeg, realMul, realOne)
proof
  constructor
    constructor
    . exact realAdd.abelian_group
    . constructor
      . exact realMul.monoid
      . exact realMul.distributive
  . exact realMul.commutative

-- Section: Order helpers for linear arithmetic

theorem realLess.not_self (A : Real)
  shows ¬(A < A)
proof
  intro less
  have irreflexive := realLess.irreflexive_on
  exact irreflexive with A, less

-- Two reals compare one way, are equal, or compare the other way.
theorem realLess.trichotomy (A B : Real)
  shows A < B ∨ A = B ∨ B < A
proof
  by_contra none
  have distinct : A ≠ B
    intro equal
    apply none
    right
    left
    exact equal
  have connected := realLess.connected_on
  have comparison := connected with A, B, distinct
  apply none
  cases comparison with ab | ba
  . left
    exact ab
  . right
    right
    exact ba

theorem realLe.not_less (A B : Real)
  requires le : A ≤ B
  shows ¬(B < A)
proof
  intro less
  have cycle := realLe.transitive_less with *
  exact realLess.not_self with cycle

theorem realLe.of_not_less (A B : Real)
  requires notLess : ¬(B < A)
  shows A ≤ B
proof
  by_contra notLe
  apply notLess
  exact realLess.of_not_le with *

theorem realLe.antisymmetric (A B : Real)
  requires ab : A ≤ B
  requires ba : B ≤ A
  shows A = B
proof
  have abSubset := realLe.subset at A, B with *
  have baSubset := realLe.subset at B, A with *
  exact Subset.antisymmetric with abSubset, baSubset