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