-- Real analysis: Sequences
-- 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.Analysis.Sequences
import Metric

-- Section: Sequences
predicate RealSequence (u : Set) := FunctionBetween(u, ℕ, ℝ)

-- The epsilon definition: eventually every term lies in the open
-- ball of radius E around L.
predicate ConvergesTo (u : Set) (L : Real) :=
  RealSequence(u) ∧
  (∀ E ∈ ℝ, 0 < E →
    ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n →
      uₙ ∈ openBall(L, E))

predicate EventuallyEqual (u v : Set) :=
  ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n → uₙ = vₙ

def negSequence (u : Set) : Set :=
  compose(realNeg, u, ℕ, ℝ, ℝ)

def addSequence (u v : Set) : Set :=
  compose(realAdd, pairFunctions(u, v, ℕ, ℝ, ℝ), ℕ, ℝ × ℝ, ℝ)

def subSequence (u v : Set) : Set :=
  addSequence(u, negSequence(v))

def mulSequence (u v : Set) : Set :=
  compose(realMul, pairFunctions(u, v, ℕ, ℝ, ℝ), ℕ, ℝ × ℝ, ℝ)

def invSequence (u : Set) : Set :=
  compose(realInv, u, ℕ, ℝ, ℝ)

def divSequence (u v : Set) : Set :=
  compose(realDiv, pairFunctions(u, v, ℕ, ℝ, ℝ), ℕ, ℝ × ℝ, ℝ)

-- A positive scale strictly larger than |A|.
def limitScale (A : Real) : Real := abs(A) + 1

-- The radius E/(2C), named so epsilon proofs need not expose the concrete
-- implementation of division by a positive real.
def scaledRadius (E C : Real) : Real := half(E) / C

-- A uniform bound for the reciprocal factors near a nonzero limit L.
def inverseScale (L : Real) : Real :=
  realInvValue(half(abs(L))) * abs(realInvValue(L))

theorem limitScale.real (A : Real)
  shows Real(limitScale(A))
proof
  unfold limitScale
  exact realAddValue.real at abs(A), realOne with
    abs.real at A with assumption, realOne.real

theorem limitScale.positive (A : Real)
  shows 0 < limitScale(A)
proof
  have absReal := abs.real at A
  have oneStep := realLess.add_left with realZero.real, realOne.real, absReal, realZero.lt_one
  have scaleReal := realAddValue.real with absReal, realOne.real
  have zero := realAddValue.zero_right with absReal
  rw zero at oneStep
  unfold limitScale
  exact realLe.transitive_less at realZero, abs(A), abs(A) + 1 with
    realZero.real, absReal, scaleReal,
    abs.nonnegative at A with assumption, oneStep

theorem abs.lt_limitScale (A : Real)
  shows abs(A) < limitScale(A)
proof
  have absReal := abs.real at A
  have step := realLess.add_left with realZero.real, realOne.real, absReal, realZero.lt_one
  have zero := realAddValue.zero_right with absReal
  rw zero at step
  unfold limitScale
  exact step

theorem scaledRadius.real (E C : Real)
  shows Real(scaledRadius(E, C))
proof
  unfold scaledRadius
  typecheck

theorem scaledRadius.positive (E C : Real)
  requires positiveE : 0 < E
  requires positiveC : 0 < C
  shows 0 < scaledRadius(E, C)
proof
  have inversePositive := IsOrderedField.positive_inverse with reals.ordered_field, positiveC
  have halfPositive := half.positive with positiveE
  have inverseReal := realInvValue.real at C
  unfold scaledRadius
  rw realDiv.eq_mul_inv
  unfold realInvValue
  unfold realInvValue at inverseReal
  exact realMulValue.positive at half(E), realInv(C) with
    half.real at E with assumption,
    inverseReal,
    halfPositive, inversePositive

theorem scaledRadius.cancel (E C : Real)
  requires positiveC : 0 < C
  shows C * scaledRadius(E, C) = half(E)
proof
  have halfReal := half.real at E
  have inverseReal := realInvValue.real at C
  have nonzero : C ≠ 0
    intro equal
    rw equal at positiveC
    exact IsOrderedField.irreflexive with reals.ordered_field, positiveC
  have inverse := realInvValue.mul_right with nonzero
  have inverseLaw : C * realInvValue(C) = 1 by exact inverse
  have commute := realMulValue.commutative at C, half(E) with
    assumption, halfReal
  have firstAssoc := realMulValue.associative at
    C, half(E), realInvValue(C) with assumption, halfReal, inverseReal
  have secondAssoc := realMulValue.associative at
    half(E), C, realInvValue(C) with halfReal, assumption, inverseReal
  have one := realMulValue.one_right with halfReal
  unfold scaledRadius
  rw realDiv.eq_mul_inv
  calc
    C * (half(E) * realInvValue(C)) =
        (C * half(E)) * realInvValue(C) := by cc
    _ = (half(E) * C) * realInvValue(C) := by cc
    _ = half(E) * (C * realInvValue(C)) := secondAssoc
    _ = half(E) * 1 := by cc
    _ = half(E) := one

theorem inverseScale.real (L : Real)
  shows Real(inverseScale(L))
proof
  unfold inverseScale
  exact realMulValue.real at
    realInvValue(half(abs(L))), abs(realInvValue(L)) with
      realInvValue.real at half(abs(L)) with
        half.real at abs(L) with abs.real at L with assumption,
      abs.real at realInvValue(L) with realInvValue.real at L with assumption

theorem inverseScale.positive (L : Real)
  requires nonzero : L ≠ 0
  shows 0 < inverseScale(L)
proof
  have absLReal := abs.real at L
  have absLPositive := abs.positive_of_ne with nonzero
  have halfReal := half.real with absLReal
  have halfPositive := half.positive with absLPositive
  have inverseHalfPositive := realInvValue.positive with halfPositive
  have inverseLReal := realInvValue.real at L
  have inverseLNonzero := realInvValue.nonzero with nonzero
  have absInversePositive := abs.positive_of_ne with inverseLNonzero
  unfold inverseScale
  exact realMulValue.positive at
    realInvValue(half(abs(L))), abs(realInvValue(L)) with
      realInvValue.real at half(abs(L)) with halfReal,
      abs.real at realInvValue(L) with inverseLReal,
      inverseHalfPositive, absInversePositive

theorem ConvergesTo.sequence (u : Set) (L : Real)
  requires converges : ConvergesTo(u, L)
  shows RealSequence(u)
proof
  simp [ConvergesTo]

theorem ConvergesTo.eventually (u : Set) (L E : Real)
  requires converges : ConvergesTo(u, L)
  requires positive : 0 < E
  shows ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n →
    uₙ ∈ openBall(L, E)
proof
  rcases converges with ⟨sequence, eventually⟩
  exact eventually with E, positive

