no goals
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
gp : Pair α
s_nth_eq : Stream'.Seq.get? g.s n = some gp
⊢ Stream'.Seq.get? (partialDenominators g) n = some gp.b
simp [partialDenominators, s_nth_eq]