no goals
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
b : α
nth_part_denom_eq : Stream'.Seq.get? (partialDenominators g) n = some b
⊢ ∃ gp, Stream'.Seq.get? g.s n = some gp ∧ gp.b = b
simpa [partialDenominators, Stream'.Seq.map_get?] using nth_part_denom_eq