-- Two eventual properties hold together on a common tail. This packages the
-- elementary maximum-index argument for one or two sequences.
theorem ConvergesTo.common_eventually (u v : Set) (L M E D : Real)
  requires convergesL : ConvergesTo(u, L)
  requires convergesM : ConvergesTo(v, M)
  requires positiveE : 0 < E
  requires positiveD : 0 < D
  shows ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n →
    (uₙ ∈ openBall(L, E) ∧ vₙ ∈ openBall(M, D))
proof
  obtain ⟨N, nNatural, closeL⟩ := ConvergesTo.eventually with convergesL, positiveE
  obtain ⟨M0, mNatural, closeM⟩ := ConvergesTo.eventually with convergesM, positiveD
  have typedN : Nat(N) by exact nat.omega.backward at N with nNatural
  have typedM : Nat(M0) by exact nat.omega.backward at M0 with mNatural
  have comparison := Less.trichotomy with typedN, typedM
  cases comparison with nLessM | rest
  . have nLeM := Less.implies_LessEqual at N, M0 with
      typedN, typedM, nLessM
    witness M0
    constructor
    . exact mNatural
    . intros n nInNaturals mLeN
      have nLeLittleN := LessEqual.transitive with nLeM, mLeN
      constructor
      . exact closeL with n, nInNaturals, nLeLittleN
      . exact closeM with n, nInNaturals, mLeN
  . cases rest with equal | mLessN
    . witness N
      constructor
      . exact nNatural
      . intros n nInNaturals nLeLittleN
        have mLeLittleN : M0 ≤ n by rwa ← equal
        constructor
        . exact closeL with n, nInNaturals, nLeLittleN
        . exact closeM with n, nInNaturals, mLeLittleN
    . have mLeN := Less.implies_LessEqual at M0, N with
        typedM, typedN, mLessN
      witness N
      constructor
      . exact nNatural
      . intros n nInNaturals nLeLittleN
        have mLeLittleN := LessEqual.transitive with mLeN, nLeLittleN
        constructor
        . exact closeL with n, nInNaturals, nLeLittleN
        . exact closeM with n, nInNaturals, mLeLittleN

theorem RealSequence.value (u : Set, n : Nat)
  requires sequence : RealSequence(u)
  shows Real(uₙ)
proof
  unfold RealSequence at sequence
  have nInNaturals : n ∈ ℕ by simp [Nat]
  obtain ⟨A, realA, mapped⟩ := FunctionBetween.exists_value with sequence, nInNaturals
  have applied := FunctionBetween.apply_value with sequence, mapped
  rw applied
  exact realA

instance RealSequence.value_type (u : Set, n : Nat)
  requires sequence : RealSequence(u)
  shows Real(uₙ)
proof
  exact RealSequence.value with sequence

theorem negSequence.sequence (u : Set)
  requires sequence : RealSequence(u)
  shows RealSequence(negSequence(u))
proof
  unfold RealSequence at sequence
  unfold RealSequence
  unfold negSequence
  exact compose.function with sequence, realNeg.function

theorem negSequence.value (u : Set, n : Nat)
  requires sequence : RealSequence(u)
  requires valueReal : Real(uₙ)
  shows negSequence(u)[n] = -uₙ
proof
  have nNatural : n ∈ ℕ by simp [Nat]
  have function : u : ℕ → ℝ by exact sequence
  have value := compose.apply with function, realNeg.function, nNatural
  simp [negSequence]

theorem addSequence.sequence (u v : Set)
  requires sequenceU : RealSequence(u)
  requires sequenceV : RealSequence(v)
  shows RealSequence(addSequence(u, v))
proof
  have functionU : u : ℕ → ℝ by exact sequenceU
  have functionV : v : ℕ → ℝ by exact sequenceV
  have paired := pairFunctions.function with functionU, functionV
  unfold RealSequence
  unfold addSequence
  exact compose.function with paired, realAdd.function

theorem addSequence.value (u v : Set, n : Nat)
  requires sequenceU : RealSequence(u)
  requires sequenceV : RealSequence(v)
  requires valueUReal : Real(uₙ)
  requires valueVReal : Real(vₙ)
  shows addSequence(u, v)[n] = uₙ + vₙ
proof
  have nNatural : n ∈ ℕ by simp [Nat]
  have functionU : u : ℕ → ℝ by exact sequenceU
  have functionV : v : ℕ → ℝ by exact sequenceV
  have paired := pairFunctions.function with functionU, functionV
  have outer := compose.apply with paired, realAdd.function, nNatural
  have pairValue := pairFunctions.apply with functionU, functionV, nNatural
  unfold addSequence
  rw pairValue at outer
  simp [call2]

theorem mulSequence.sequence (u v : Set)
  requires sequenceU : RealSequence(u)
  requires sequenceV : RealSequence(v)
  shows RealSequence(mulSequence(u, v))
proof
  have functionU : u : ℕ → ℝ by exact sequenceU
  have functionV : v : ℕ → ℝ by exact sequenceV
  have paired := pairFunctions.function with functionU, functionV
  unfold RealSequence
  unfold mulSequence
  exact compose.function with paired, realMul.function

theorem mulSequence.value (u v : Set, n : Nat)
  requires sequenceU : RealSequence(u)
  requires sequenceV : RealSequence(v)
  requires valueUReal : Real(uₙ)
  requires valueVReal : Real(vₙ)
  shows mulSequence(u, v)[n] = uₙ * vₙ
proof
  have nNatural : n ∈ ℕ by simp [Nat]
  have functionU : u : ℕ → ℝ by exact sequenceU
  have functionV : v : ℕ → ℝ by exact sequenceV
  have paired := pairFunctions.function with functionU, functionV
  have outer := compose.apply with paired, realMul.function, nNatural
  have pairValue := pairFunctions.apply with functionU, functionV, nNatural
  unfold mulSequence
  rw pairValue at outer
  simp [call2]

theorem invSequence.sequence (u : Set)
  requires sequence : RealSequence(u)
  shows RealSequence(invSequence(u))
proof
  unfold RealSequence at sequence
  unfold RealSequence
  unfold invSequence
  exact compose.function with sequence, realInv.function

theorem invSequence.value (u : Set, n : Nat)
  requires sequence : RealSequence(u)
  shows invSequence(u)[n] = realInvValue(uₙ)
proof
  have nNatural : n ∈ ℕ by simp [Nat]
  have function : u : ℕ → ℝ by exact sequence
  have value := compose.apply with function, realInv.function, nNatural
  simp [invSequence, realInvValue]

theorem divSequence.sequence (u v : Set)
  requires sequenceU : RealSequence(u)
  requires sequenceV : RealSequence(v)
  shows RealSequence(divSequence(u, v))
proof
  have functionU : u : ℕ → ℝ by exact sequenceU
  have functionV : v : ℕ → ℝ by exact sequenceV
  have paired := pairFunctions.function with functionU, functionV
  unfold RealSequence
  unfold divSequence
  exact compose.function with paired, realDiv.function

