-- Order compatibility of rational operations
-- 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.Rat.OrderedOperations
import Density

-- The mainstream typed interface to the set-level transitivity certificate.
theorem rationalLess.transitive (x y z : Rational)
  requires xy : x < y
  requires yz : y < z
  shows x < z
proof
  have transitive := rationalLess.transitive_on
  exact transitive with x, y, z, xy, yz

-- Adding the same displayed rational preserves strict order.  The quotient
-- calculation is isolated here so clients can use the ordered-group
-- law without exposing representatives.
-- No rational is below itself.
theorem rationalLess.irreflexive (x : Rational)
  shows ¬(x < x)
proof
  intro less
  have irreflexive := rationalLess.irreflexive_on
  exact irreflexive with x, less

-- Two rationals compare one way, are equal, or compare the other way.
theorem rationalLess.trichotomy (x y : Rational)
  shows x < y ∨ x = y ∨ y < x
proof
  by_contra none
  have distinct : x ≠ y
    intro equal
    apply none
    right
    left
    exact equal
  have connected := rationalLess.connected_on
  have comparison := connected with x, y, distinct
  apply none
  cases comparison with xy | yx
  . left
    exact xy
  . right
    right
    exact yx

theorem rationalLess.add_right_classes (a b m c d n e f k : Nat)
  requires mNonzero : m ≠ 0
  requires nNonzero : n ≠ 0
  requires kNonzero : k ≠ 0
  requires less : relates(rationalLess,
    rationalClass(a, b, m), rationalClass(c, d, n))
  shows relates(rationalLess,
    rationalAddValue(rationalClass(a, b, m), rationalClass(e, f, k)),
    rationalAddValue(rationalClass(c, d, n), rationalClass(e, f, k)))
proof
  have crossLess := rationalLess.classes.forward with mNonzero, nNonzero, less
  have squareNatural := mul.closed at k, k with *
  have squareNonzero := mul.nonzero with kNonzero, kNonzero
  have leftNatural : Nat(n * a + m * d) by simp [mul.closed, add.closed]
  have rightNatural : Nat(m * c + n * b) by simp [mul.closed, add.closed]
  have scaled := Less.mul_left with squareNonzero, crossLess
  have commonNatural : Nat(((m * n) * k) * e + ((m * n) * k) * f) by simp [mul.closed, add.closed]
  have commonReflexive := LessEqual.reflexive with commonNatural
  have augmented := Less.add_LessEqual at
    (k * k) * (n * a + m * d), (k * k) * (m * c + n * b),
    ((m * n) * k) * e + ((m * n) * k) * f,
    ((m * n) * k) * e + ((m * n) * k) * f with
    *{2}, commonNatural, commonNatural, scaled, commonReflexive
  have leftShape : (k * k) * (n * a + m * d) + (((m * n) * k) * e + ((m * n) * k) * f) = (n * k) * (k * a + m * e) + (m * k) * (k * d + n * f)
    ring
  have rightShape : (k * k) * (m * c + n * b) + (((m * n) * k) * e + ((m * n) * k) * f) = (m * k) * (k * c + n * e) + (n * k) * (k * b + m * f)
    ring
  rw [leftShape, rightShape] at augmented
  have leftSum := rationalAddValue.classes at
    a, b, m, e, f, k with mNonzero, kNonzero
  have rightSum := rationalAddValue.classes at
    c, d, n, e, f, k with nNonzero, kNonzero
  rw [leftSum, rightSum]
  have mkNonzero := mul.nonzero with mNonzero, kNonzero
  have nkNonzero := mul.nonzero with nNonzero, kNonzero
  unfold rationalClassSum
  exact rationalLess.classes.backward with mkNonzero, nkNonzero, augmented

-- Translation invariance stated at the public rational boundary.
theorem rationalLess.add_right (x y z : Rational)
  requires less : x < y
  shows x + z < y + z
proof
  obtain ⟨a, aNatural, b, bNatural, m, mNatural, mNonzero, xShape⟩ :=
    Rational.coordinates at x with assumption
  obtain ⟨c, cNatural, d, dNatural, n, nNatural, nNonzero, yShape⟩ :=
    Rational.coordinates at y with assumption
  obtain ⟨e, eNatural, f, fNatural, k, kNatural, kNonzero, zShape⟩ :=
    Rational.coordinates at z with assumption
  rw [xShape, yShape] at less
  rw [xShape, yShape, zShape, rationalAddValue.notation, rationalAddValue.notation]
  exact rationalLess.add_right_classes with mNonzero, nNonzero, kNonzero, less

