no goals
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
h : Stream'.Seq.head s = none
n : ℕ
⊢ convergents'Aux s (n + 1) = 0
simp [convergents'Aux, h, convergents'Aux.match_1]