-- Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean
theorem zero_le_of_contsAux_b : 0 ≤ ((of v).contsAux n).b

Proof state:
case succ.inl.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux (n + 1)).b
terminated : g.TerminatedAt (n + 1 - 1)
⊢ 0 ≤ ((of v).contsAux (n + 1 + 1)).b

Tactic:
have : g.contsAux (n + 2) = g.contsAux (n + 1) :=
  contsAux_stable_step_of_terminated terminated

Result:
case succ.inl.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux (n + 1)).b
terminated : g.TerminatedAt (n + 1 - 1)
this : g.contsAux (n + 2) = g.contsAux (n + 1)
⊢ 0 ≤ ((of v).contsAux (n + 1 + 1)).b

Proof state:
case succ.inl.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux (n + 1)).b
terminated : g.TerminatedAt (n + 1 - 1)
this : g.contsAux (n + 2) = g.contsAux (n + 1)
⊢ 0 ≤ ((of v).contsAux (n + 1 + 1)).b

Tactic:
simp only [g, this, IH]

Result:
no goals

Proof state:
case succ.inr
K : Type u_1
v : K
n✝ : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux n).b
not_terminated : ¬g.TerminatedAt (n - 1)
⊢ 0 ≤ ((of v).contsAux (n + 1)).b

Tactic:
calc
  (0 : K) ≤ fib (n + 1) := mod_cast (n + 1).fib.zero_le
  _ ≤ ((of v).contsAux (n + 1)).b := fib_le_of_contsAux_b (Or.inr not_terminated)

Result:
no goals

Proof state:
case zero
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
⊢ 0 ≤ ((of v).contsAux 0).b

Tactic:
rfl

Result:
no goals

Proof state:
case succ
K : Type u_1
v : K
n✝ : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux n).b
⊢ 0 ≤ ((of v).contsAux (n + 1)).b

Tactic:
rcases Decidable.em <| g.TerminatedAt (n - 1) with terminated | not_terminated

Result:
case succ.inl
K : Type u_1
v : K
n✝ : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux n).b
terminated : g.TerminatedAt (n - 1)
⊢ 0 ≤ ((of v).contsAux (n + 1)).b

case succ.inr
K : Type u_1
v : K
n✝ : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux n).b
not_terminated : ¬g.TerminatedAt (n - 1)
⊢ 0 ≤ ((of v).contsAux (n + 1)).b

Proof state:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
⊢ 0 ≤ ((of v).contsAux n).b

Tactic:
let g := of v

Result:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
⊢ 0 ≤ ((of v).contsAux n).b

Proof state:
case succ.inl.zero
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
IH : 0 ≤ ((of v).contsAux 0).b
terminated : g.TerminatedAt (0 - 1)
⊢ 0 ≤ ((of v).contsAux (0 + 1)).b

Tactic:
simp [zero_le_one]

Result:
no goals

Proof state:
case succ.inl
K : Type u_1
v : K
n✝ : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux n).b
terminated : g.TerminatedAt (n - 1)
⊢ 0 ≤ ((of v).contsAux (n + 1)).b

Tactic:
rcases n with - | n

Result:
case succ.inl.zero
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
IH : 0 ≤ ((of v).contsAux 0).b
terminated : g.TerminatedAt (0 - 1)
⊢ 0 ≤ ((of v).contsAux (0 + 1)).b

case succ.inl.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux (n + 1)).b
terminated : g.TerminatedAt (n + 1 - 1)
⊢ 0 ≤ ((of v).contsAux (n + 1 + 1)).b