-- Commutativity turns right translation into the corresponding left law.
theorem rationalLess.add_left (x y z : Rational)
  requires less : x < y
  shows z + x < z + y
proof
  have translated := rationalLess.add_right at x, y, z with less
  obtain ⟨a, aNatural, b, bNatural, m, mNatural, mNonzero, xShape⟩ :=
    Rational.coordinates at x with assumption
  obtain ⟨c, cNatural, d, dNatural, n, nNatural, nNonzero, yShape⟩ :=
    Rational.coordinates at y with assumption
  obtain ⟨e, eNatural, f, fNatural, k, kNatural, kNonzero, zShape⟩ :=
    Rational.coordinates at z with assumption
  have xzCommutative := rationalClassSum.commutative at
    a, b, m, e, f, k with mNonzero, kNonzero
  have yzCommutative := rationalClassSum.commutative at
    c, d, n, e, f, k with nNonzero, kNonzero
  have xzLeft := rationalAddValue.classes at
    a, b, m, e, f, k with mNonzero, kNonzero
  have zxRight := rationalAddValue.classes at
    e, f, k, a, b, m with kNonzero, mNonzero
  have yzLeft := rationalAddValue.classes at
    c, d, n, e, f, k with nNonzero, kNonzero
  have zyRight := rationalAddValue.classes at
    e, f, k, c, d, n with kNonzero, nNonzero
  rw [xShape, yShape, zShape] at translated
  rw [xShape, yShape, zShape]
  rw [rationalAddValue.notation, rationalAddValue.notation] at translated
  rw [rationalAddValue.notation, rationalAddValue.notation]
  rw [xzLeft, yzLeft] at translated
  rw [zxRight, zyRight]
  rwa [xzCommutative, yzCommutative] at translated

theorem rationalLess.of_add_right (x y z : Rational)
  requires translated : x + z < y + z
  shows x < y
proof
  have leftRational := rationalAddValue.rational at x, z with
    *{2}
  have rightRational := rationalAddValue.rational at y, z with
    *{2}
  have negativeZ := rationalNegValue.rational at z
  have shiftedBack := rationalLess.add_right with leftRational, rightRational, negativeZ, translated
  have leftCancel := rationalAddValue.add_sub_cancel_right at x, z with
    *{2}
  have rightCancel := rationalAddValue.add_sub_cancel_right at y, z with
    *{2}
  unfold rationalSubValue at leftCancel
  unfold rationalSubValue at rightCancel
  rwa [leftCancel, rightCancel] at shiftedBack

-- The product of two positive rationals is positive.  At displayed
-- representatives, positivity says b<a and d<c; normalization isolates the
-- positive remainder (a-b)(c-d) without introducing integer subtraction.
theorem rationalLess.mul_positive (x y : Rational)
  requires positiveX : rationalZero < x
  requires positiveY : rationalZero < y
  shows rationalZero < x * y
proof
  obtain ⟨a, aNatural, b, bNatural, m, mNatural, mNonzero, xShape⟩ :=
    Rational.coordinates at x with assumption
  obtain ⟨c, cNatural, d, dNatural, n, nNatural, nNonzero, yShape⟩ :=
    Rational.coordinates at y with assumption
  have oneNonzero : 1 ≠ 0
    intro oneZero
    arith
  have displayedX := positiveX
  have displayedY := positiveY
  rw xShape at displayedX
  rw yShape at displayedY
  unfold rationalZero at displayedX
  unfold rationalZero at displayedY
  have bLessA : b < a
    have cross := rationalLess.classes.forward with oneNonzero, mNonzero, displayedX
    simpa [mul.left_zero, mul.right_zero, mul.left_unit,
      mul.right_unit, add.left_unit, add.right_unit] using cross
  have dLessC : d < c
    have cross := rationalLess.classes.forward with oneNonzero, nNonzero, displayedY
    simpa [mul.left_zero, mul.right_zero, mul.left_unit,
      mul.right_unit, add.left_unit, add.right_unit] using cross
  obtain ⟨k, kNatural, aShape⟩ := bLessA
  obtain ⟨l, lNatural, cShape⟩ := dLessC
  have succKNonzero : succ(k) ≠ 0
    intro succKZero
    have zeroNotSuccK := Naturals.disjoint.zero.succ at k
    apply zeroNotSuccK
    rw succKZero
    rfl
  have succLNonzero : succ(l) ≠ 0
    intro succLZero
    have zeroNotSuccL := Naturals.disjoint.zero.succ at l
    apply zeroNotSuccL
    rw succLZero
    rfl
  have remainderNonzero := mul.nonzero with succKNonzero, succLNonzero
  have positiveRemainder := Less.add_positive at
    a * d + b * c, succ(k) * succ(l) with
    remainderNonzero
  have productGap : a * d + b * c + succ(k) * succ(l) = a * c + b * d
    rw [← aShape, ← cShape]
    ring
  rw productGap at positiveRemainder
  rw [xShape, yShape, rationalMulValue.notation, rationalMulValue.classes]
  unfold rationalClassMul
  unfold rationalZero
  have mnNonzero := mul.nonzero with mNonzero, nNonzero
  apply rationalLess.classes.backward with oneNonzero, mnNonzero
  ring_nf
  exact positiveRemainder