theorem divSequence.value (u v : Set, n : Nat)
  requires sequenceU : RealSequence(u)
  requires sequenceV : RealSequence(v)
  shows divSequence(u, v)[n] = uₙ / vₙ
proof
  have nNatural : n ∈ ℕ by simp [Nat]
  have functionU : u : ℕ → ℝ by exact sequenceU
  have functionV : v : ℕ → ℝ by exact sequenceV
  have paired := pairFunctions.function with functionU, functionV
  have outer := compose.apply with paired, realDiv.function, nNatural
  have pairValue := pairFunctions.apply with functionU, functionV, nNatural
  unfold divSequence
  rw pairValue at outer
  simp [call2]

theorem subSequence.sequence (u v : Set)
  requires sequenceU : RealSequence(u)
  requires sequenceV : RealSequence(v)
  shows RealSequence(subSequence(u, v))
proof
  have negSequenceV := negSequence.sequence with sequenceV
  unfold subSequence
  exact addSequence.sequence with sequenceU, negSequenceV

theorem subSequence.value (u v : Set, n : Nat)
  requires sequenceU : RealSequence(u)
  requires sequenceV : RealSequence(v)
  requires valueUReal : Real(uₙ)
  requires valueVReal : Real(vₙ)
  shows subSequence(u, v)[n] = uₙ - vₙ
proof
  have negSequenceV := negSequence.sequence with sequenceV
  have negValueReal := RealSequence.value with negSequenceV
  have sumValue := addSequence.value with sequenceU, negSequenceV, valueUReal, negValueReal
  have negValue := negSequence.value with sequenceV, valueVReal
  unfold subSequence
  unfold realSubValue
  rw negValue at sumValue
  exact sumValue

theorem ConvergesTo.neg (u : Set) (L : Real)
  requires converges : ConvergesTo(u, L)
  shows ConvergesTo(negSequence(u), -L)
proof
  have sequence := ConvergesTo.sequence with converges
  have negLimitReal := realNegValue.real at L
  constructor
  . exact negSequence.sequence with sequence
  . intros E realE positive
    have typedE : Real(E) by exact realE
    obtain ⟨N, nNatural, close⟩ := ConvergesTo.eventually with converges, positive
    witness N
    constructor
    . exact nNatural
    . intros n nInNaturals nAfterN
      have typedN : Nat(n) by exact nat.omega.backward at n with nInNaturals
      have valueInReals := RealSequence.value with sequence
      have typedValue : Real(u(n)) by exact valueInReals
      have near := close with n, nInNaturals, nAfterN
      have nearData := openBall.membership.forward at
        L, E, u(n) with near
      rcases nearData with ⟨realValue, within⟩
      have valueShape := negSequence.value with sequence
      have negValueReal := realNegValue.real with typedValue
      have negDistance := dist.neg at u(n), L with
        typedValue, assumption
      apply openBall.membership.backward
      constructor
      . rw valueShape
        exact negValueReal
      . rw valueShape
        rwa negDistance

theorem ConvergesTo.add (u v : Set) (L M : Real)
  requires convergesU : ConvergesTo(u, L)
  requires convergesV : ConvergesTo(v, M)
  shows ConvergesTo(addSequence(u, v), L + M)
proof
  have sequenceU := ConvergesTo.sequence with convergesU
  have sequenceV := ConvergesTo.sequence with convergesV
  have sumLimitReal := realAddValue.real at L, M with *
  constructor
  . exact addSequence.sequence with sequenceU, sequenceV
  . intros E realE positive
    have typedE : Real(E) by exact realE
    have radiusReal := half.real with typedE
    have radiusPositive := half.positive with positive
    obtain ⟨N, nNatural, closeBoth⟩ := ConvergesTo.common_eventually with
      convergesU, convergesV, radiusPositive, radiusPositive
    witness N
    constructor
    . exact nNatural
    . intros n nInNaturals nAfterN
      have typedN : Nat(n) by exact nat.omega.backward at n with nInNaturals
      obtain ⟨nearU, nearV⟩ := closeBoth with n, nInNaturals, nAfterN
      have uInReals := RealSequence.value with sequenceU
      have vInReals := RealSequence.value with sequenceV
      have typedU : Real(u(n)) by exact uInReals
      have typedV : Real(v(n)) by exact vInReals
      have uData := openBall.membership.forward at
        L, half(E), u(n) with nearU
      have vData := openBall.membership.forward at
        M, half(E), v(n) with nearV
      rcases uData with ⟨realU, closeU⟩
      rcases vData with ⟨realV, closeV⟩
      have sumValueReal := realAddValue.real with typedU, typedV
      have firstDistanceReal := dist.real at u(n), L with
        typedU, assumption
      have secondDistanceReal := dist.real at v(n), M with
        typedV, assumption
      have distanceSumReal := realAddValue.real with firstDistanceReal, secondDistanceReal
      have totalDistanceReal := dist.real with sumValueReal, sumLimitReal
      have distanceBound := dist.add_add at
        u(n), v(n), L, M with
          typedU, typedV, *{2}
      have radiusSumBound := realLess.add with
        firstDistanceReal, radiusReal, secondDistanceReal, radiusReal, closeU, closeV
      have doubled := half.add_self with typedE
      rw doubled at radiusSumBound
      have within := realLe.transitive_less with
        totalDistanceReal, distanceSumReal, typedE, distanceBound, radiusSumBound
      have valueShape := addSequence.value with sequenceU, sequenceV
      apply openBall.membership.backward
      constructor
      . rw valueShape
        unfold call2
        unfold call2 at sumValueReal
        exact sumValueReal
      . rw valueShape
        unfold call2
        unfold call2 at within
        exact within

-- Products of convergent real sequences converge to the product of their
-- limits.  The estimate is the one used in a handwritten proof:
--
--   |uₙvₙ - LM| ≤ |uₙ| |vₙ - M| + |M| |uₙ - L|.
--
-- First make uₙ locally bounded, then assign half of epsilon to each term.
theorem ConvergesTo.mul (u v : Set) (L M : Real)
  requires convergesU : ConvergesTo(u, L)
  requires convergesV : ConvergesTo(v, M)
  shows ConvergesTo(mulSequence(u, v), L * M)
