-- Rational operations lifted from signed natural fractions
-- 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.Operations
import Order
import Algebra.Ring.Core

-- The rational represented by (a-b)/m. The nonzero side condition belongs to
-- the theorems that use this construction; the definition itself is total.
def rationalClass (a b m : Set) : Set :=
  ⟦((a, b), m)⟧[rationalRepresentatives, rationalEquivalent]

def rationalZero : Rational := rationalClass(0, 0, 1)
def rationalOne : Rational := rationalClass(1, 0, 1)

def rationalClassNeg (a b m : Set) : Set := rationalClass(b, a, m)

-- (a-b)/m + (c-d)/n = ((n*a+m*c)-(n*b+m*d))/(m*n).
def rationalRepresentativeSum (a b m c d n : Set) : Set :=
  ((n * a + m * c, n * b + m * d), m * n)

def rationalClassSum (a b m c d n : Set) : Set :=
  rationalClass(n * a + m * c, n * b + m * d, m * n)

-- (a-b)(c-d) = (a*c+b*d)-(a*d+b*c).
def rationalRepresentativeMul (a b m c d n : Set) : Set :=
  ((a * c + b * d, a * d + b * c), m * n)

def rationalClassMul (a b m c d n : Set) : Set :=
  rationalClass(a * c + b * d, a * d + b * c, m * n)

-- Quotient-level operations are set-theoretic function graphs. Their
-- witnesses retain the representative calculation, while the bounded carrier
-- makes every public input and output a rational number.
def rationalAdd : Set :=
  { p ∈ ((ℚ × ℚ) × ℚ) |
    ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ ∃ m, Nat(m) ∧ m ≠ 0 ∧
    ∃ c, Nat(c) ∧ ∃ d, Nat(d) ∧ ∃ n, Nat(n) ∧ n ≠ 0 ∧
      p = ((rationalClass(a, b, m), rationalClass(c, d, n)) ↦
        rationalClassSum(a, b, m, c, d, n)) }

def rationalMul : Set :=
  { p ∈ ((ℚ × ℚ) × ℚ) |
    ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ ∃ m, Nat(m) ∧ m ≠ 0 ∧
    ∃ c, Nat(c) ∧ ∃ d, Nat(d) ∧ ∃ n, Nat(n) ∧ n ≠ 0 ∧
      p = ((rationalClass(a, b, m), rationalClass(c, d, n)) ↦
        rationalClassMul(a, b, m, c, d, n)) }

def rationalNeg : Set :=
  { p ∈ (ℚ × ℚ) |
    ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ ∃ m, Nat(m) ∧ m ≠ 0 ∧
      p = (rationalClass(a, b, m) ↦ rationalClassNeg(a, b, m)) }

def rationalAddValue (x y : Rational) : Rational := rationalAdd((x, y))
def rationalMulValue (x y : Rational) : Rational := rationalMul((x, y))
def rationalNegValue (x : Rational) : Rational := rationalNeg(x)

theorem rationalClass.rational (a b m : Nat)
  requires nonzero : m ≠ 0
  shows Rational(rationalClass(a, b, m))
proof
  unfold Rational
  unfold ℚ
  unfold rationalClass
  apply quotient.contains_class
  . exact rationalEquivalent.equivalence
  . have representative := rationalRepresentatives.pair at a, b, m
    specialize representative with *{1}
    exact representative

-- On displayed rational classes, strict order is exactly the familiar
-- cross-multiplication inequality.  This is the quotient boundary used by
-- arithmetic clients: representative transport stays inside the API.
theorem rationalLess.classes (a b m c d n : Nat)
  requires mNonzero : m ≠ 0
  requires nNonzero : n ≠ 0
  shows relates(rationalLess, rationalClass(a, b, m), rationalClass(c, d, n)) ↔
    n * a + m * d < m * c + n * b
proof
  constructor
  . intro less
    have leftRational := rationalClass.rational at a, b, m with mNonzero
    have rightRational := rationalClass.rational at c, d, n with nNonzero
    unfold rationalClass at leftRational
    unfold rationalClass at rightRational
    unfold rationalClass at less
    obtain ⟨u, uInLeft, uRepresentative, v, vInRight, vRepresentative, representativeLess⟩ :=
      rationalLess.representatives at
        ⟦((a, b), m)⟧[rationalRepresentatives, rationalEquivalent],
        ⟦((c, d), n)⟧[rationalRepresentatives, rationalEquivalent] with
        leftRational, rightRational, less
    have leftRepresentative := rationalRepresentatives.pair at a, b, m with mNonzero
    have rightRepresentative := rationalRepresentatives.pair at c, d, n with nNonzero
    have leftSelf := equivalenceClass.self with rationalEquivalent.equivalence, leftRepresentative
    have rightSelf := equivalenceClass.self with rationalEquivalent.equivalence, rightRepresentative
    have leftEquivalent := Rational.members_related at
      ⟦((a, b), m)⟧[rationalRepresentatives, rationalEquivalent],
      u, ((a, b), m) with leftRational, uInLeft, leftSelf
    have rightEquivalent := Rational.members_related at
      ⟦((c, d), n)⟧[rationalRepresentatives, rationalEquivalent],
      v, ((c, d), n) with rightRational, vInRight, rightSelf
    have displayedLess := rationalRepresentativeLess.transport with
      uRepresentative, vRepresentative, leftRepresentative, rightRepresentative, leftEquivalent, rightEquivalent, representativeLess
    exact rationalRepresentativeLess.pair.forward with mNonzero, nNonzero, displayedLess
  . intro crossLess
    unfold rationalClass
    exact rationalLess.of_representatives with mNonzero, nNonzero, crossLess

theorem Rational.coordinates (q : Set)
  requires rational : Rational(q)
  shows ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ ∃ m, Nat(m) ∧ m ≠ 0 ∧
    q = rationalClass(a, b, m)
proof
  unfold Rational at rational
  unfold ℚ at rational
  have quotientMember := quotient.membership.forward at
    rationalRepresentatives, rationalEquivalent, q
  specialize quotientMember with rational
  rcases quotientMember with ⟨bounded, u, uRepresentative, classShape⟩
  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, representativeShape⟩ := rationalRepresentatives.coordinates with uRepresentative
  witness a
  witness b
  witness m
  constructor
  exact mNonzero
  unfold rationalClass
  rw ← representativeShape
  exact classShape

theorem rationalClass.eq (a b m c d n : Nat)
  requires mNonzero : m ≠ 0
  requires nNonzero : n ≠ 0
  requires equivalent : n * a + m * d = m * c + n * b
  shows rationalClass(a, b, m) = rationalClass(c, d, n)
proof
  unfold rationalClass
  apply equivalenceClass.eq
  . exact rationalEquivalent.equivalence
  . have left := rationalRepresentatives.pair at a, b, m with mNonzero
    exact left
  . have right := rationalRepresentatives.pair at c, d, n with nNonzero
    exact right
  . have characterization := rationalEquivalent.relates_representatives at a, b, m, c, d, n
    specialize characterization with *{2}
    apply characterization.backward
    exact equivalent

theorem rationalClass.equivalent_of_eq (a b m c d n : Nat)
  requires mNonzero : m ≠ 0
  requires nNonzero : n ≠ 0
  requires same : rationalClass(a, b, m) = rationalClass(c, d, n)
  shows n * a + m * d = m * c + n * b