theorem rationalLess.sub_positive (x y : Rational)
  requires less : x < y
  shows rationalZero < y - x
proof
  have negX := rationalNegValue.rational at x
  have shifted := rationalLess.add_right at x, y, -x with
    *{2}, negX, less
  have inverse := rationalAddValue.neg_right at x
  rw inverse at shifted
  unfold rationalSubValue
  exact shifted

-- Multiplication by a positive rational preserves strict order.  The proof is
-- the textbook difference argument z(y-x)>0, with distributivity supplying
-- z*y = z*x + z*(y-x).
theorem rationalLess.mul_left (x y z : Rational)
  requires positiveZ : rationalZero < z
  requires less : x < y
  shows z * x < z * y
proof
  have gapRational := rationalSubValue.rational at y, x with
    *{2}
  have positiveGap := rationalLess.sub_positive with less
  have positiveProduct := rationalLess.mul_positive with positiveZ, positiveGap
  have zxRational := rationalMulValue.rational at z, x with
    *{2}
  have productRational := rationalMulValue.rational at z, y - x with
    assumption, gapRational
  have shifted := rationalLess.add_left with
    rationalZero.rational, productRational, zxRational, positiveProduct
  have leftIdentity := rationalAddValue.zero_right with zxRational
  rw leftIdentity at shifted
  have gapCloses := rationalAddValue.add_sub_cancel_left at x, y with
    *{2}
  have decomposition : z * x + z * (y - x) = z * y
    have distributed := rationalMulValue.distributive_left at z, x, y - x with
      *{2}, gapRational
    rw gapCloses at distributed
    rw ← distributed
    rfl
  rwa decomposition at shifted

theorem rationalLess.mul_right (x y z : Rational)
  requires positiveZ : rationalZero < z
  requires less : x < y
  shows x * z < y * z
proof
  have scaled := rationalLess.mul_left with positiveZ, less
  have leftCommutative := rationalMulValue.commutative at z, x with
    *{2}
  have rightCommutative := rationalMulValue.commutative at z, y with
    *{2}
  rwa [leftCommutative, rightCommutative] at scaled

-- Cancellation by a positive rational.  Together with mul_left this says
-- that positive scaling is an order embedding.
theorem rationalLess.of_mul_left (x y z : Rational)
  requires positiveZ : rationalZero < z
  requires scaled : z * x < z * y
  shows x < y
proof
  have xDistinctY : x ≠ y
    intro equal
    rw equal at scaled
    have irreflexive := rationalLess.irreflexive_on
    exact irreflexive with z * y, scaled
  have connected := rationalLess.connected_on
  have comparison := connected with x, y, xDistinctY
  cases comparison with xLessY | yLessX
  . exact xLessY
  . have reverse := rationalLess.mul_left at y, x, z with
      *{3}, positiveZ, yLessX
    have cycle := rationalLess.transitive with scaled, reverse
    have irreflexive := rationalLess.irreflexive_on
    exfalso
    exact irreflexive with z * x, cycle

theorem rationalLess.neg_reverse (x y : Rational)
  requires less : x < y
  shows -y < -x