proof
  have sequenceU := ConvergesTo.sequence with convergesU
  have sequenceV := ConvergesTo.sequence with convergesV
  have productLimitReal := realMulValue.real at L, M with
    *{2}
  constructor
  . exact mulSequence.sequence with sequenceU, sequenceV
  . intros E realE positiveE
    have typedE : Real(E) by exact realE
    have scaleMReal := limitScale.real at M
    have scaleMPositive := limitScale.positive at M
    have radiusUReal := scaledRadius.real with typedE, scaleMReal
    have radiusUPositive := scaledRadius.positive with positiveE, scaleMPositive
    have absLReal := abs.real at L
    have boundReal := realAddValue.real with radiusUReal, absLReal
    have radiusAboveAbsL := realLess.add_right with realZero.real, radiusUReal, absLReal, radiusUPositive
    have zeroPlusAbsL := realAddValue.zero_left with absLReal
    rw zeroPlusAbsL at radiusAboveAbsL
    have boundPositive := realLe.transitive_less at
      realZero, abs(L), scaledRadius(E, limitScale(M)) + abs(L) with
        realZero.real, absLReal, boundReal,
        abs.nonnegative at L with assumption, radiusAboveAbsL
    have radiusVReal := scaledRadius.real with typedE, boundReal
    have radiusVPositive := scaledRadius.positive with positiveE, boundPositive
    obtain ⟨N, nNatural, closeBoth⟩ := ConvergesTo.common_eventually with
      convergesU, convergesV, radiusUPositive, radiusVPositive
    witness N
    constructor
    . exact nNatural
    . intros n nInNaturals nAfterN
      have typedN : Nat(n) by exact nat.omega.backward at n with nInNaturals
      obtain ⟨nearU, nearV⟩ := closeBoth with n, nInNaturals, nAfterN
      have typedU := RealSequence.value with sequenceU
      have typedV := RealSequence.value with sequenceV
      have uData := openBall.membership.forward at
        L, scaledRadius(E, limitScale(M)), uₙ with nearU
      have vData := openBall.membership.forward at
        M, scaledRadius(E, scaledRadius(E, limitScale(M)) + abs(L)), vₙ
        with nearV
      rcases uData with ⟨realU, closeU⟩
      rcases vData with ⟨realV, closeV⟩

      -- Closeness to L supplies the local bound |uₙ| < radiusU + |L|.
      have absUReal := abs.real with typedU
      have distUReal := dist.real at uₙ, L with typedU
      have distVReal := dist.real at vₙ, M with typedV
      have absUBound := abs.le_dist_add_abs at uₙ, L with
        typedU, assumption
      have closeUWithAbsL := realLess.add_right with distUReal, radiusUReal, absLReal, closeU
      have distPlusAbsReal := realAddValue.real with distUReal, absLReal
      have uBounded := realLe.transitive_less with
        absUReal, distPlusAbsReal, boundReal, absUBound, closeUWithAbsL

      -- Each summand in the product estimate is strictly below E/2.
      have uBoundedLe := realLess.implies_le with absUReal, boundReal, uBounded
      have distVNonnegative := dist.nonnegative at vₙ, M with
        typedV, assumption
      have firstWeak := realLe.mul_right_of_nonnegative with
        absUReal, boundReal, distVReal, uBoundedLe, distVNonnegative
      have firstStrict := realLess.mul_left_of_positive with
        distVReal, radiusVReal, boundReal, closeV, boundPositive
      have firstTermReal := realMulValue.real with absUReal, distVReal
      have firstMiddleReal := realMulValue.real with boundReal, distVReal
      have firstUpperReal := realMulValue.real with boundReal, radiusVReal
      have firstBelowProduct := realLe.transitive_less with
        firstTermReal, firstMiddleReal, firstUpperReal, firstWeak, firstStrict
      have firstCancellation := scaledRadius.cancel with typedE, boundReal, boundPositive
      rw firstCancellation at firstBelowProduct

      have absMReal := abs.real at M
      have absMLess := abs.lt_limitScale at M
      have absMLe := realLess.implies_le with absMReal, scaleMReal, absMLess
      have distUNonnegative := dist.nonnegative at uₙ, L with
        typedU, assumption
      have secondWeak := realLe.mul_right_of_nonnegative with
        absMReal, scaleMReal, distUReal, absMLe, distUNonnegative
      have secondStrict := realLess.mul_left_of_positive with
        distUReal, radiusUReal, scaleMReal, closeU, scaleMPositive
      have secondTermReal := realMulValue.real with absMReal, distUReal
      have secondMiddleReal := realMulValue.real with scaleMReal, distUReal
      have secondUpperReal := realMulValue.real with scaleMReal, radiusUReal
      have secondBelowProduct := realLe.transitive_less with
        secondTermReal, secondMiddleReal, secondUpperReal, secondWeak, secondStrict
      have secondCancellation := scaledRadius.cancel with typedE, scaleMReal, scaleMPositive
      rw secondCancellation at secondBelowProduct

      have estimate := dist.mul_mul at uₙ, vₙ, L, M with
        typedU, typedV, *{2}
      have halfReal := half.real with typedE
      have sumBelow := realLess.add with
        firstTermReal, halfReal, secondTermReal, halfReal, firstBelowProduct, secondBelowProduct
      have doubled := half.add_self with typedE
      rw doubled at sumBelow
      have productValueReal := realMulValue.real with typedU, typedV
      have totalDistanceReal := dist.real with productValueReal, productLimitReal
      have estimateSumReal := realAddValue.real with firstTermReal, secondTermReal
      have within := realLe.transitive_less with
        totalDistanceReal, estimateSumReal, typedE, estimate, sumBelow
      have valueShape := mulSequence.value with sequenceU, sequenceV, typedU, typedV
      apply openBall.membership.backward
      constructor
      . rw valueShape
        exact productValueReal
      . rw valueShape
        exact within

-- A convergent sequence may be inverted when its limit is nonzero.  The
-- proof is the textbook one: first keep the sequence at least |L|/2 away
-- from zero, then use
--
--   |uₙ⁻¹ - L⁻¹| = |uₙ - L| |uₙ⁻¹| |L⁻¹|.
theorem ConvergesTo.inv (u : Set) (L : Real)
  requires converges : ConvergesTo(u, L)
  requires nonzero : L ≠ 0
  shows ConvergesTo(invSequence(u), realInvValue(L))