proof
  have left := rationalRepresentatives.pair at a, b, m with *
  have right := rationalRepresentatives.pair at c, d, n with *
  have related := equivalenceClass.related_of_eq at
    rationalRepresentatives, rationalEquivalent,
    ((a, b), m), ((c, d), n)
  simp [rationalClass] at same
  specialize related with rationalEquivalent.equivalence, left, right, same
  have characterization := rationalEquivalent.relates_representatives at a, b, m, c, d, n with *
  apply characterization.forward
  exact related

theorem rationalZero.rational
  shows Rational(rationalZero)
proof
  unfold rationalZero
  apply rationalClass.rational
  . have oneNonzero := Naturals.disjoint.zero.succ at 0
    intro oneZero
    apply oneNonzero
    simp

theorem rationalOne.rational
  shows Rational(rationalOne)
proof
  unfold rationalOne
  apply rationalClass.rational
  . have oneNonzero := Naturals.disjoint.zero.succ at 0
    intro oneZero
    apply oneNonzero
    simp

theorem rationalClassNeg.well_defined (a b m c d n : Nat)
  requires mNonzero : m ≠ 0
  requires nNonzero : n ≠ 0
  requires equivalent : n * a + m * d = m * c + n * b
  shows rationalClassNeg(a, b, m) = rationalClassNeg(c, d, n)
proof
  unfold rationalClassNeg
  have reversed : n * b + m * c = m * d + n * a by linear_combination equivalent
  exact rationalClass.eq with *

theorem rationalClassNeg.rational (a b m : Nat)
  requires nonzero : m ≠ 0
  shows Rational(rationalClassNeg(a, b, m))
proof
  unfold rationalClassNeg
  exact rationalClass.rational with *

theorem rationalRepresentativeSum.representative (a b m c d n : Nat)
  requires mNonzero : m ≠ 0
  requires nNonzero : n ≠ 0
  shows rationalRepresentativeSum(a, b, m, c, d, n) ∈ rationalRepresentatives
proof
  unfold rationalRepresentativeSum
  apply rationalRepresentatives.pair
  . exact mul.nonzero with mNonzero, nNonzero

-- Two equivalent choices for each summand produce equivalent sum
-- representatives. The certificate is the familiar common-denominator
-- calculation, expressed as a linear combination of the two input equations.
theorem rationalClassSum.well_defined (a b m a2 b2 m2 c d n c2 d2 n2 : Nat)
  requires mNonzero : m ≠ 0
  requires m2Nonzero : m2 ≠ 0
  requires nNonzero : n ≠ 0
  requires n2Nonzero : n2 ≠ 0
  requires leftEquivalent : m2 * a + m * b2 = m * a2 + m2 * b
  requires rightEquivalent : n2 * c + n * d2 = n * c2 + n2 * d
  shows rationalClassSum(a, b, m, c, d, n) =
    rationalClassSum(a2, b2, m2, c2, d2, n2)
proof
  unfold rationalClassSum
  apply rationalClass.eq
  . exact mul.nonzero with mNonzero, nNonzero
  . exact mul.nonzero with m2Nonzero, n2Nonzero
  . linear_combination n * n2 * leftEquivalent + m * m2 * rightEquivalent

theorem rationalClassSum.rational (a b m c d n : Nat)
  requires mNonzero : m ≠ 0
  requires nNonzero : n ≠ 0
  shows Rational(rationalClassSum(a, b, m, c, d, n))
proof
  unfold rationalClassSum
  apply rationalClass.rational
  . exact mul.nonzero with mNonzero, nNonzero

theorem rationalClassSum.zero_right (a b m : Nat)
  requires nonzero : m ≠ 0
  shows rationalClassSum(a, b, m, 0, 0, 1) = rationalClass(a, b, m)
proof
  simp [rationalClassSum, mul.left_unit, mul.right_unit, mul.right_zero, add.right_unit]

theorem rationalClassSum.commutative (a b m c d n : Nat)
  requires mNonzero : m ≠ 0
  requires nNonzero : n ≠ 0
  shows rationalClassSum(a, b, m, c, d, n) = rationalClassSum(c, d, n, a, b, m)
proof
  unfold rationalClassSum
  apply rationalClass.eq
  . exact mul.nonzero with mNonzero, nNonzero
  . exact mul.nonzero with nNonzero, mNonzero
  . ring

theorem rationalClassSum.associative (a b m c d n e f k : Nat)
  requires mNonzero : m ≠ 0
  requires nNonzero : n ≠ 0
  requires kNonzero : k ≠ 0
  shows rationalClassSum(n * a + m * c, n * b + m * d, m * n, e, f, k) =
    rationalClassSum(a, b, m, k * c + n * e, k * d + n * f, n * k)
proof
  unfold rationalClassSum
  apply rationalClass.eq
  . have mnNonzero := mul.nonzero with mNonzero, nNonzero
    exact mul.nonzero with mnNonzero, kNonzero
  . have nkNonzero := mul.nonzero with nNonzero, kNonzero
    exact mul.nonzero with mNonzero, nkNonzero
  . ring

theorem rationalClassSum.neg_right (a b m : Nat)
  requires nonzero : m ≠ 0
  shows rationalClassSum(a, b, m, b, a, m) = rationalZero
proof
  unfold rationalClassSum
  unfold rationalZero
  apply rationalClass.eq
  . exact mul.nonzero with nonzero, nonzero
  . have oneNonzero := Naturals.disjoint.zero.succ at 0
    intro oneZero
    apply oneNonzero
    simp
  . ring

theorem rationalRepresentativeMul.representative (a b m c d n : Nat)
  requires mNonzero : m ≠ 0
  requires nNonzero : n ≠ 0
  shows rationalRepresentativeMul(a, b, m, c, d, n) ∈ rationalRepresentatives
proof
  unfold rationalRepresentativeMul
  apply rationalRepresentatives.pair
  . exact mul.nonzero with mNonzero, nNonzero

-- Multiplication respects both quotient arguments. Expanding signed products
-- turns the goal into a polynomial combination of the two equivalence
-- equations; no representative is selected and no cancellation is assumed.
theorem rationalClassMul.well_defined (a b m a2 b2 m2 c d n c2 d2 n2 : Nat)
  requires mNonzero : m ≠ 0
  requires m2Nonzero : m2 ≠ 0
  requires nNonzero : n ≠ 0
  requires n2Nonzero : n2 ≠ 0
  requires leftEquivalent : m2 * a + m * b2 = m * a2 + m2 * b
  requires rightEquivalent : n2 * c + n * d2 = n * c2 + n2 * d
  shows rationalClassMul(a, b, m, c, d, n) =
    rationalClassMul(a2, b2, m2, c2, d2, n2)
proof
  unfold rationalClassMul
  apply rationalClass.eq
  . exact mul.nonzero with mNonzero, nNonzero
  . exact mul.nonzero with m2Nonzero, n2Nonzero
  . linear_combination n2 * c * leftEquivalent - n2 * d * leftEquivalent + m * a2 * rightEquivalent - m * b2 * rightEquivalent

theorem rationalClassMul.rational (a b m c d n : Nat)
  requires mNonzero : m ≠ 0
  requires nNonzero : n ≠ 0
  shows Rational(rationalClassMul(a, b, m, c, d, n))
proof
  unfold rationalClassMul
  apply rationalClass.rational
  . exact mul.nonzero with mNonzero, nNonzero

theorem rationalClassMul.one_right (a b m : Nat)
  requires nonzero : m ≠ 0
  shows rationalClassMul(a, b, m, 1, 0, 1) = rationalClass(a, b, m)