proof
  have negX := rationalNegValue.rational at x
  have negY := rationalNegValue.rational at y
  have translated := rationalLess.add_right at x, y, -x with
    *{2}, negX, less
  have inverseX := rationalAddValue.neg_right at x
  rw inverseX at translated
  have sumRational := rationalAddValue.rational at y, -x with assumption, negX
  have shifted := rationalLess.add_left with rationalZero.rational, sumRational, negY, translated
  have leftIdentity := rationalAddValue.zero_right with negY
  rw leftIdentity at shifted
  have associative := rationalAddValue.associative at -y, y, -x with
    negY, assumption, negX
  rw ← associative at shifted
  have inverseY := rationalAddValue.neg_left at y
  rw inverseY at shifted
  have rightIdentity := rationalAddValue.zero_left with negX
  rwa rightIdentity at shifted

-- A positive gap y-x has the expected sign, stated without exposing quotient
-- representatives.  This is the witness-selection lemma used by open real
-- cuts: if x < y, then x-y belongs to the rational cut at zero.
theorem rationalLess.sub_self_negative (x y : Rational)
  requires less : x < y
  shows x - y < rationalZero
proof
  have translated := rationalLess.add_right at x, y, -y with less
  have inverse := rationalAddValue.neg_right at y
  rw inverse at translated
  unfold rationalSubValue
  exact translated

theorem rationalLess.sub_left (x y z : Rational)
  requires less : x < y + z
  shows x - y < z
proof
  have translated := rationalLess.add_right at x, y + z, -y with less
  have cancellation := rationalAddValue.sum_sub_left at y, z with
    *{2}
  unfold rationalSubValue at cancellation
  rw cancellation at translated
  unfold rationalSubValue
  exact translated

theorem rationalLess.add_left_of_sub_left (x y z : Rational)
  requires less : x - y < z
  shows x < y + z
proof
  have translated := rationalLess.add_left at x - y, z, y with less
  have cancellation := rationalAddValue.add_sub_cancel_left at y, x with
    *{2}
  rwa cancellation at translated

-- The rational arithmetic progression beginning at (a-b)/n with mesh 1/D.
-- It is kept as a quotient-level helper so the Archimedean proof can reason
-- about a finite grid without introducing a new coercion primitive.
def rationalGrid (a b n D k : Nat) : Set :=
  rationalClass(D * a + k * n, D * b, n * D)

theorem rationalGrid.rational (a b n D k : Nat)
  requires nNonzero : n ≠ 0
  requires DNonzero : D ≠ 0
  shows Rational(rationalGrid(a, b, n, D, k))
proof
  unfold rationalGrid
  apply rationalClass.rational
  . exact mul.nonzero with nNonzero, DNonzero

theorem rationalGrid.zero (a b n D : Nat)
  requires nNonzero : n ≠ 0
  requires DNonzero : D ≠ 0
  shows rationalGrid(a, b, n, D, 0) = rationalClass(a, b, n)
proof
  unfold rationalGrid
  apply rationalClass.eq
  . exact mul.nonzero with nNonzero, DNonzero
  . exact nNonzero
  . settle with mul.left_zero, mul.right_zero, add.right_unit, mul.associative

theorem rationalGrid.successor (a b n D k : Nat)
  requires nNonzero : n ≠ 0
  requires DNonzero : D ≠ 0
  shows rationalGrid(a, b, n, D, succ(k)) =
    rationalAddValue(rationalGrid(a, b, n, D, k), rationalClass(1, 0, D))
proof
  have nDNonzero := mul.nonzero with nNonzero, DNonzero
  have gridComputed := rationalAddValue.classes at
    D * a + k * n, D * b, n * D, 1, 0, D with
    nDNonzero, DNonzero
  have stepEquality : rationalGrid(a, b, n, D, succ(k)) =
      rationalClassSum(D * a + k * n, D * b, n * D, 1, 0, D)
    unfold rationalGrid
    unfold rationalClassSum
    apply rationalClass.eq
    . exact nDNonzero
    . exact mul.nonzero with nDNonzero, DNonzero
    . simp with mul.right_zero, mul.left_zero, add.right_unit,
        mul.right_unit, mul.left_unit
      ring
  have computedReverse : rationalClassSum(
      D * a + k * n, D * b, n * D, 1, 0, D) =
      rationalAddValue(rationalGrid(a, b, n, D, k), rationalClass(1, 0, D))
    unfold rationalGrid
    simp
  calc
    rationalGrid(a, b, n, D, succ(k)) =
        rationalClassSum(D * a + k * n, D * b, n * D, 1, 0, D) := stepEquality
    _ = rationalAddValue(rationalGrid(a, b, n, D, k), rationalClass(1, 0, D)) := computedReverse

