K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
zeroth_s_eq : Stream'.Seq.get? g.s 0 = some gp
⊢ continuantsAux g (1 + 1) = { a := gp.b * g.h + gp.a, b := gp.b }
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
zeroth_s_eq : Stream'.Seq.get? g.s 0 = some gp
⊢ continuants g 1 = { a := gp.b * g.h + gp.a, b := gp.b }
simp [nth_cont_eq_succ_nth_cont_aux]
no goals
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
zeroth_s_eq : Stream'.Seq.get? g.s 0 = some gp
⊢ continuantsAux g (1 + 1) = { a := gp.b * g.h + gp.a, b := gp.b }
convert second_continuant_aux_eq zeroth_s_eq