proof
  have sequence := ConvergesTo.sequence with converges
  have inverseLimitReal := realInvValue.real at L
  constructor
  . exact invSequence.sequence with sequence
  . intros E realE positiveE
    have typedE : Real(E) by exact realE
    have absLReal := abs.real at L
    have absLPositive := abs.positive_of_ne with nonzero
    have halfAbsLReal := half.real with absLReal
    have halfAbsLPositive := half.positive with absLPositive
    have scaleReal := inverseScale.real at L
    have scalePositive := inverseScale.positive with nonzero
    have radiusReal := scaledRadius.real with typedE, scaleReal
    have radiusPositive := scaledRadius.positive with positiveE, scalePositive
    obtain ⟨N, nNatural, closeBoth⟩ := ConvergesTo.common_eventually with
      converges, converges, halfAbsLPositive, radiusPositive
    witness N
    constructor
    . exact nNatural
    . intros n nInNaturals nAfterN
      have typedN : Nat(n) by exact nat.omega.backward at n with nInNaturals
      obtain ⟨nearZero, nearE⟩ := closeBoth with n, nInNaturals, nAfterN
      have typedU := RealSequence.value with sequence
      have zeroData := openBall.membership.forward at
        L, half(abs(L)), uₙ with nearZero
      have epsilonData := openBall.membership.forward at
        L, scaledRadius(E, inverseScale(L)), uₙ with nearE
      rcases zeroData with ⟨realU, closeZero⟩
      rcases epsilonData with ⟨realUAgain, closeE⟩

      have lower := abs.half_lt_of_dist_lt_half with typedU, nonzero, closeZero
      have nonzeroU : uₙ ≠ 0
        intro equal
        have absoluteZero := abs.zero
        rw [equal, absoluteZero] at lower
        have irreflexive := realLess.irreflexive_on
        have cycle := realLess.transitive with
          realZero.real, halfAbsLReal, realZero.real, halfAbsLPositive, lower
        exact irreflexive with realZero, cycle

      -- Reciprocation reverses the lower bound |L|/2 < |uₙ|.
      have inverseBound := realInvValue.antitone_positive with halfAbsLReal, halfAbsLPositive, lower
      have absInverseU := abs.inv with typedU, nonzeroU
      rw ← absInverseU at inverseBound

      have inverseLReal := realInvValue.real at L
      have inverseLNonzero := realInvValue.nonzero with nonzero
      have absInverseLReal := abs.real with inverseLReal
      have absInverseLPositive := abs.positive_of_ne with inverseLNonzero
      have factorBound := realLess.mul_right_of_positive at
        abs(realInvValue(uₙ)), realInvValue(half(abs(L))),
        abs(realInvValue(L)) with
          abs.real at realInvValue(uₙ) with
            realInvValue.real at uₙ with typedU,
          realInvValue.real at half(abs(L)) with halfAbsLReal,
          absInverseLReal, inverseBound, absInverseLPositive
      have factorBoundScale : abs(realInvValue(uₙ)) *
          abs(realInvValue(L)) < inverseScale(L)
        unfold inverseScale
        exact factorBound

      -- Multiply the two strict estimates, using nonnegativity of distance
      -- for the weak first step.
      have distanceReal := dist.real at uₙ, L with typedU
      have factorReal := realMulValue.real at
        abs(realInvValue(uₙ)), abs(realInvValue(L)) with
          abs.real at realInvValue(uₙ) with
            realInvValue.real at uₙ with typedU,
          absInverseLReal
      have distanceNonnegative := dist.nonnegative at uₙ, L with
        typedU, assumption
      have factorLe := realLess.implies_le with factorReal, scaleReal, factorBoundScale
      have weakProduct := realLe.mul_left_of_nonnegative with
        factorReal, scaleReal, distanceReal, factorLe, distanceNonnegative
      have strictProduct := realLess.mul_right_of_positive with
        distanceReal, radiusReal, scaleReal, closeE, scalePositive
      have lowerProductReal := realMulValue.real with distanceReal, factorReal
      have middleProductReal := realMulValue.real with distanceReal, scaleReal
      have upperProductReal := realMulValue.real with radiusReal, scaleReal
      have productBelow := realLe.transitive_less with
        lowerProductReal, middleProductReal, upperProductReal, weakProduct, strictProduct
      have cancellation := scaledRadius.cancel with typedE, scaleReal, scalePositive
      have commute := realMulValue.commutative with radiusReal, scaleReal
      rw [commute, cancellation] at productBelow
      have halfBelowE := half.lt_self with typedE, positiveE
      have halfReal := half.real with typedE
      have productBelowE := realLess.transitive with
        lowerProductReal, halfReal, typedE, productBelow, halfBelowE
      have inverseDistance := dist.inv_inv with typedU, nonzeroU, nonzero
      rw ← inverseDistance at productBelowE

      have valueShape := invSequence.value with sequence
      apply openBall.membership.backward
      constructor
      . rw valueShape
        exact realInvValue.real with typedU
      . rw valueShape
        exact productBelowE

theorem ConvergesTo.sub (u v : Set) (L M : Real)
  requires convergesU : ConvergesTo(u, L)
  requires convergesV : ConvergesTo(v, M)
  shows ConvergesTo(subSequence(u, v), L - M)
proof
  have negConverges := ConvergesTo.neg with convergesV
  have sumConverges := ConvergesTo.add with convergesU, negConverges
  unfold subSequence
  unfold realSubValue
  exact sumConverges

-- A real sequence has at most one limit. The proof uses the ball of radius
-- half the distance between two proposed limits.
theorem ConvergesTo.unique (u : Set) (L M : Real)
  requires convergesL : ConvergesTo(u, L)
  requires convergesM : ConvergesTo(u, M)
  shows L = M
proof
  by_contra unequal
  have distancePositive := dist.positive_of_ne with unequal
  have radiusPositive := half.positive with distancePositive
  obtain ⟨n, nNatural, closeBoth⟩ := ConvergesTo.common_eventually with
    convergesL, convergesM, radiusPositive, radiusPositive
  have typedN : Nat(n) by exact nat.omega.backward at n with nNatural
  have nLeN := LessEqual.reflexive with typedN
  obtain ⟨nearL, nearM⟩ := closeBoth with n, nNatural, nLeN
  have sequence := ConvergesTo.sequence with convergesL
  have valueInReals := RealSequence.value with sequence
  have equal := openBall.half_radius_unique with nearL, nearM
  exact unequal with equal

def constantSequence (L : Real) : Set :=
  { p ∈ ℕ × ℝ | ∃ n ∈ ℕ, p = (n ↦ L) }

theorem constantSequence.relates (L : Real, n : Nat)
  shows relates(constantSequence(L), n, L)
proof
  have nInNaturals : n ∈ ℕ by simp [Nat]
  have lInReals : L ∈ ℝ by simp [Real]
  unfold relates
  apply constantSequence.membership.backward
  constructor
  . exact product.pair with nInNaturals, lInReals
  . refine ⟨n, nInNaturals, rfl⟩

theorem constantSequence.function (L : Real)
  shows constantSequence(L) : ℕ → ℝ
proof
  constructor
    intros p member
    obtain ⟨bounded, witnesses⟩ := constantSequence.membership.forward with member
    exact bounded
  . constructor
      intros n A nA B nB
      unfold relates at nA
      obtain ⟨_, i, iNatural, firstShape⟩ := constantSequence.membership.forward with nA
      unfold relates at nB
      obtain ⟨_, j, jNatural, secondShape⟩ := constantSequence.membership.forward with nB
      have firstCoordinates := orderedPair.injective with firstShape
      have secondCoordinates := orderedPair.injective with secondShape
      rcases firstCoordinates with ⟨_, equalA⟩
      rcases secondCoordinates with ⟨_, equalB⟩
      rw [equalA, equalB]
      rfl
    . intros n nNatural
      witness L
      constructor
      . settle with Real
      . have typedN : Nat(n)
          exact nNatural
        exact constantSequence.relates with assumption, typedN

theorem constantSequence.sequence (L : Real)
  shows RealSequence(constantSequence(L))
proof
  unfold RealSequence
  exact constantSequence.function with assumption

theorem constantSequence.value (L : Real, n : Nat)
  shows constantSequence(L)(n) = L
proof
  have function := constantSequence.function at L
  have mapped := constantSequence.relates with *
  exact FunctionBetween.apply_value with function, mapped