proof
  settle with rationalClassMul, mul.left_unit, mul.right_unit, mul.left_zero,
    mul.right_zero, add.left_unit, add.right_unit

theorem rationalClassMul.commutative (a b m c d n : Nat)
  requires mNonzero : m ≠ 0
  requires nNonzero : n ≠ 0
  shows rationalClassMul(a, b, m, c, d, n) = rationalClassMul(c, d, n, a, b, m)
proof
  unfold rationalClassMul
  apply rationalClass.eq
  . exact mul.nonzero with mNonzero, nNonzero
  . exact mul.nonzero with nNonzero, mNonzero
  . ring

theorem rationalClassMul.associative (a b m c d n e f k : Nat)
  requires mNonzero : m ≠ 0
  requires nNonzero : n ≠ 0
  requires kNonzero : k ≠ 0
  shows rationalClassMul(a * c + b * d, a * d + b * c, m * n, e, f, k) =
    rationalClassMul(a, b, m, c * e + d * f, c * f + d * e, n * k)
proof
  unfold rationalClassMul
  apply rationalClass.eq
  . have mnNonzero := mul.nonzero with mNonzero, nNonzero
    exact mul.nonzero with mnNonzero, kNonzero
  . have nkNonzero := mul.nonzero with nNonzero, kNonzero
    exact mul.nonzero with mNonzero, nkNonzero
  . ring

theorem rationalClassMul.distributive_left (a b m c d n e f k : Nat)
  requires mNonzero : m ≠ 0
  requires nNonzero : n ≠ 0
  requires kNonzero : k ≠ 0
  shows rationalClassMul(a, b, m, k * c + n * e, k * d + n * f, n * k) =
    rationalClassSum(
      a * c + b * d, a * d + b * c, m * n,
      a * e + b * f, a * f + b * e, m * k)
proof
  unfold rationalClassMul
  unfold rationalClassSum
  apply rationalClass.eq
  . have nkNonzero := mul.nonzero with nNonzero, kNonzero
    exact mul.nonzero with mNonzero, nkNonzero
  . have mnNonzero := mul.nonzero with mNonzero, nNonzero
    have mkNonzero := mul.nonzero at m, k with *
    exact mul.nonzero with mnNonzero, mkNonzero
  . ring

theorem rationalNeg.relates (a b m : Nat)
  requires mNonzero : m ≠ 0
  shows relates(rationalNeg, rationalClass(a, b, m), rationalClassNeg(a, b, m))
proof
  unfold relates
  apply rationalNeg.membership.backward
  constructor
  . apply product.pair at rationalClass(a, b, m), rationalClassNeg(a, b, m), ℚ, ℚ
    . have input := rationalClass.rational at a, b, m with
        *{3}, mNonzero
      exact input
    . have output := rationalClassNeg.rational at a, b, m with
        *{3}, mNonzero
      exact output
  . refine ⟨a, assumption, b, assumption, m, assumption, mNonzero, rfl⟩

theorem rationalNeg.factors (x y : Set)
  requires mapped : relates(rationalNeg, x, y)
  shows ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ ∃ m, Nat(m) ∧ m ≠ 0 ∧
    x = rationalClass(a, b, m) ∧ y = rationalClassNeg(a, b, m)
proof
  unfold relates at mapped
  simp [rationalNeg.membership] at mapped
  rcases mapped with ⟨bounded, a, aNat, b, bNat, m, mNat, mNonzero, shape⟩
  obtain ⟨inputShape, outputShape⟩ := orderedPair.injective with shape
  refine ⟨a, aNat, b, bNat, m, mNat, mNonzero, inputShape, outputShape⟩

theorem rationalNeg.total
  shows TotalBetween(rationalNeg, ℚ, ℚ)
proof
  intros x xRational
  have typedX : Rational(x) by exact xRational
  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, xShape⟩ := Rational.coordinates with typedX
  witness rationalClassNeg(a, b, m)
  constructor
  . have output := rationalClassNeg.rational at a, b, m with
      aNat, bNat, mNat, mNonzero
    exact output
  . rw xShape
    exact rationalNeg.relates with aNat, bNat, mNat, mNonzero

theorem rationalNeg.functional
  shows Functional(rationalNeg)
proof
  intros x y xy z xz
  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, inputFirst, outputFirst⟩ := rationalNeg.factors with xy
  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, inputSecond, outputSecond⟩ := rationalNeg.factors with xz
  rw inputFirst at inputSecond
  have equivalent := rationalClass.equivalent_of_eq with
    aNat, bNat, mNat, cNat, dNat, nNat, mNonzero, nNonzero, inputSecond
  have sameNegative := rationalClassNeg.well_defined with
    aNat, bNat, mNat, cNat, dNat, nNat, mNonzero, nNonzero, equivalent
  rwa [outputFirst, outputSecond]

theorem rationalNeg.function
  shows rationalNeg : ℚ → ℚ
proof
  constructor
    intros p hp
    simp [rationalNeg.membership] at hp
    rcases hp with ⟨bounded, witnesses⟩
    exact bounded
  . constructor
    . exact rationalNeg.functional
    . exact rationalNeg.total

theorem rationalAdd.relates (a b m c d n : Nat)
  requires mNonzero : m ≠ 0
  requires nNonzero : n ≠ 0
  shows relates(rationalAdd,
    (rationalClass(a, b, m), rationalClass(c, d, n)),
    rationalClassSum(a, b, m, c, d, n))
proof
  unfold relates
  apply rationalAdd.membership.backward at
    ((rationalClass(a, b, m), rationalClass(c, d, n)) ↦
      rationalClassSum(a, b, m, c, d, n))
  constructor
  . apply product.pair at
      (rationalClass(a, b, m), rationalClass(c, d, n)),
      rationalClassSum(a, b, m, c, d, n), ℚ × ℚ, ℚ
    . apply product.pair at rationalClass(a, b, m), rationalClass(c, d, n), ℚ, ℚ
      . have left := rationalClass.rational at a, b, m with mNonzero
        exact left
      . have right := rationalClass.rational at c, d, n with nNonzero
        exact right
    . have sum := rationalClassSum.rational at a, b, m, c, d, n
      specialize sum with *{2}
      exact sum
  refine ⟨a, assumption, b, assumption, m, assumption, mNonzero, c, assumption, d, assumption, n, assumption, nNonzero, rfl⟩

theorem rationalAdd.factors (x y : Set)
  requires h : relates(rationalAdd, x, y)
  shows ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ ∃ m, Nat(m) ∧ m ≠ 0 ∧
    ∃ c, Nat(c) ∧ ∃ d, Nat(d) ∧ ∃ n, Nat(n) ∧ n ≠ 0 ∧
      x = (rationalClass(a, b, m), rationalClass(c, d, n)) ∧
      y = rationalClassSum(a, b, m, c, d, n)
proof
  unfold relates at h
  simp [rationalAdd.membership] at h
  rcases h with ⟨bounded, a, aNat, b, bNat, m, mNat, mNonzero, c, cNat, d, dNat, n, nNat, nNonzero, shape⟩
  have coordinates := orderedPair.injective at x, y,
    (rationalClass(a, b, m), rationalClass(c, d, n)),
    rationalClassSum(a, b, m, c, d, n)
  specialize coordinates with shape
  rcases coordinates with ⟨inputShape, outputShape⟩
  refine ⟨a, aNat, b, bNat, m, mNat, mNonzero, c, cNat, d, dNat, n, nNat, nNonzero, inputShape, outputShape⟩