theorem rationalGrid.natural_step (a b n D k : Nat)
  requires nNonzero : n ≠ 0
  requires DNonzero : D ≠ 0
  shows rationalGrid(a, b, n, D, D * k) =
    rationalAddValue(rationalClass(a, b, n), rationalClass(k, 0, 1))
proof
  have oneNonzero : 1 ≠ 0
    intro oneZero
    arith
  have sumComputed := rationalAddValue.classes at
    a, b, n, k, 0, 1 with nNonzero, oneNonzero
  rw sumComputed
  unfold rationalGrid
  unfold rationalClassSum
  apply rationalClass.eq
  . exact mul.nonzero with nNonzero, DNonzero
  . exact mul.nonzero with nNonzero, oneNonzero
  . ring

-- Every rational lies below a displayed natural number.  The witness is
-- canonical: for (a-b)/m we may take a+1.  This is the first
-- Archimedean boundary lemma; clients need not inspect representatives.
theorem Rational.below_natural (x : Rational)
  shows ∃ n, Nat(n) ∧
    x < rationalClass(n, 0, 1)
proof
  obtain ⟨a, aNatural, b, bNatural, m, mNatural, mNonzero, xShape⟩ :=
    Rational.coordinates with assumption
  witness succ(a)
  rw xShape
  have oneNonzero : 1 ≠ 0
    intro oneZero
    arith
  have cross : Less(a, add(mul(m, succ(a)), b))
    have shape := natural.zero_or_successor with mNatural
    cases shape with zero | successor
    . exfalso
      apply mNonzero
      exact zero
    . obtain ⟨j, jNatural, mShape⟩ := successor
      rw mShape
      have successorNatural := Naturals.constructor.succ with aNatural
      have productStep := mul.succ_left with jNatural, successorNatural
      rw productStep
      have jProductNatural : Nat(mul(j, succ(a))) by typecheck
      have aLessSuccessor : a < succ(a)
        apply Less.of_membership
        . exact membership.self_successor with aNatural
      have productNonnegative := Grace.Core.Nat.Order.LessEqual.zero with jProductNatural
      have first := Less.add_LessEqual with
        aNatural, successorNatural, Naturals.constructor.zero, jProductNatural, aLessSuccessor, productNonnegative
      have aZero := add.right_unit with aNatural
      rw aZero at first
      have bNonnegative := Grace.Core.Nat.Order.LessEqual.zero with bNatural
      have sumNatural : Nat(add(succ(a), mul(j, succ(a)))) by typecheck
      have final := Less.add_LessEqual with
        aNatural, sumNatural, Naturals.constructor.zero, bNatural, first, bNonnegative
      rwa aZero at final
  have classLaw := rationalLess.classes at
    a, b, m, succ(a), 0, 1 with mNonzero, oneNonzero
  have leftShape : add(mul(1, a), mul(m, 0)) = a by ring
  have rightShape : add(mul(m, succ(a)), mul(1, b)) =
      add(mul(m, succ(a)), b)
    ring
  rw [leftShape, rightShape] at classLaw
  exact classLaw.backward with cross

-- The symmetric half of rational unboundedness: every rational lies above a
-- negative displayed natural.  Negation transports the preceding witness,
-- so no second representative calculation is needed.
theorem Rational.above_negative_natural (x : Rational)
  shows ∃ n, Nat(n) ∧
    rationalClass(0, n, 1) < x
proof
  have negativeRational := rationalNegValue.rational at x
  obtain ⟨n, nNatural, below⟩ := Rational.below_natural with negativeRational
  witness n
  have oneNatural := Naturals.constructor.succ with Naturals.constructor.zero
  have oneNonzero : 1 ≠ 0
    intro oneZero
    arith
  have naturalRational := rationalClass.rational with
    nNatural, Naturals.constructor.zero, oneNatural, oneNonzero
  have reversed := rationalLess.neg_reverse with below
  have involutive := rationalNegValue.involutive at x
  rw [involutive, rationalNegValue.notation] at reversed
  have negativeClass := rationalNegValue.classes with
    nNatural, Naturals.constructor.zero, oneNatural, oneNonzero
  rw negativeClass at reversed
  unfold rationalClassNeg at reversed
  exact reversed