theorem constantSequence.converges (L : Real)
  shows ConvergesTo(constantSequence(L), L)
proof
  constructor
  . exact constantSequence.sequence at L
  . intros E realE positive
    witness 0
    constructor
    . exact nat.omega.forward at 0 with Naturals.constructor.zero
    . intros n nNatural zeroLeN
      have typedN : Nat(n) by exact nNatural
      have value := constantSequence.value with assumption, typedN
      rw value
      exact openBall.center with positive

-- Changing finitely many terms cannot change the limit of a sequence.
theorem ConvergesTo.eventually_equal (u v : Set) (L : Real)
  requires converges : ConvergesTo(u, L)
  requires sequenceV : RealSequence(v)
  requires eventuallyEqual : EventuallyEqual(u, v)
  shows ConvergesTo(v, L)
proof
  rcases converges with ⟨sequenceU, eventuallyClose⟩
  obtain ⟨M, mNatural, equalAfterM⟩ := eventuallyEqual
  have typedM : Nat(M) by exact nat.omega.backward at M with mNatural
  constructor
  . exact sequenceV
  . intros E realE positive
    obtain ⟨N, nNatural, closeAfterN⟩ :=
      eventuallyClose with E, realE, positive
    have typedN : Nat(N) by exact nat.omega.backward at N with nNatural
    have comparison := Less.trichotomy with typedN, typedM
    cases comparison with nLessM | rest
    . witness M
      constructor
      . exact mNatural
      . intros n nInNaturals mLeN
        have nLeM := Less.implies_LessEqual with nLessM
        have nLeLittleN := LessEqual.transitive with nLeM, mLeN
        have close := closeAfterN with n, nInNaturals, nLeLittleN
        have equal := equalAfterM with n, nInNaturals, mLeN
        rwa equal at close
    . cases rest with equalNM | mLessN
      . witness N
        constructor
        . exact nNatural
        . intros n nInNaturals nLeLittleN
          have close := closeAfterN with n, nInNaturals, nLeLittleN
          have mLeLittleN : M ≤ n by rwa ← equalNM
          have equal := equalAfterM with n, nInNaturals, mLeLittleN
          rwa equal at close

      . witness N
        constructor
        . exact nNatural
        . intros n nInNaturals nLeLittleN
          have mLeN := Less.implies_LessEqual with typedM, typedN, mLessN
          have mLeLittleN := LessEqual.transitive with typedM, typedN, mLeN, nLeLittleN
          have close := closeAfterN with n, nInNaturals, nLeLittleN
          have equal := equalAfterM with n, nInNaturals, mLeLittleN
          rwa equal at close

-- Quotients now follow from the product and reciprocal rules.  The short
-- proof is precisely the payoff of treating `/` as the field operation.
theorem ConvergesTo.div (u v : Set) (L M : Real)
  requires convergesU : ConvergesTo(u, L)
  requires convergesV : ConvergesTo(v, M)
  requires nonzeroM : M ≠ 0
  shows ConvergesTo(divSequence(u, v), L / M)
proof
  have sequenceU := ConvergesTo.sequence with convergesU
  have sequenceV := ConvergesTo.sequence with convergesV
  have inverseConverges := ConvergesTo.inv with convergesV, nonzeroM
  have productConverges := ConvergesTo.mul with convergesU, inverseConverges
  have limitShape := realDiv.eq_mul_inv at L, M with *
  rw limitShape
  apply ConvergesTo.eventually_equal with productConverges
  . exact divSequence.sequence with sequenceU, sequenceV
    witness 0
    constructor
    . exact nat.omega.forward at 0 with Naturals.constructor.zero
    . intros n nNatural zeroLeN
      have typedN : Nat(n) by exact nat.omega.backward at n with nNatural
      have inverseSequence := invSequence.sequence with sequenceV
      have inverseValueReal := RealSequence.value with inverseSequence
      have valueUReal := RealSequence.value with sequenceU
      have valueVReal := RealSequence.value with sequenceV
      have mulValue := mulSequence.value with sequenceU, inverseSequence, valueUReal, inverseValueReal
      have invValue := invSequence.value with sequenceV
      have divValue := divSequence.value with sequenceU, sequenceV
      have quotientValue := realDiv.eq_mul_inv with valueUReal, valueVReal
      rw [mulValue, invValue, divValue, quotientValue]
      rfl

-- Section: OrderLimits
theorem openBall.order_characterization (X C E : Real)
  shows X ∈ openBall(C, E) ↔ (C - E < X ∧ X < C + E)
proof
  have differenceReal := realSubValue.real at X, C with *
  have negDifferenceReal := realNegValue.real with differenceReal
  have negDifference : -(X - C) = C - X
    unfold realSubValue
    have negCReal := realNegValue.real at C
    have negXReal := realNegValue.real at X
    have distributed := realNegValue.add at X, -C with
      assumption, negCReal
    have involutive := realNegValue.involutive at C
    have commute := realAddValue.commutative at -X, C with
      negXReal, assumption
    cc
  constructor
  . intro member
    obtain ⟨_, within⟩ := openBall.membership.forward with member
    unfold dist at within
    have upperDifference := realLe.transitive_less at
      X - C, abs(X - C), E with
        differenceReal, abs.real at X - C with differenceReal, assumption,
        abs.upper at X - C with differenceReal, within
    have lowerDifference := realLe.transitive_less at
      -(X - C), abs(X - C), E with
        negDifferenceReal, abs.real at X - C with differenceReal, assumption,
        abs.upper_neg at X - C with differenceReal, within
    have upper := realLess.add_right at X - C, E, C with
      differenceReal, *{2}, upperDifference
    have lower := realLess.add_right at -(X - C), E, X with
      negDifferenceReal, *{2}, lowerDifference
    have upperLeft := realSubValue.add_right_cancel at X, C with
      *{2}
    have upperRight := realAddValue.commutative at E, C with
      *{2}
    rw [upperLeft, upperRight] at upper
    rw negDifference at lower
    have lowerLeft := realSubValue.add_right_cancel at C, X with
      *{2}
    rw lowerLeft at lower
    have lowerRight := realAddValue.commutative at E, X with
      *{2}
    rw lowerRight at lower
    have lowerShifted : (C - E) + E < X + E
      have cancel := realSubValue.add_right_cancel at C, E with
        *{2}
      rwa cancel
    have cMinusEReal := realSubValue.real at C, E with *
    have lowerFinal := realLess.add_right_iff.forward with lowerShifted
    constructor
    . exact lowerFinal
    . exact upper
  . intro bounds
    rcases bounds with ⟨lower, upper⟩
    have sumCEReal := realAddValue.real at C, E with *
    have sumXEReal := realAddValue.real at X, E with *
    have negCReal := realNegValue.real at C
    have negXReal := realNegValue.real at X
    have cMinusEReal := realSubValue.real at C, E with *
    have upperDifference := realLess.add_right at X, C + E, -C with
      assumption, sumCEReal, negCReal, upper
    have lowerDifference := realLess.add_right at C - E, X, E with
      cMinusEReal, *{2}, lower
    have cancelCE := realSubValue.add_right_cancel at C, E with
      *{2}
    rw cancelCE at lowerDifference
    have lowerDifferenceAgain := realLess.add_right at
      C, X + E, -X with
        assumption, sumXEReal, negXReal, lowerDifference
    have commuteCE := realAddValue.commutative at C, E with
      *{2}
    rw commuteCE at upperDifference
    have cancelEC := realSubValue.add_cancel_right at E, C with
      *{2}
    unfold realSubValue at cancelEC
    rw cancelEC at upperDifference
    have commuteXE := realAddValue.commutative at X, E with
      *{2}
    rw commuteXE at lowerDifferenceAgain
    have cancelEX := realSubValue.add_cancel_right at E, X with
      *{2}
    unfold realSubValue at cancelEX
    rw cancelEX at lowerDifferenceAgain
    have sign := Real.sign_cases with differenceReal
    apply openBall.membership.backward
    constructor
    . settle with Real
    . unfold dist
      cases sign with nonpositive | nonnegative
      . have nonpositiveLe := realLe.of_subset at X - C, realZero with
          differenceReal, realZero.real, nonpositive
        have absolute := abs.of_nonpositive with nonpositiveLe
        rw [absolute, negDifference]
        unfold realSubValue
        exact lowerDifferenceAgain
      . have nonnegativeLe := realLe.of_subset at realZero, X - C with
          realZero.real, differenceReal, nonnegative
        have absolute := abs.of_nonnegative with nonnegativeLe
        rw absolute
        unfold realSubValue
        exact upperDifference

