English
If a stream element has fractional part zero, then the next element of the stream vanishes (is none). More precisely, if IntFractPair.stream v n = Some p and p.fr = 0, then IntFractPair.stream v (n+1) = None.
Русский
Если следующий элемент потока имеет дробную часть нулевую, то следующий элемент потока отсутствует (none). Пусть IntFractPair.stream v n = Some p и p.fr = 0, тогда IntFractPair.stream v (n+1) = None.
LaTeX
$$$\forall v\,\forall n\,\forall p,\; (\operatorname{IntFractPair}.\operatorname{stream}(v,n) = \mathrm{Some}(p) \land p.f r = 0)\Rightarrow \operatorname{IntFractPair}.\operatorname{stream}(v,n+1) = \mathrm{None}$$$
Lean4
theorem stream_eq_none_of_fr_eq_zero {ifp_n : IntFractPair K} (stream_nth_eq : IntFractPair.stream v n = some ifp_n)
(nth_fr_eq_zero : ifp_n.fr = 0) : IntFractPair.stream v (n + 1) = none :=
by
obtain ⟨_, fr⟩ := ifp_n
change fr = 0 at nth_fr_eq_zero
simp [IntFractPair.stream, stream_nth_eq, nth_fr_eq_zero]