theorem rationalAdd.total
  shows TotalBetween(rationalAdd, ℚ × ℚ, ℚ)
proof
  intros input hInput
  obtain ⟨bounded, q, qRational, r, rRational, inputShape⟩ := product.membership.forward with hInput
  have qTyped : Rational(q) by exact qRational
  have rTyped : Rational(r) by exact rRational
  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, qShape⟩ := Rational.coordinates with qTyped
  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, rShape⟩ := Rational.coordinates with rTyped
  witness rationalClassSum(a, b, m, c, d, n)
  constructor
  . exact rationalClassSum.rational at a, b, m, c, d, n with mNonzero, nNonzero
  . rw [inputShape, qShape, rShape]
    exact rationalAdd.relates with aNat, bNat, mNat, cNat, dNat, nNat, mNonzero, nNonzero

theorem rationalAdd.functional
  shows Functional(rationalAdd)
proof
  intros input y hY z hZ
  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, c, cNat, d, dNat, n, nNat, nNonzero, inputFirst, outputFirst⟩ := rationalAdd.factors with hY
  obtain ⟨a2, a2Nat, b2, b2Nat, m2, m2Nat, m2Nonzero, c2, c2Nat, d2, d2Nat, n2, n2Nat, n2Nonzero, inputSecond, outputSecond⟩ := rationalAdd.factors with hZ
  rw inputFirst at inputSecond
  have inputs := orderedPair.injective at
    rationalClass(a, b, m), rationalClass(c, d, n),
    rationalClass(a2, b2, m2), rationalClass(c2, d2, n2)
  specialize inputs with inputSecond
  rcases inputs with ⟨leftSame, rightSame⟩
  have leftEquivalent := rationalClass.equivalent_of_eq with
    aNat, bNat, mNat, a2Nat, b2Nat, m2Nat, mNonzero, m2Nonzero, leftSame
  have rightEquivalent := rationalClass.equivalent_of_eq with
    cNat, dNat, nNat, c2Nat, d2Nat, n2Nat, nNonzero, n2Nonzero, rightSame
  have sameSum := rationalClassSum.well_defined at
    a, b, m, a2, b2, m2, c, d, n, c2, d2, n2
  specialize sameSum with
    mNonzero, m2Nonzero, nNonzero, n2Nonzero, leftEquivalent, rightEquivalent
  rwa [outputFirst, outputSecond]

theorem rationalAdd.function
  shows rationalAdd : ℚ × ℚ → ℚ
proof
  constructor
    intros p hp
    simp [rationalAdd.membership] at hp
    rcases hp with ⟨bounded, witnesses⟩
    exact bounded
  . constructor
    . exact rationalAdd.functional
    . exact rationalAdd.total

theorem rationalMul.relates (a b m c d n : Nat)
  requires mNonzero : m ≠ 0
  requires nNonzero : n ≠ 0
  shows relates(rationalMul,
    (rationalClass(a, b, m), rationalClass(c, d, n)),
    rationalClassMul(a, b, m, c, d, n))
proof
  unfold relates
  apply rationalMul.membership.backward at
    ((rationalClass(a, b, m), rationalClass(c, d, n)) ↦
      rationalClassMul(a, b, m, c, d, n))
  constructor
  . apply product.pair at
      (rationalClass(a, b, m), rationalClass(c, d, n)),
      rationalClassMul(a, b, m, c, d, n), ℚ × ℚ, ℚ
    . apply product.pair at rationalClass(a, b, m), rationalClass(c, d, n), ℚ, ℚ
      . have left := rationalClass.rational at a, b, m with mNonzero
        exact left
      . have right := rationalClass.rational at c, d, n with nNonzero
        exact right
    . have product := rationalClassMul.rational at a, b, m, c, d, n
      specialize product with *{2}
      exact product
  refine ⟨a, assumption, b, assumption, m, assumption, mNonzero, c, assumption, d, assumption, n, assumption, nNonzero, rfl⟩

theorem rationalMul.factors (x y : Set)
  requires h : relates(rationalMul, x, y)
  shows ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ ∃ m, Nat(m) ∧ m ≠ 0 ∧
    ∃ c, Nat(c) ∧ ∃ d, Nat(d) ∧ ∃ n, Nat(n) ∧ n ≠ 0 ∧
      x = (rationalClass(a, b, m), rationalClass(c, d, n)) ∧
      y = rationalClassMul(a, b, m, c, d, n)
proof
  unfold relates at h
  simp [rationalMul.membership] at h
  rcases h with ⟨bounded, a, aNat, b, bNat, m, mNat, mNonzero, c, cNat, d, dNat, n, nNat, nNonzero, shape⟩
  have coordinates := orderedPair.injective at x, y,
    (rationalClass(a, b, m), rationalClass(c, d, n)),
    rationalClassMul(a, b, m, c, d, n)
  specialize coordinates with shape
  rcases coordinates with ⟨inputShape, outputShape⟩
  refine ⟨a, aNat, b, bNat, m, mNat, mNonzero, c, cNat, d, dNat, n, nNat, nNonzero, inputShape, outputShape⟩

theorem rationalMul.total
  shows TotalBetween(rationalMul, ℚ × ℚ, ℚ)
proof
  intros input hInput
  obtain ⟨bounded, q, qRational, r, rRational, inputShape⟩ := product.membership.forward with hInput
  have qTyped : Rational(q) by exact qRational
  have rTyped : Rational(r) by exact rRational
  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, qShape⟩ := Rational.coordinates with qTyped
  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, rShape⟩ := Rational.coordinates with rTyped
  witness rationalClassMul(a, b, m, c, d, n)
  constructor
  . exact rationalClassMul.rational at a, b, m, c, d, n with mNonzero, nNonzero
  . rw [inputShape, qShape, rShape]
    exact rationalMul.relates with aNat, bNat, mNat, cNat, dNat, nNat, mNonzero, nNonzero

theorem rationalMul.functional
  shows Functional(rationalMul)
proof
  intros input y hY z hZ
  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, c, cNat, d, dNat, n, nNat, nNonzero, inputFirst, outputFirst⟩ := rationalMul.factors with hY
  obtain ⟨a2, a2Nat, b2, b2Nat, m2, m2Nat, m2Nonzero, c2, c2Nat, d2, d2Nat, n2, n2Nat, n2Nonzero, inputSecond, outputSecond⟩ := rationalMul.factors with hZ
  rw inputFirst at inputSecond
  have inputs := orderedPair.injective at
    rationalClass(a, b, m), rationalClass(c, d, n),
    rationalClass(a2, b2, m2), rationalClass(c2, d2, n2)
  specialize inputs with inputSecond
  rcases inputs with ⟨leftSame, rightSame⟩
  have leftEquivalent := rationalClass.equivalent_of_eq with
    aNat, bNat, mNat, a2Nat, b2Nat, m2Nat, mNonzero, m2Nonzero, leftSame
  have rightEquivalent := rationalClass.equivalent_of_eq with
    cNat, dNat, nNat, c2Nat, d2Nat, n2Nat, nNonzero, n2Nonzero, rightSame
  have sameProduct := rationalClassMul.well_defined at
    a, b, m, a2, b2, m2, c, d, n, c2, d2, n2
  specialize sameProduct with
    mNonzero, m2Nonzero, nNonzero, n2Nonzero, leftEquivalent, rightEquivalent
  rwa [outputFirst, outputSecond]

theorem rationalMul.function
  shows rationalMul : ℚ × ℚ → ℚ
