K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminated_at_n : TerminatedAt g n
k : ℕ
hnk : Nat.succ n ≤ k
hk : continuantsAux g k = continuantsAux g (n + 1)
⊢ continuantsAux g (k + 1) = continuantsAux g (n + 1)
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminated_at_n : TerminatedAt g n
⊢ continuantsAux g m = continuantsAux g (n + 1)
refine' Nat.le_induction rfl (fun k hnk hk => _) _ n_lt_m
case intro
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminated_at_n : TerminatedAt g n
k : ℕ
hnk : Nat.succ n ≤ n + k + 1
hk : continuantsAux g (n + k + 1) = continuantsAux g (n + 1)
⊢ continuantsAux g (n + k + 1 + 1) = continuantsAux g (n + 1)
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminated_at_n : TerminatedAt g n
k : ℕ
hnk : Nat.succ n ≤ k
hk : continuantsAux g k = continuantsAux g (n + 1)
⊢ continuantsAux g (k + 1) = continuantsAux g (n + 1)
rcases Nat.exists_eq_add_of_lt hnk with ⟨k, rfl⟩
case intro
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminated_at_n : TerminatedAt g n
k : ℕ
hnk : Nat.succ n ≤ n + k + 1
hk : continuantsAux g (n + k + 1) = continuantsAux g (n + 1)
⊢ TerminatedAt g (n + k)
case intro
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminated_at_n : TerminatedAt g n
k : ℕ
hnk : Nat.succ n ≤ n + k + 1
hk : continuantsAux g (n + k + 1) = continuantsAux g (n + 1)
⊢ continuantsAux g (n + k + 1 + 1) = continuantsAux g (n + 1)
refine' (continuantsAux_stable_step_of_terminated _).trans hk
no goals
case intro
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminated_at_n : TerminatedAt g n
k : ℕ
hnk : Nat.succ n ≤ n + k + 1
hk : continuantsAux g (n + k + 1) = continuantsAux g (n + 1)
⊢ TerminatedAt g (n + k)
exact terminated_stable (Nat.le_add_right _ _) terminated_at_n