K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminated_at_succ_n : Stream'.Seq.get? s (n + 1) = none
⊢ squashSeq s n = s
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminated_at_succ_n : Stream'.Seq.TerminatedAt s (n + 1)
⊢ squashSeq s n = s
change s.get? (n + 1) = none at terminated_at_succ_n
no goals
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminated_at_succ_n : Stream'.Seq.get? s (n + 1) = none
⊢ squashSeq s n = s
cases s_nth_eq : s.get? n <;> simp only [*, squashSeq]