K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
terminated_at_n : Stream'.Seq.get? g.s n = none
⊢ continuantsAux g (n + 2) = continuantsAux g (n + 1)
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
terminated_at_n : TerminatedAt g n
⊢ continuantsAux g (n + 2) = continuantsAux g (n + 1)
rw [terminatedAt_iff_s_none] at terminated_at_n
no goals
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
terminated_at_n : Stream'.Seq.get? g.s n = none
⊢ continuantsAux g (n + 2) = continuantsAux g (n + 1)
simp only [continuantsAux, Nat.add_eq, add_zero, terminated_at_n]