proof
  constructor
    intros p hp
    simp [rationalMul.membership] at hp
    rcases hp with ⟨bounded, witnesses⟩
    exact bounded
  . constructor
    . exact rationalMul.functional
    . exact rationalMul.total

instance rationalAdd.operation
  shows AddOperation(ℚ, rationalAdd)
proof
  exact rationalAdd.function

instance rationalMul.operation
  shows MulOperation(ℚ, rationalMul)
proof
  exact rationalMul.function

instance rationalNeg.operation
  shows NegOperation(ℚ, rationalNeg)
proof
  exact rationalNeg.function

instance rationalZero.of_nat
  shows OfNat(ℚ, 0, rationalZero)
proof
  constructor
  . typecheck
  . exact rationalZero.rational

instance rationalOne.of_nat
  shows OfNat(ℚ, 1, rationalOne)
proof
  constructor
  . typecheck
  . exact rationalOne.rational

notation infixl 60 "+" => call2 via AddOperation(ℚ, _) for Rational
notation infixl 70 "*" => call2 via MulOperation(ℚ, _) for Rational
notation prefix 75 "-" => apply via NegOperation(ℚ, _) for Rational
notation numeral "0" via OfNat(ℚ, 0, _) for Rational
notation numeral "1" via OfNat(ℚ, 1, _) for Rational
def rationalSubValue (x y : Rational) : Rational := x + (-y)
notation infixl 60 "-" => rationalSubValue for Rational

-- Compatibility equations connect the instance-selected graph presentation
-- to the established public value names.
theorem rationalAddValue.notation (x y : Set)
  shows rationalAdd(x, y) = rationalAddValue(x, y)
proof
  unfold call2
  unfold rationalAddValue
  rfl

theorem rationalMulValue.notation (x y : Set)
  shows rationalMul(x, y) = rationalMulValue(x, y)
proof
  unfold call2
  unfold rationalMulValue
  rfl

theorem rationalNegValue.notation (x : Set)
  shows rationalNeg(x) = rationalNegValue(x)
proof
  unfold rationalNegValue
  rfl

theorem rationalNegValue.rational (x : Rational)
  shows Rational(-x)
proof
  rw rationalNegValue.notation
  have xMember : x ∈ ℚ by simp [Rational]
  obtain ⟨y, yMember, mapped⟩ := FunctionBetween.exists_value with rationalNeg.function, xMember
  have applied := FunctionBetween.apply_value with rationalNeg.function, mapped
  unfold rationalNegValue
  rw applied
  exact yMember

theorem rationalNegValue.classes (a b m : Nat)
  requires mNonzero : m ≠ 0
  shows rationalNegValue(rationalClass(a, b, m)) = rationalClassNeg(a, b, m)
proof
  have input := rationalClass.rational at a, b, m with
    *{3}, mNonzero
  have inputMember := input
  unfold Rational at inputMember
  have mapped := rationalNeg.relates at a, b, m with
    *{3}, mNonzero
  unfold rationalNegValue
  exact FunctionBetween.apply_value with rationalNeg.function, inputMember, mapped

theorem rationalAddValue.rational (x y : Rational)
  shows Rational(x + y)
proof
  rw rationalAddValue.notation
  have xMember : x ∈ ℚ by simp [Rational]
  have yMember : y ∈ ℚ by simp [Rational]
  have inputMember := product.pair with xMember, yMember
  obtain ⟨z, zMember, mapped⟩ := FunctionBetween.exists_value with rationalAdd.function, inputMember
  have applied := FunctionBetween.apply_value with rationalAdd.function, inputMember, mapped
  unfold rationalAddValue
  rw applied
  exact zMember

theorem rationalMulValue.rational (x y : Rational)
  shows Rational(x * y)
proof
  rw rationalMulValue.notation
  have xMember : x ∈ ℚ by simp [Rational]
  have yMember : y ∈ ℚ by simp [Rational]
  have inputMember := product.pair with xMember, yMember
  obtain ⟨z, zMember, mapped⟩ := FunctionBetween.exists_value with rationalMul.function, inputMember
  have applied := FunctionBetween.apply_value with rationalMul.function, inputMember, mapped
  unfold rationalMulValue
  rw applied
  exact zMember

theorem rationalNegValue.rational_raw (x : Rational)
  shows Rational(rationalNegValue(x))
proof
  have result := rationalNegValue.rational at x
  rwa rationalNegValue.notation at result

theorem rationalAddValue.rational_raw (x y : Rational)
  shows Rational(rationalAddValue(x, y))
proof
  have result := rationalAddValue.rational at x, y with *
  rwa rationalAddValue.notation at result

theorem rationalMulValue.rational_raw (x y : Rational)
  shows Rational(rationalMulValue(x, y))
proof
  have result := rationalMulValue.rational at x, y with *
  rwa rationalMulValue.notation at result

-- The public operations compute by choosing the unique graph value. These
-- equations let a proof move cleanly between quotient notation and a concrete
-- representative calculation without unfolding the function graph.
theorem rationalAddValue.classes (a b m c d n : Nat)
  requires mNonzero : m ≠ 0
  requires nNonzero : n ≠ 0
  shows rationalAddValue(rationalClass(a, b, m), rationalClass(c, d, n)) =
    rationalClassSum(a, b, m, c, d, n)
proof
  have left := rationalClass.rational at a, b, m with *
  have right := rationalClass.rational at c, d, n with *
  have input := product.pair at
    rationalClass(a, b, m), rationalClass(c, d, n), ℚ, ℚ
  specialize input with left, right
  have mapped := rationalAdd.relates at a, b, m, c, d, n with
    *{6},
    mNonzero, nNonzero
  unfold rationalAddValue
  exact FunctionBetween.apply_value with rationalAdd.function, input, mapped

theorem rationalMulValue.classes (a b m c d n : Nat)
  requires mNonzero : m ≠ 0
  requires nNonzero : n ≠ 0
  shows rationalMulValue(rationalClass(a, b, m), rationalClass(c, d, n)) =
    rationalClassMul(a, b, m, c, d, n)
proof
  have left := rationalClass.rational at a, b, m with *
  have right := rationalClass.rational at c, d, n with *
  have input := product.pair at
    rationalClass(a, b, m), rationalClass(c, d, n), ℚ, ℚ
  specialize input with left, right
  have mapped := rationalMul.relates at a, b, m, c, d, n with
    *{6},
    mNonzero, nNonzero
  unfold rationalMulValue
  exact FunctionBetween.apply_value with rationalMul.function, input, mapped

theorem rationalAddValue.commutative (x y : Rational)
  shows x + y = y + x
proof
  rw [rationalAddValue.notation, rationalAddValue.notation]
  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, xShape⟩ :=
    Rational.coordinates at x with assumption
  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, yShape⟩ :=
    Rational.coordinates at y with assumption
  have mnNonzero := mul.nonzero with mNonzero, nNonzero
  rw [xShape, yShape, rationalAddValue.classes, rationalAddValue.classes]
  exact rationalClassSum.commutative with aNat, bNat, mNat, cNat, dNat, nNat, mNonzero, nNonzero

theorem rationalAddValue.zero_right (x : Rational)
  shows x + 0 = x
