English
If the (n+1)th stream term is a some ifp whose fractional part is zero, then there exists a previous term ifp_n with nonzero fractional part and with ifp_n.fr^{-1} having integer part equal to floor(ifp_n.fr^{-1}).
Русский
Если (n+1)й член потока — Some ifp с нулевой дробной частью, тогда существует предыдущий ifp_n с ненулевой дробной частью и с тем, что ifp_n.fr^{-1} имеет целую часть, равную floor(ifp_n.fr^{-1}).
LaTeX
$$$\exists ifp_n,\; \operatorname{IntFractPair}.\operatorname{stream}(v,n) = \mathrm{Some}(ifp_n) \land ifp_n.f r^{-1} = \lfloor ifp_n.f r^{-1} \rfloor$$$
Lean4
theorem exists_succ_nth_stream_of_fr_zero {ifp_succ_n : IntFractPair K}
(stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n) (succ_nth_fr_eq_zero : ifp_succ_n.fr = 0) :
∃ ifp_n : IntFractPair K, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ⌊ifp_n.fr⁻¹⌋ := by
-- get the witness from `succ_nth_stream_eq_some_iff` and prove that it has the additional
-- properties
rcases succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq with ⟨ifp_n, seq_nth_eq, _, rfl⟩
refine ⟨ifp_n, seq_nth_eq, ?_⟩
simpa only [IntFractPair.of, Int.fract, sub_eq_zero] using succ_nth_fr_eq_zero