theorem rationalLess.natural_successor (n : Nat)
  shows relates(rationalLess,
    rationalClass(n, 0, 1), rationalClass(succ(n), 0, 1))
proof
  have oneNonzero : 1 ≠ 0
    intro oneZero
    arith
  apply rationalLess.classes.backward with oneNonzero, oneNonzero
  have succNatural := Naturals.constructor.succ at n
  have nUnit := mul.left_unit at n
  have zeroUnit := mul.left_unit with Naturals.constructor.zero
  have succUnit := mul.left_unit with succNatural
  have nZero := add.right_unit at n
  have succAddZero := add.right_unit with succNatural
  rw [nUnit, zeroUnit, succUnit, nZero, succAddZero]
  apply Less.of_membership
  . exact membership.self_successor at n

theorem rationalLess.positive_natural_successor (n : Nat)
  shows relates(rationalLess, rationalZero, rationalClass(succ(n), 0, 1))
proof
  have oneNonzero : 1 ≠ 0
    intro oneZero
    arith
  unfold rationalZero
  apply rationalLess.classes.backward with oneNonzero, oneNonzero
  have succNatural := Naturals.constructor.succ at n
  have zeroUnit := mul.left_unit with Naturals.constructor.zero
  have succUnit := mul.left_unit with succNatural
  have zeroZero := add.right_unit with Naturals.constructor.zero
  have succAddZero := add.right_unit with succNatural
  rw [zeroUnit, succUnit, zeroZero, succAddZero]
  have succNonzero : succ(n) ≠ 0
    intro succZero
    have zeroNotSucc := Naturals.disjoint.zero.succ at n
    apply zeroNotSucc
    rw succZero
    rfl
  have positive := Less.add_positive at 0, succ(n) with succNonzero
  simpa [add.left_unit] using positive

-- Every positive rational dominates a positive unit fraction.  This is the
-- mesh-selection form of the Archimedean property used for finite rational
-- grids; clients never need to inspect the chosen denominator.
theorem rationalZero.lt_one
  shows rationalZero < rationalOne
proof
  have step := rationalLess.positive_natural_successor at 0 with *
  unfold rationalOne
  exact step

theorem rationalLess.exists_positive_unit_fraction (x : Rational)
  requires positive : rationalZero < x
  shows ∃ D, Nat(D) ∧ D ≠ 0 ∧
    rationalZero < rationalClass(1, 0, D) ∧
    rationalClass(1, 0, D) < x
proof
  obtain ⟨a, aNatural, b, bNatural, m, mNatural, mNonzero, xShape⟩ :=
    Rational.coordinates with assumption
  have oneNatural := Naturals.constructor.succ with Naturals.constructor.zero
  have oneNonzero : 1 ≠ 0
    intro oneZero
    arith
  have displayedPositive := positive
  rw xShape at displayedPositive
  unfold rationalZero at displayedPositive
  have numeratorPositive := rationalLess.classes.forward with oneNonzero, mNonzero, displayedPositive
  have bLessA : b < a
    simpa [mul.left_zero, mul.right_zero, mul.left_unit,
      mul.right_unit, add.left_unit, add.right_unit] using numeratorPositive
  witness 2 * m
  have twoNonzero : 2 ≠ 0
    intro twoZero
    arith
  have denominatorNonzero := mul.nonzero with twoNonzero, mNonzero
  constructor
  . exact denominatorNonzero
  constructor
  . unfold rationalZero
    apply rationalLess.classes.backward with oneNonzero, denominatorNonzero
    have zeroLessOne : 0 < 1
      apply Less.of_membership
      . exact membership.self_successor with Naturals.constructor.zero
    ring_nf
    exact zeroLessOne
  . rw xShape
    apply rationalLess.classes.backward with denominatorNonzero, mNonzero
    have oneLessTwo : 1 < 2
      apply Less.of_membership
      . exact membership.self_successor with oneNatural
    have scaled := Less.mul_left with mNonzero, oneLessTwo
    have unit : m * 1 = m by ring
    have twoMComm : m * 2 = 2 * m by ring
    rw [unit, twoMComm] at scaled
    have mLessTwoM := scaled
    have productNatural : Nat((2 * m) * b) by typecheck
    have productReflexive := LessEqual.reflexive with productNatural
    have lower := Less.add_LessEqual with mLessTwoM, productReflexive
    have succBLeA := bLessA
    have upper := LessEqual.mul_left at succ(b), a, 2 * m with
      succBLeA
    have lowerShape : m + (2 * m) * b = m * 1 + (2 * m) * b by ring
    have middleShape : (2 * m) + (2 * m) * b = (2 * m) * succ(b) by ring
    have upperShape : (2 * m) * a = (2 * m) * a + m * 0 by ring
    rw [lowerShape, middleShape] at lower
    rw upperShape at upper
    exact Less.transitive_LessEqual with lower, upper