proof
  rw rationalAddValue.notation
  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, xShape⟩ :=
    Rational.coordinates with assumption
  have zeroNat : Nat(0) by typecheck
  have oneNat : Nat(1) by typecheck
  have oneNonzero : 1 ≠ 0
    intro oneZero
    arith
  have computed := rationalAddValue.classes with
    aNat, bNat, mNat, zeroNat, zeroNat, oneNat, mNonzero, oneNonzero
  have identity := rationalClassSum.zero_right with aNat, bNat, mNat, mNonzero
  have computedZero : rationalAddValue(rationalClass(a, b, m), rationalZero) = rationalClassSum(a, b, m, 0, 0, 1)
    simpa [rationalZero] using computed
  have classIdentity : rationalAddValue(rationalClass(a, b, m), rationalZero) = rationalClass(a, b, m)
    calc
      rationalAddValue(rationalClass(a, b, m), rationalZero) =
        rationalClassSum(a, b, m, 0, 0, 1) := computedZero
      _ = rationalClass(a, b, m) := identity
  simpa [xShape] using classIdentity

theorem rationalAddValue.zero_left (x : Rational)
  shows 0 + x = x
proof
  calc
    rationalZero + x = x + rationalZero :=
      rationalAddValue.commutative at rationalZero, x with
        rationalZero.rational, assumption
    _ = x := rationalAddValue.zero_right at x with assumption

theorem rationalAddValue.neg_right (x : Rational)
  shows x + (-x) = 0
proof
  rw [rationalAddValue.notation, rationalNegValue.notation]
  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, xShape⟩ :=
    Rational.coordinates with assumption
  have negative := rationalNegValue.classes with aNat, bNat, mNat, mNonzero
  have sum := rationalAddValue.classes with aNat, bNat, mNat, bNat, aNat, mNat, mNonzero, mNonzero
  have sumNegative : rationalAddValue(rationalClass(a, b, m), rationalClassNeg(a, b, m)) = rationalClassSum(a, b, m, b, a, m)
    simpa [rationalClassNeg] using sum
  have inverse := rationalClassSum.neg_right with aNat, bNat, mNat, mNonzero
  have classInverse : rationalAddValue(rationalClass(a, b, m), rationalNegValue(rationalClass(a, b, m))) = rationalZero
    rwa [negative, sumNegative]
  simpa [xShape] using classInverse

theorem rationalAddValue.neg_left (x : Rational)
  shows (-x) + x = 0
proof
  calc
    (-x) + x = x + (-x) :=
      rationalAddValue.commutative at -x, x with
        rationalNegValue.rational with *{2}
    _ = rationalZero := rationalAddValue.neg_right at x with assumption

theorem rationalAddValue.associative (x y z : Rational)
  shows (x + y) + z = x + (y + z)
proof
  rw [rationalAddValue.notation, rationalAddValue.notation, rationalAddValue.notation, rationalAddValue.notation]
  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, xShape⟩ :=
    Rational.coordinates at x with assumption
  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, yShape⟩ :=
    Rational.coordinates at y with assumption
  obtain ⟨e, eNat, f, fNat, k, kNat, kNonzero, zShape⟩ :=
    Rational.coordinates at z with assumption
  have leftNumeratorNat : Nat(n * a + m * c) by typecheck
  have leftDenumeratorNat : Nat(n * b + m * d) by typecheck
  have mnNat : Nat(m * n) by typecheck
  have rightNumeratorNat : Nat(k * c + n * e) by typecheck
  have rightDenumeratorNat : Nat(k * d + n * f) by typecheck
  have nkNat : Nat(n * k) by typecheck
  have mnNonzero := mul.nonzero with mNat, nNat, mNonzero, nNonzero
  have nkNonzero := mul.nonzero with nNat, kNat, nNonzero, kNonzero
  have leftOuterClasses := rationalAddValue.classes with
    leftNumeratorNat, leftDenumeratorNat, mnNat, eNat, fNat, kNat, mnNonzero, kNonzero
  have leftOuter : rationalAddValue(rationalClassSum(a, b, m, c, d, n), rationalClass(e, f, k)) = rationalClassSum(n * a + m * c, n * b + m * d, m * n, e, f, k)
    simpa [rationalClassSum] using leftOuterClasses
  have rightOuterClasses := rationalAddValue.classes with
    aNat, bNat, mNat, rightNumeratorNat, rightDenumeratorNat, nkNat, mNonzero, nkNonzero
  have rightOuter : rationalAddValue(rationalClass(a, b, m), rationalClassSum(c, d, n, e, f, k)) = rationalClassSum(a, b, m, k * c + n * e, k * d + n * f, n * k)
    simpa [rationalClassSum] using rightOuterClasses
  rw [xShape, yShape, zShape, rationalAddValue.classes, rationalAddValue.classes, leftOuter, rightOuter]
  exact rationalClassSum.associative with
    aNat, bNat, mNat, cNat, dNat, nNat, eNat, fNat, kNat, mNonzero, nNonzero, kNonzero

theorem rationalMulValue.commutative (x y : Rational)
  shows x * y = y * x
proof
  rw [rationalMulValue.notation, rationalMulValue.notation]
  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, xShape⟩ :=
    Rational.coordinates at x with assumption
  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, yShape⟩ :=
    Rational.coordinates at y with assumption
  rw [xShape, yShape, rationalMulValue.classes, rationalMulValue.classes]
  exact rationalClassMul.commutative with mNonzero, nNonzero

theorem rationalMulValue.associative (x y z : Rational)
  shows (x * y) * z = x * (y * z)
proof
  rw [rationalMulValue.notation, rationalMulValue.notation, rationalMulValue.notation, rationalMulValue.notation]
  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, xShape⟩ :=
    Rational.coordinates at x with assumption
  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, yShape⟩ :=
    Rational.coordinates at y with assumption
  obtain ⟨e, eNat, f, fNat, k, kNat, kNonzero, zShape⟩ :=
    Rational.coordinates at z with assumption
  have leftNumeratorNat : Nat(a * c + b * d) by typecheck
  have leftDenominatorNat : Nat(a * d + b * c) by typecheck
  have mnNat : Nat(m * n) by typecheck
  have rightNumeratorNat : Nat(c * e + d * f) by typecheck
  have rightDenominatorNat : Nat(c * f + d * e) by typecheck
  have nkNat : Nat(n * k) by typecheck
  have mnNonzero := mul.nonzero with mNat, nNat, mNonzero, nNonzero
  have nkNonzero := mul.nonzero with nNat, kNat, nNonzero, kNonzero
  have leftOuterClasses := rationalMulValue.classes with
    leftNumeratorNat, leftDenominatorNat, mnNat, eNat, fNat, kNat, mnNonzero, kNonzero
  have leftOuter : rationalMulValue(
      rationalClassMul(a, b, m, c, d, n), rationalClass(e, f, k)) =
      rationalClassMul(a * c + b * d, a * d + b * c, m * n, e, f, k)
    simpa [rationalClassMul] using leftOuterClasses
  have rightOuterClasses := rationalMulValue.classes with
    aNat, bNat, mNat, rightNumeratorNat, rightDenominatorNat, nkNat, mNonzero, nkNonzero
  have rightOuter : rationalMulValue(
      rationalClass(a, b, m), rationalClassMul(c, d, n, e, f, k)) =
      rationalClassMul(a, b, m,
        c * e + d * f, c * f + d * e, n * k)
    simpa [rationalClassMul] using rightOuterClasses
  rw [xShape, yShape, zShape, rationalMulValue.classes, rationalMulValue.classes, leftOuter, rightOuter]
  exact rationalClassMul.associative with mNonzero, nNonzero, kNonzero

theorem rationalMulValue.one_right (x : Rational)
  shows x * rationalOne = x
