English
The (n+1)th stream term is none precisely when either the nth term is none or the nth term corresponds to a fractional part equal to zero at some stage; equivalently, termination propagates according to a termination step.
Русский
Следующий член потока равен none тогда и только тогда, когда предыдущий член потока уже равен none или существует шаг, на котором дробная часть нуля, что приводит к прекращению.
LaTeX
$$$\operatorname{IntFractPair}.\operatorname{stream}(v,n+1) = \mathrm{None} \;\iff\; \Big(\operatorname{IntFractPair}.\operatorname{stream}(v,n) = \mathrm{None}\;\lor\; \exists p, \operatorname{IntFractPair}.\operatorname{stream}(v,n) = \mathrm{Some}(p) \land p.f r = 0\Big)$$$
Lean4
/-- Gives a recurrence to compute the `n + 1`th value of the sequence of integer and fractional
parts of a value in case of termination.
-/
theorem succ_nth_stream_eq_none_iff :
IntFractPair.stream v (n + 1) = none ↔
IntFractPair.stream v n = none ∨ ∃ ifp, IntFractPair.stream v n = some ifp ∧ ifp.fr = 0 :=
by
rw [IntFractPair.stream]
cases IntFractPair.stream v n <;> simp [imp_false]
