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
⊢ denominators g 1 = gp.b
simp [denom_eq_conts_b, first_continuant_eq zeroth_s_eq]