proof
  rw rationalMulValue.notation
  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, xShape⟩ :=
    Rational.coordinates with assumption
  have oneNonzero : 1 ≠ 0
    intro oneZero
    arith
  rw xShape
  unfold rationalOne
  have computed := rationalMulValue.classes at
    a, b, m, 1, 0, 1 with mNonzero, oneNonzero
  rw computed
  exact rationalClassMul.one_right with mNonzero

theorem rationalMulValue.one_left (x : Rational)
  shows rationalOne * x = x
proof
  calc
    rationalOne * x = x * rationalOne :=
      rationalMulValue.commutative at rationalOne, x with
        rationalOne.rational, assumption
    _ = x := rationalMulValue.one_right at x with assumption

theorem rationalMulValue.zero_right (x : Rational)
  shows x * rationalZero = rationalZero
proof
  rw rationalMulValue.notation
  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, xShape⟩ :=
    Rational.coordinates with assumption
  have oneNonzero : 1 ≠ 0
    intro oneZero
    arith
  rw xShape
  unfold rationalZero
  rw rationalMulValue.classes
  unfold rationalClassMul
  apply rationalClass.eq
  . exact mul.nonzero with mNonzero, oneNonzero
  . exact oneNonzero
  . ring

theorem rationalMulValue.zero_left (x : Rational)
  shows rationalZero * x = rationalZero
proof
  calc
    rationalZero * x = x * rationalZero :=
      rationalMulValue.commutative at rationalZero, x with
        rationalZero.rational, assumption
    _ = rationalZero := rationalMulValue.zero_right at x with assumption

theorem rationalMulValue.neg_right (x y : Rational)
  shows x * (-y) = -(x * y)
proof
  rw [rationalMulValue.notation, rationalNegValue.notation, rationalNegValue.notation, rationalMulValue.notation]
  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, xShape⟩ :=
    Rational.coordinates at x with assumption
  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, yShape⟩ :=
    Rational.coordinates at y with assumption
  have productDenominatorNonzero := mul.nonzero with mNonzero, nNonzero
  rw [xShape, yShape, rationalNegValue.classes]
  unfold rationalClassNeg
  rw rationalMulValue.classes
  unfold rationalClassMul
  rw rationalMulValue.classes
  unfold rationalClassMul
  have negComputed := rationalNegValue.classes at
    a * c + b * d, a * d + b * c, m * n with
      productDenominatorNonzero
  rw negComputed
  unfold rationalClassNeg
  apply rationalClass.eq
  . exact productDenominatorNonzero
  . exact productDenominatorNonzero
  . ring

theorem rationalMulValue.neg_left (x y : Rational)
  shows (-x) * y = -(x * y)
proof
  have commutativeLeft := rationalMulValue.commutative at -x, y with
    rationalNegValue.rational with *{2}
  have commutativeRight := rationalMulValue.commutative at y, x with
    *{2}
  rw [commutativeLeft, rationalMulValue.neg_right, commutativeRight]
  rfl

theorem rationalMulValue.distributive_left (x y z : Rational)
  shows x * (y + z) = x * y + x * z
proof
  rw [rationalMulValue.notation, rationalAddValue.notation, rationalMulValue.notation, rationalMulValue.notation, rationalAddValue.notation]
  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, xShape⟩ :=
    Rational.coordinates at x with assumption
  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, yShape⟩ :=
    Rational.coordinates at y with assumption
  obtain ⟨e, eNat, f, fNat, k, kNat, kNonzero, zShape⟩ :=
    Rational.coordinates at z with assumption
  have nkNonzero := mul.nonzero with nNonzero, kNonzero
  have mnNonzero := mul.nonzero with mNonzero, nNonzero
  have mkNonzero := mul.nonzero with mNonzero, kNonzero
  have sumComputed := rationalAddValue.classes at
    c, d, n, e, f, k with nNonzero, kNonzero
  have leftComputed := rationalMulValue.classes at
    a, b, m, k * c + n * e, k * d + n * f, n * k with
    mNonzero, nkNonzero
  have xyComputed := rationalMulValue.classes at
    a, b, m, c, d, n with mNonzero, nNonzero
  have xzComputed := rationalMulValue.classes at
    a, b, m, e, f, k with mNonzero, kNonzero
  have rightComputed := rationalAddValue.classes at
    a * c + b * d, a * d + b * c, m * n,
    a * e + b * f, a * f + b * e, m * k with
    mnNonzero, mkNonzero
  rw [xShape, yShape, zShape]
  calc
    rationalMulValue(rationalClass(a, b, m),
      rationalAddValue(rationalClass(c, d, n), rationalClass(e, f, k))) =
        rationalMulValue(rationalClass(a, b, m),
          rationalClassSum(c, d, n, e, f, k)) := by simp [sumComputed]
    _ = rationalClassMul(a, b, m,
        k * c + n * e, k * d + n * f, n * k) :=
      by simpa [rationalClassSum] using leftComputed
    _ = rationalClassSum(
        a * c + b * d, a * d + b * c, m * n,
        a * e + b * f, a * f + b * e, m * k) :=
      rationalClassMul.distributive_left at
        a, b, m, c, d, n, e, f, k with
        mNonzero, nNonzero, kNonzero
    _ = rationalAddValue(
        rationalClassMul(a, b, m, c, d, n),
        rationalClassMul(a, b, m, e, f, k)) :=
      by simpa [rationalClassMul] using rightComputed
    _ = rationalAddValue(
        rationalMulValue(rationalClass(a, b, m), rationalClass(c, d, n)),
        rationalMulValue(rationalClass(a, b, m), rationalClass(e, f, k))) :=
      by simp [xyComputed, xzComputed]

theorem rationalMulValue.distributive_right (x y z : Rational)
  shows (x + y) * z = x * z + y * z
proof
  have sumRational := rationalAddValue.rational at x, y with
    *{2}
  have outerCommutative := rationalMulValue.commutative at x + y, z with
    sumRational, assumption
  have distributed := rationalMulValue.distributive_left at z, x, y with
    *{3}
  have firstCommutative := rationalMulValue.commutative at z, x with
    *{2}
  have secondCommutative := rationalMulValue.commutative at z, y with
    *{2}
  rw [outerCommutative, distributed, firstCommutative, secondCommutative]
  rfl

theorem rationalSubValue.rational (x y : Rational)
  shows Rational(x - y)
proof
  unfold rationalSubValue
  exact rationalAddValue.rational at x, -y with
    assumption, rationalNegValue.rational at y with assumption

theorem rationalAddValue.add_sub_cancel_left (x y : Rational)
  shows x + (y - x) = y
proof
  unfold rationalSubValue
  have associative := rationalAddValue.associative at x, y, -x with
    *{2}, rationalNegValue.rational at x with assumption
  have associativeYX := rationalAddValue.associative at y, x, -x with
    *{2}, rationalNegValue.rational at x with assumption
  have commutative := rationalAddValue.commutative at x, y with
    *{2}
  have inverse := rationalAddValue.neg_right at x
  have identity := rationalAddValue.zero_right at y
  have regroup : x + (y + (-x)) = (x + y) + (-x)
    rw associative
    rfl
  have swap : (x + y) + (-x) = (y + x) + (-x)
    rw commutative
    rfl
  have cancel : y + (x + (-x)) = y + rationalZero
    rw inverse
    rfl
  calc
    x + (y + (-x)) = (x + y) + (-x) := regroup
    _ = (y + x) + (-x) := swap
    _ = y + (x + (-x)) := associativeYX
    _ = y + rationalZero := cancel
    _ = y := identity

