English
The (n+1)th stream equals some ifp_succ_n exactly when there is some ifp_n with the nth stream equal to some ifp_n, this ifp_n has nonzero fractional part, and ifp_n.fr⁻¹ matches ifp_succ_n via the integer constructor of the pair.
Русский
Член (n+1) потока равен некоторому ifp_succ_n тогда и только тогда, когда существует ifp_n с тем, что поток на позиции n равен some ifp_n, дробная часть ifp_n не равна нулю, и ifp_n.fr⁻¹ сопоставляется с ifp_succ_n через конструктор пары.
LaTeX
$$$\operatorname{IntFractPair}.\operatorname{stream}(v,n+1) = \mathrm{Some}(ifp_{succ}) \iff \exists ifp_n,\; \operatorname{IntFractPair}.\operatorname{stream}(v,n) = \mathrm{Some}(ifp_n) \land ifp_n.f r \neq 0 \land \operatorname{IntFractPair}.\operatorname{of}(ifp_n.f r) = ifp_{succ}$$$
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 non-termination.
-/
theorem succ_nth_stream_eq_some_iff {ifp_succ_n : IntFractPair K} :
IntFractPair.stream v (n + 1) = some ifp_succ_n ↔
∃ ifp_n : IntFractPair K,
IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n :=
by simp [IntFractPair.stream, ite_eq_iff, Option.bind_eq_some_iff]