-- A sequence is eventually bounded when one positive real bounds the
-- absolute values of all terms in a tail.
predicate EventuallyBounded (u : Set) :=
  RealSequence(u) ∧
  (∃ B ∈ ℝ, 0 < B ∧
    (∃ N ∈ ℕ, (∀ n ∈ ℕ, N ≤ n →
      u(n) ∈ openBall(realZero, B))))

predicate NonnegativeTerms (u : Set) :=
  ∀ n ∈ ℕ, RealLe(realZero, u(n))

predicate PointwiseLE (u v : Set) :=
  ∀ n ∈ ℕ, RealLe(u(n), v(n))

predicate BoundedAboveBy (u : Set) (B : Real) :=
  ∀ n ∈ ℕ, RealLe(u(n), B)

predicate BoundedBelowBy (u : Set) (A : Real) :=
  ∀ n ∈ ℕ, RealLe(A, u(n))

predicate UnitIntervalTerms (u : Set) :=
  ∀ n ∈ ℕ,
    RealLe(realZero, u(n)) ∧ RealLe(u(n), realOne)

-- Every convergent sequence is bounded on a tail.  The familiar estimate
-- |uₙ| ≤ |uₙ - L| + |L| gives the explicit bound |L| + 1.
-- A value within half of E of C on both sides lies in the open E-ball around C.
theorem openBall.of_half_bounds (Q C E : Real)
  requires positive : 0 < E
  requires low : C - half(E) ≤ Q
  requires high : Q ≤ C + half(E)
  shows Q ∈ openBall(C, E)
proof
  have halfLess := half.lt_self with *
  have bounds : C - E < Q ∧ Q < C + E
    constructor
    . linarith
    . linarith
  exact openBall.order_characterization.backward with bounds

theorem ConvergesTo.eventually_bounded (u : Set) (L : Real)
  requires converges : ConvergesTo(u, L)
  shows EventuallyBounded(u)
proof
  have boundReal := limitScale.real at L
  have boundPositive := limitScale.positive at L
  obtain ⟨N, nNatural, close⟩ := ConvergesTo.eventually with converges, realZero.lt_one
  constructor
  . exact ConvergesTo.sequence with converges
  . witness limitScale(L)
    constructor
      exact boundReal
    . constructor
      . exact boundPositive
      . witness N
        constructor
        . exact nNatural
        . intros n nInNaturals nAfterN
          have sequence := ConvergesTo.sequence with converges
          have typedN : Nat(n) by exact nat.omega.backward at n with nInNaturals
          have typedValue := RealSequence.value with sequence
          have near := close with n, nInNaturals, nAfterN
          have nearData := openBall.membership.forward at
            L, realOne, uₙ with near
          rcases nearData with ⟨_, distanceLessOne⟩
          have distanceReal := dist.real at uₙ, L with typedValue
          have absLReal := abs.real at L
          have sumReal := realAddValue.real with distanceReal, absLReal
          have absoluteBound := abs.le_dist_add_abs at uₙ, L with
            typedValue, assumption
          have sumBelow := realLess.add_right with distanceReal, realOne.real, absLReal, distanceLessOne
          have absValueReal := abs.real with typedValue
          have onePlusAbsReal := realAddValue.real with realOne.real, absLReal
          have strictBound := realLe.transitive_less with
            absValueReal, sumReal, onePlusAbsReal, absoluteBound, sumBelow
          have commute := realAddValue.commutative with realOne.real, absLReal
          unfold limitScale
          rw commute at strictBound
          apply openBall.membership.backward
          constructor
            exact typedValue
          . unfold dist
            have zero := realSubValue.zero_right with typedValue
            rwa zero

-- A nonnegative sequence cannot converge to a negative number.  The proof
-- chooses the ball of radius -L/2 around a hypothetical negative limit L;
-- every point in that ball is still negative.
theorem ConvergesTo.nonnegative_of_nonnegative_terms (u : Set) (L : Real)
  requires converges : ConvergesTo(u, L)
  requires nonnegative : NonnegativeTerms(u)
  shows 0 ≤ L
