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
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
⊢ Stream'.IsSeq (IntFractPair.stream v)
intro _ hyp
no goals
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
simp [IntFractPair.stream, hyp]