no goals
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_n gp_succ_n : Pair K
s_nth_eq : Stream'.Seq.get? s n = some gp_n
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
⊢ Stream'.Seq.get? (squashSeq s n) n = some { a := gp_n.a, b := gp_n.b + gp_succ_n.a / gp_succ_n.b }
simp [*, squashSeq]