no goals
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
⊢ Stream'.Seq.get? (squashGCF g (n + 1)).s m = Stream'.Seq.get? g.s m
simp only [squashGCF, squashSeq_nth_of_lt m_lt_n, Nat.add_eq, add_zero]