proof
  have sign := Real.sign_cases at L
  cases sign with nonpositive | nonnegativeCut
  . by_contra notNonnegative
    have unequalZero : L ≠ 0
      intro equalZero
      apply notNonnegative
      rw equalZero
      exact realLe.reflexive with realZero.real
    have negative : L < 0
        apply realLess.characterization.backward
        unfold RealLess
        refine ⟨assumption, realZero.real, _⟩
        unfold ProperSubset
        refine ⟨nonpositive, unequalZero⟩
    have negativeView := realLess.characterization.forward with negative
    have reversed := RealLess.neg_reverse at L, realZero with
        assumption, realZero.real, negativeView
    have positiveNeg : 0 < -L
      apply realLess.characterization.backward
      rwa realNegValue.zero at reversed
    have negLReal := realNegValue.real at L
    have radiusReal := half.real with negLReal
    have radiusPositive := half.positive with positiveNeg
    obtain ⟨N, nNatural, close⟩ := ConvergesTo.eventually with converges, radiusPositive
    have typedN : Nat(N) by exact nat.omega.backward at N with nNatural
    have nLeN := LessEqual.reflexive with typedN
    have near := close with N, nNatural, nLeN
    have sequence := ConvergesTo.sequence with converges
    have typedValue := RealSequence.value with sequence
    have nearData := openBall.membership.forward at
      L, half(-L), u[N] with near
    rcases nearData with ⟨_, distanceBelowHalf⟩
    have halfBelowNeg := half.lt_self with positiveNeg
    have distanceReal := dist.real at u[N], L with typedValue
    have distanceBelowNeg := realLess.transitive with
      distanceReal, radiusReal, negLReal, distanceBelowHalf, halfBelowNeg
    have differenceReal := realSubValue.real at u[N], L with
      typedValue, assumption
    have differenceAbsoluteReal := abs.real with differenceReal
    have differenceUpper := abs.upper with differenceReal
    unfold dist at distanceBelowNeg
    have differenceBelowNeg := realLe.transitive_less with
      differenceReal, differenceAbsoluteReal, negLReal, differenceUpper, distanceBelowNeg
    have shifted := realLess.add_right at
      u[N] - L, -L, L with
        differenceReal, negLReal, assumption, differenceBelowNeg
    have cancel := realSubValue.add_right_cancel at u[N], L with
      typedValue, assumption
    have inverse := realAddValue.neg_left at L
    rw [cancel, inverse] at shifted
    have termNonnegativeView := nonnegative with N, nNatural
    have termNonnegative := realLe.characterization.backward with termNonnegativeView
    have impossible := realLe.transitive_less with
      realZero.real, typedValue, realZero.real, termNonnegative, shifted
    exact IsOrderedField.irreflexive with reals.ordered_field, impossible
  . exact realLe.of_subset at realZero, L with
      realZero.real, assumption, nonnegativeCut

-- Termwise order passes to limits.  Apply the preceding theorem to the
-- convergent difference vₙ - uₙ, then translate 0 ≤ M - L by L.
theorem ConvergesTo.le_of_le_terms (u v : Set) (L M : Real)
  requires convergesU : ConvergesTo(u, L)
  requires convergesV : ConvergesTo(v, M)
  requires ordered : PointwiseLE(u, v)
  shows L ≤ M
proof
  have sequenceU := ConvergesTo.sequence with convergesU
  have sequenceV := ConvergesTo.sequence with convergesV
  have differenceConverges := ConvergesTo.sub with convergesV, convergesU
  have differenceNonnegative : NonnegativeTerms(subSequence(v, u))
    intros n nNatural
    have typedN : Nat(n) by exact nat.omega.backward at n with nNatural
    have typedU := RealSequence.value with sequenceU
    have typedV := RealSequence.value with sequenceV
    have value := subSequence.value with sequenceV, sequenceU, typedV, typedU
    have termOrderView := ordered with n, nNatural
    have termOrder := realLe.characterization.backward with termOrderView
    have subset := realLe.subset with typedU, typedV, termOrder
    have nonnegativeDifference := realSubValue.nonnegative_of_subset with typedU, typedV, subset
    have differenceReal := realSubValue.real with typedV, typedU
    rw value
    have nonnegativeLe := realLe.of_subset with realZero.real, nonnegativeDifference
    exact realLe.characterization.forward with nonnegativeLe
  have limitDifferenceNonnegative := ConvergesTo.nonnegative_of_nonnegative_terms with
    differenceConverges, differenceNonnegative
  have differenceReal := realSubValue.real at M, L with *
  have translated := realLe.add_right at
    realZero, M - L, L with
      realZero.real, differenceReal, assumption,
      limitDifferenceNonnegative
  have zero := realAddValue.zero_left at L
  have cancel := realSubValue.add_right_cancel at M, L with
    *{2}
  rwa [zero, cancel] at translated

theorem ConvergesTo.le_constant (u : Set) (L B : Real)
  requires converges : ConvergesTo(u, L)
  requires bounded : BoundedAboveBy(u, B)
  shows L ≤ B
proof
  have constantConverges := constantSequence.converges at B
  apply ConvergesTo.le_of_le_terms with converges, constantConverges
  intros n nNatural
  have typedN : Nat(n) by exact nat.omega.backward at n with nNatural
  have value := constantSequence.value at B, n with assumption, typedN
  rw value
  exact bounded with n, nNatural

theorem ConvergesTo.ge_constant (u : Set) (L A : Real)
  requires converges : ConvergesTo(u, L)
  requires bounded : BoundedBelowBy(u, A)
  shows A ≤ L
proof
  have constantConverges := constantSequence.converges at A
  apply ConvergesTo.le_of_le_terms with constantConverges, converges
  intros n nNatural
  have typedN : Nat(n) by exact nat.omega.backward at n with nNatural
  have value := constantSequence.value at A, n with assumption, typedN
  rw value
  exact bounded with n, nNatural

-- The squeeze theorem now has its textbook order-theoretic proof: pass both
-- inequalities to the limit and use antisymmetry.
theorem ConvergesTo.squeeze (u v w : Set) (L : Real)
  requires convergesU : ConvergesTo(u, L)
  requires sequenceV : RealSequence(v)
  requires convergesW : ConvergesTo(w, L)
  requires lower : PointwiseLE(u, v)
  requires upper : PointwiseLE(v, w)
  shows ConvergesTo(v, L)
proof
  constructor
  . exact sequenceV
  . intros E realE positiveE
    have typedE : Real(E) by exact realE
    obtain ⟨N, nNatural, close⟩ := ConvergesTo.common_eventually with
      convergesU, convergesW, positiveE, positiveE
    witness N
    constructor
    . exact nNatural
    . intros n nInNaturals nAfterN
      have typedN : Nat(n) by exact nat.omega.backward at n with nInNaturals
      have sequenceU := ConvergesTo.sequence with convergesU
      have sequenceW := ConvergesTo.sequence with convergesW
      have typedU := RealSequence.value with sequenceU
      have typedV := RealSequence.value with sequenceV
      have typedW := RealSequence.value with sequenceW
      obtain ⟨nearU, nearW⟩ := close with n, nInNaturals, nAfterN
      have intervalU := openBall.order_characterization.forward at
        uₙ, L, E with typedU, assumption, typedE, nearU
      have intervalW := openBall.order_characterization.forward at
        wₙ, L, E with typedW, assumption, typedE, nearW
      rcases intervalU with ⟨lowerU, _⟩
      rcases intervalW with ⟨_, upperW⟩
      have uLeVView := lower with n, nInNaturals
      have vLeWView := upper with n, nInNaturals
      have uLeV := realLe.characterization.backward with uLeVView
      have vLeW := realLe.characterization.backward with vLeWView
      have lowerEndpointReal := realSubValue.real at L, E with
        assumption, typedE
      have lowerV := realLess.transitive_le with lowerEndpointReal, typedU, typedV, lowerU, uLeV
      have upperV := realLe.transitive_less with typedV, typedW, vLeW, upperW
      apply openBall.order_characterization.backward with typedV
      constructor
      . exact lowerV
      . exact upperV