no goals
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ TerminatedAt (of v) n ↔ IntFractPair.stream v (n + 1) = none
rw [of_terminatedAt_iff_intFractPair_seq1_terminatedAt, Stream'.Seq.TerminatedAt,
  IntFractPair.get?_seq1_eq_succ_get?_stream]