-- Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean
theorem fib_le_of_contsAux_b :
    n ≤ 1 ∨ ¬(of v).TerminatedAt (n - 2) → (fib n : K) ≤ ((of v).contsAux n).b :=
  Nat.strong_induction_on n
    (by
      intro n IH hyp
      rcases n with (_ | _ | n)
      · simp [fib_add_two, contsAux] -- case n = 0
      · simp [fib_add_two, contsAux] -- case n = 1
      · let g := of v -- case 2 ≤ n
        have : ¬n + 2 ≤ 1

Proof state:
case succ.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
⊢ ↑(fib (n + 1 + 1)) ≤ ((of v).contsAux (n + 1 + 1)).b

Tactic:
let g := of v

Result:
case succ.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
⊢ ↑(fib (n + 1 + 1)) ≤ ((of v).contsAux (n + 1 + 1)).b

Proof state:
K : Type u_1
v : K
n✝ : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this✝ : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
this : ↑(fib n) + ↑(fib (n + 1)) ≤ gp.a * ppconts.b + gp.b * pconts.b
⊢ ↑(fib (n + 2)) ≤ ((of v).contsAux (n + 2)).b

Tactic:
simpa [g, fib_add_two, add_comm, contsAux_recurrence s_ppred_nth_eq ppconts_eq pconts_eq]

Result:
no goals

Proof state:
case succ.succ.intro
K : Type u_1
v : K
n✝ : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
⊢ ↑(fib n) + ↑(fib (n + 1)) ≤ ppconts.b + gp.b * pconts.b

Tactic:
have not_terminatedAt_ppred_n : ¬TerminatedAt g (n - 2) :=
  mt (terminated_stable (n - 1).pred_le) not_terminatedAt_pred_n

Result:
case succ.succ.intro
K : Type u_1
v : K
n✝ : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
not_terminatedAt_ppred_n : ¬g.TerminatedAt (n - 2)
⊢ ↑(fib n) + ↑(fib (n + 1)) ≤ ppconts.b + gp.b * pconts.b

Proof state:
case succ.succ.intro
K : Type u_1
v : K
n✝ : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
⊢ ↑(fib (n + 1 + 1)) ≤ ((of v).contsAux (n + 1 + 1)).b

Tactic:
simp only [Nat.succ_eq_add_one, Nat.add_assoc, Nat.reduceAdd]

Result:
case succ.succ.intro
K : Type u_1
v : K
n✝ : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
⊢ ↑(fib (n + 2)) ≤ ((of v).contsAux (n + 2)).b

Proof state:
case succ.succ.intro
K : Type u_1
v : K
n✝ : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
not_terminatedAt_ppred_n : ¬g.TerminatedAt (n - 2)
ppred_nth_fib_le_ppconts_B : ↑(fib n) ≤ ppconts.b
⊢ ↑(fib (n + 1)) ≤ gp.b * pconts.b

Tactic:
suffices 1 * (fib (n + 1) : K) ≤ gp.b * pconts.b by rwa [one_mul] at this

Result:
case succ.succ.intro
K : Type u_1
v : K
n✝ : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
not_terminatedAt_ppred_n : ¬g.TerminatedAt (n - 2)
ppred_nth_fib_le_ppconts_B : ↑(fib n) ≤ ppconts.b
⊢ 1 * ↑(fib (n + 1)) ≤ gp.b * pconts.b

Proof state:
case succ.succ.intro
K : Type u_1
v : K
n✝ : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
not_terminatedAt_ppred_n : ¬g.TerminatedAt (n - 2)
ppred_nth_fib_le_ppconts_B : ↑(fib n) ≤ ppconts.b
one_le_gp_b : 1 ≤ gp.b
⊢ 1 * ↑(fib (n + 1)) ≤ gp.b * pconts.b

Tactic:
have : (0 : K) ≤ fib (n + 1) := mod_cast (fib (n + 1)).zero_le

Result:
case succ.succ.intro
K : Type u_1
v : K
n✝ : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this✝ : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
not_terminatedAt_ppred_n : ¬g.TerminatedAt (n - 2)
ppred_nth_fib_le_ppconts_B : ↑(fib n) ≤ ppconts.b
one_le_gp_b : 1 ≤ gp.b
this : 0 ≤ ↑(fib (n + 1))
⊢ 1 * ↑(fib (n + 1)) ≤ gp.b * pconts.b