[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
⊢ Stream'.IsSeq (IntFractPair.stream v)
[PROOFSTEP]
intro _ hyp
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
hyp : IntFractPair.stream v n✝ = none
⊢ IntFractPair.stream v (n✝ + 1) = none
[PROOFSTEP]
simp [IntFractPair.stream, hyp]
