case refl
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.TerminatedAt s n
⊢ convergents'Aux s n = convergents'Aux s n

case step
K : Type u_1
g : GeneralizedContinuedFraction K
n m✝ : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.TerminatedAt s n
m : ℕ
n_le_m : Nat.le n m
IH : convergents'Aux s m = convergents'Aux s n
⊢ convergents'Aux s (Nat.succ m) = convergents'Aux s n
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
n_le_m : n ≤ m
terminated_at_n : Stream'.Seq.TerminatedAt s n
⊢ convergents'Aux s m = convergents'Aux s n
induction' n_le_m with m n_le_m IH
no goals
case refl
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.TerminatedAt s n
⊢ convergents'Aux s n = convergents'Aux s n
rfl
case step
K : Type u_1
g : GeneralizedContinuedFraction K
n m✝ : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.TerminatedAt s n
m : ℕ
n_le_m : Nat.le n m
IH : convergents'Aux s m = convergents'Aux s n
⊢ Stream'.Seq.TerminatedAt s m
case step
K : Type u_1
g : GeneralizedContinuedFraction K
n m✝ : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.TerminatedAt s n
m : ℕ
n_le_m : Nat.le n m
IH : convergents'Aux s m = convergents'Aux s n
⊢ convergents'Aux s (Nat.succ m) = convergents'Aux s n
refine' (convergents'Aux_stable_step_of_terminated _).trans IH
no goals
case step
K : Type u_1
g : GeneralizedContinuedFraction K
n m✝ : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.TerminatedAt s n
m : ℕ
n_le_m : Nat.le n m
IH : convergents'Aux s m = convergents'Aux s n
⊢ Stream'.Seq.TerminatedAt s m
exact s.terminated_stable n_le_m terminated_at_n