-- Given positive rationals a and g, choose a positive rational delta below
-- one whose product with a is smaller than g.  This is the reusable
-- Archimedean approximation step behind multiplication of open real cuts.
theorem rationalLess.exists_small_positive_multiplier (a g : Rational)
  requires positiveA : rationalZero < a
  requires positiveG : rationalZero < g
  shows ∃ delta ∈ ℚ,
    rationalZero < delta ∧ delta < rationalOne ∧ a * delta < g
proof
  obtain ⟨D, dNatural, dNonzero, unitPositive, unitBelowG⟩ := rationalLess.exists_positive_unit_fraction with
    positiveG
  obtain ⟨N, nNatural, aBelowN⟩ :=
    Rational.below_natural at a with assumption
  have oneNatural : Nat(1) by typecheck
  have oneNonzero : 1 ≠ 0
    intro oneZero
    arith
  have twoNonzero : 2 ≠ 0
    intro twoZero
    arith
  have nNonzero : N ≠ 0
    intro nZero
    have aBelowZero := aBelowN
    rw nZero at aBelowZero
    have zeroShape : rationalClass(0, 0, 1) = rationalZero
      unfold rationalZero
      rfl
    rw zeroShape at aBelowZero
    have cycle := rationalLess.transitive with positiveA, aBelowZero
    have impossible := rationalLess.irreflexive_on
    exact impossible with rationalZero, cycle
  have dnNonzero := mul.nonzero with dNonzero, nNonzero
  have eNonzero := mul.nonzero with twoNonzero, dnNonzero
  have deltaRational := rationalClass.rational at 1, 0, 2 * (D * N) with
    eNonzero
  have naturalRational := rationalClass.rational at N, 0, 1 with
    oneNonzero
  have deltaPositive : rationalZero < rationalClass(1, 0, 2 * (D * N))
    unfold rationalZero
    apply rationalLess.classes.backward with oneNonzero, eNonzero
    have zeroLessOne : 0 < 1
      apply Less.of_membership
      . exact membership.self_successor at 0 with Naturals.constructor.zero
    ring_nf
    exact zeroLessOne
  have oneLessTwo : 1 < 2
    apply Less.of_membership
    . exact membership.self_successor at 1 with oneNatural
  have dnPositive := Less.add_positive at 0, D * N with dnNonzero
  have oneLeDN : 1 ≤ D * N
    unfold Less at dnPositive
    simpa [add.left_unit] using dnPositive
  have dnLessE := Less.mul_left with dnNonzero, oneLessTwo
  have eShape : (D * N) * 2 = 2 * (D * N) by ring
  rw eShape at dnLessE
  simp [mul.right_unit] at dnLessE
  have oneLessE : 1 < 2 * (D * N) by exact LessEqual.transitive_Less with oneLeDN, dnLessE
  have deltaBelowOne : rationalClass(1, 0, 2 * (D * N)) < rationalOne
    unfold rationalOne
    apply rationalLess.classes.backward with eNonzero, oneNonzero
    ring_nf
    ring_nf at oneLessE
    exact oneLessE
  have scaled := rationalLess.mul_right with deltaPositive, aBelowN
  have naturalTimesDelta : rationalClass(N, 0, 1) *
      rationalClass(1, 0, 2 * (D * N)) = rationalClass(1, 0, 2 * D)
    rw [rationalMulValue.notation, rationalMulValue.classes]
    unfold rationalClassMul
    apply rationalClass.eq
    . exact mul.nonzero at 1, 2 * (D * N) with oneNonzero, eNonzero
    . exact mul.nonzero at 2, D with twoNonzero, dNonzero
    . ring
  rw naturalTimesDelta at scaled
  have dLessTwoD := Less.mul_left with dNonzero, oneLessTwo
  ring_nf at dLessTwoD
  have twoDNonzero := mul.nonzero with twoNonzero, dNonzero
  have halfUnitRational := rationalClass.rational at 1, 0, 2 * D with
    twoDNonzero
  have unitRational := rationalClass.rational at 1, 0, D with dNonzero
  have halfUnitBelowUnit : rationalClass(1, 0, 2 * D) < rationalClass(1, 0, D)
    apply rationalLess.classes.backward with twoDNonzero, dNonzero
    ring_nf
    exact dLessTwoD
  have productBelowG : a * rationalClass(1, 0, 2 * (D * N)) < g
    calc
      a * rationalClass(1, 0, 2 * (D * N)) < rationalClass(1, 0, 2 * D) := scaled
      _ < rationalClass(1, 0, D) := halfUnitBelowUnit
      _ < g := unitBelowG
  witness rationalClass(1, 0, 2 * (D * N))
  constructor
    exact deltaRational
  . refine ⟨deltaPositive, deltaBelowOne, productBelowG⟩