theorem rationalAddValue.add_sub_cancel_right (x y : Rational)
  shows (x + y) - y = x
proof
  unfold rationalSubValue
  have associative := rationalAddValue.associative at x, y, -y with
    *{2}, rationalNegValue.rational at y with assumption
  have inverse := rationalAddValue.neg_right at y
  have identity := rationalAddValue.zero_right at x
  have cancel : x + (y + (-y)) = x + rationalZero
    rw inverse
    rfl
  calc
    (x + y) + (-y) = x + (y + (-y)) := associative
    _ = x + rationalZero := cancel
    _ = x := identity

theorem rationalAddValue.sum_sub_left (x y : Rational)
  shows (x + y) - x = y
proof
  have commutative := rationalAddValue.commutative at x, y with
    *{2}
  have swapped : (x + y) - x = (y + x) - x
    rw commutative
    rfl
  calc
    (x + y) - x = (y + x) - x := swapped
    _ = y := rationalAddValue.add_sub_cancel_right at y, x with
      *{2}

-- Subtracting a sum from its left summand leaves the negative right summand.
-- The statement stays at the quotient level; representative arithmetic is
-- used only as the checked certificate below.
theorem rationalSubValue.sub_sum_left (x y : Rational)
  shows x - (x + y) = -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 mnNonzero := mul.nonzero with mNonzero, nNonzero
  have sumComputed := rationalAddValue.classes at
    a, b, m, c, d, n with mNonzero, nNonzero
  have negSumComputed := rationalNegValue.classes at
    n * a + m * c, n * b + m * d, m * n with mnNonzero
  have outerComputed := rationalAddValue.classes at
    a, b, m,
    n * b + m * d, n * a + m * c, m * n with
    mNonzero, mnNonzero
  have negYComputed := rationalNegValue.classes at c, d, n with nNonzero
  rw ← rationalAddValue.notation at sumComputed
  rw ← rationalNegValue.notation at negSumComputed
  rw ← rationalAddValue.notation at outerComputed
  rw ← rationalNegValue.notation at negYComputed
  have negSumShape : rationalNeg(rationalClassSum(a, b, m, c, d, n)) =
      rationalClassNeg(n * a + m * c, n * b + m * d, m * n)
    unfold rationalClassSum
    exact negSumComputed
  have outerShape : call2(rationalAdd, rationalClass(a, b, m),
      rationalClassNeg(n * a + m * c, n * b + m * d, m * n)) =
      rationalClassSum(a, b, m,
        n * b + m * d, n * a + m * c, m * n)
    unfold rationalClassNeg
    exact outerComputed
  have computedEquality : rationalClass(
      (m * n) * a + m * (n * b + m * d),
      (m * n) * b + m * (n * a + m * c),
      m * (m * n)) = rationalClass(d, c, n)
    apply rationalClass.eq
    . exact mul.nonzero at m, m * n with mNonzero, mnNonzero
    . exact nNonzero
    . ring
  simpa [xShape, yShape, rationalSubValue,
    rationalClassSum, rationalClassNeg] using computedEquality

theorem rationalNegValue.involutive (x : Rational)
  shows -(-x) = x
proof
  rw [rationalNegValue.notation, rationalNegValue.notation]
  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, xShape⟩ :=
    Rational.coordinates with assumption
  have first := rationalNegValue.classes with aNat, bNat, mNat, mNonzero
  have second := rationalNegValue.classes with bNat, aNat, mNat, mNonzero
  rw [xShape, first]
  simpa [rationalClassNeg] using second

-- The quotient operations form the same checked algebraic interface used by
-- ring normalization on the reals. All laws above were proved on ℚ.
instance rationalAdd.comm_monoid
  shows IsCommMonoid(ℚ, rationalAdd, rationalZero)
proof
  constructor
    constructor
      constructor
        exact rationalAdd.function
        intros A rationalA B rationalB C rationalC
        have typedA : Rational(A) by typecheck
        have typedB : Rational(B) by typecheck
        have typedC : Rational(C) by typecheck
        simpa [rationalAddValue.notation] using rationalAddValue.associative at A, B, C with typedA, typedB, typedC
      constructor
      . exact rationalZero.rational
      . intros A rationalA
        have typedA : Rational(A) by typecheck
        constructor
        . simpa [rationalAddValue.notation] using rationalAddValue.zero_left at A with typedA
        . simpa [rationalAddValue.notation] using rationalAddValue.zero_right at A with typedA
    intros A rationalA B rationalB
    have typedA : Rational(A) by typecheck
    have typedB : Rational(B) by typecheck
    simpa [rationalAddValue.notation] using rationalAddValue.commutative at A, B with typedA, typedB

instance rationalAdd.abelian_group
  shows IsAbelianGroup(ℚ, rationalAdd, rationalZero, rationalNeg)
proof
  constructor
    constructor
    . have additive := rationalAdd.comm_monoid
      simp [IsCommMonoid]
      constructor
      . exact rationalNeg.function
      . intros A rationalA
        have typedA : Rational(A) by typecheck
        constructor
        . simpa [rationalAddValue.notation, rationalNegValue.notation] using rationalAddValue.neg_left at A with typedA
        . simpa [rationalAddValue.notation, rationalNegValue.notation] using rationalAddValue.neg_right at A with typedA
  . have additive := rationalAdd.comm_monoid
    simp [IsCommMonoid]

instance rationalMul.monoid
  shows IsMonoid(ℚ, rationalMul, rationalOne)
proof
  constructor
    constructor
      exact rationalMul.function
      intros A rationalA B rationalB C rationalC
      have typedA : Rational(A) by typecheck
      have typedB : Rational(B) by typecheck
      have typedC : Rational(C) by typecheck
      simpa [rationalMulValue.notation] using rationalMulValue.associative at A, B, C with typedA, typedB, typedC
    constructor
    . exact rationalOne.rational
    . intros A rationalA
      have typedA : Rational(A) by typecheck
      constructor
      . simpa [rationalMulValue.notation] using rationalMulValue.one_left at A with typedA
      . simpa [rationalMulValue.notation] using rationalMulValue.one_right at A with typedA

instance rationalMul.distributive
  shows Distributive(ℚ, rationalAdd, rationalMul)
proof
  intros A rationalA B rationalB C rationalC
  have typedA : Rational(A) by typecheck
  have typedB : Rational(B) by typecheck
  have typedC : Rational(C) by typecheck
  constructor
  . simpa [rationalAddValue.notation, rationalMulValue.notation] using rationalMulValue.distributive_left at A, B, C with typedA, typedB, typedC
  . simpa [rationalAddValue.notation, rationalMulValue.notation] using rationalMulValue.distributive_right at A, B, C with typedA, typedB, typedC

instance rationalMul.commutative
  shows Commutative(ℚ, rationalMul)
proof
  intros A rationalA B rationalB
  have typedA : Rational(A) by typecheck
  have typedB : Rational(B) by typecheck
  simpa [rationalMulValue.notation] using rationalMulValue.commutative at A, B with typedA, typedB

instance rationals.comm_ring
  shows IsCommRing(ℚ, rationalAdd, rationalZero, rationalNeg, rationalMul, rationalOne)
proof
  constructor
    constructor
    . exact rationalAdd.abelian_group
    . constructor
      . exact rationalMul.monoid
      . exact rationalMul.distributive
  . exact rationalMul.commutative