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 2 = { a := gp.b * g.h + gp.a, b := gp.b }
simp [zeroth_s_eq, continuantsAux, nextContinuants, nextDenominator, nextNumerator]