-- If q < a with a positive, a multiplier can be chosen strictly between zero
-- and one while keeping q below the scaled value.  Written this way, clients
-- of open cuts can use the lemma without inspecting its Archimedean witness.
theorem rationalLess.exists_scale_below_one (q a : Rational)
  requires positiveA : rationalZero < a
  requires qLessA : q < a
  shows ∃ b ∈ ℚ,
    rationalZero < b ∧ b < rationalOne ∧ q < a * b
proof
  have gapRational := rationalSubValue.rational at a, q with
    *{2}
  have gapPositive := rationalLess.sub_positive with qLessA
  obtain ⟨delta, deltaInQ, deltaPositive, deltaBelowOne, productSmall⟩ :=
    rationalLess.exists_small_positive_multiplier at a, a - q with
      assumption, gapRational, positiveA, gapPositive
  have deltaRational : Rational(delta) by typecheck
  have oneRational := rationalOne.rational
  have bRational := rationalSubValue.rational with oneRational, deltaRational
  have bPositive := rationalLess.sub_positive with deltaBelowOne
  have translatedDelta := rationalLess.add_right with
    rationalZero.rational, deltaRational, bRational, deltaPositive
  have zeroAtB := rationalAddValue.zero_left with bRational
  have deltaCancel := rationalAddValue.add_sub_cancel_left with deltaRational, oneRational
  rw [zeroAtB, deltaCancel] at translatedDelta
  have bBelowOne : rationalOne - delta < rationalOne by exact translatedDelta
  have productRational := rationalMulValue.rational at a, delta with
    assumption, deltaRational
  have shifted := rationalLess.add_left at
    a * delta, a - q, q with
      productRational, gapRational, assumption, productSmall
  have gapCloses := rationalAddValue.add_sub_cancel_left at q, a with
    *{2}
  rw gapCloses at shifted
  have sumRational := rationalAddValue.rational at q, a * delta with
    assumption, productRational
  have negProductRational := rationalNegValue.rational with productRational
  have shiftedBack := rationalLess.add_right at
    q + a * delta, a, -(a * delta) with
      sumRational, assumption, negProductRational, shifted
  have leftCancel := rationalAddValue.add_sub_cancel_right at q, a * delta with
    assumption, productRational
  unfold rationalSubValue at leftCancel
  rw leftCancel at shiftedBack
  have productShape : a * (rationalOne - delta) = a - a * delta
    unfold rationalSubValue
    have distributed := rationalMulValue.distributive_left at
      a, rationalOne, -delta with
        assumption, oneRational,
        rationalNegValue.rational at delta with deltaRational
    have oneProduct := rationalMulValue.one_right at a
    have negProduct := rationalMulValue.neg_right at a, delta with
      assumption, deltaRational
    rwa [oneProduct, negProduct] at distributed
  have shiftedBackSub : q < a - a * delta
    unfold rationalSubValue
    exact shiftedBack
  rw ← productShape at shiftedBackSub
  witness rationalOne - delta
  constructor
    exact bRational
  . refine ⟨bPositive, bBelowOne, shiftedBackSub⟩