English
If the nth and (n+1)-st stream entries are ifp_n and ifp_succ_n respectively, then the (n+1)-st integer part satisfies (ifp_succ_n.b) ≤ (ifp_n.fr)⁻¹.
Русский
Пусть подряд идущие элементы потока равны ifp_n и ifp_succ_n; тогда b_{n+1} ≤ fr_n⁻¹.
LaTeX
$$$\\\\forall {K} {v} {n} \\\\[Field K] \\\\[LinearOrder K] \\\\[IsStrictOrderedRing K] \\\\[FloorRing K], \\\\forall nth : IntFractPair K, \\\\forall succ : IntFractPair K,\n IntFractPair.stream v n = Some nth \\\\land IntFractPair.stream v (n+1) = Some succ \\\\Rightarrow (succ.b : K) \\\\le nth.fr^{-1}$$$
Lean4
/-- Shows that the `n + 1`th integer part `bₙ₊₁` of the stream is smaller or equal than the inverse of
the `n`th fractional part `frₙ` of the stream.
This result is straight-forward as `bₙ₊₁` is defined as the floor of `1 / frₙ`.
-/
theorem succ_nth_stream_b_le_nth_stream_fr_inv {ifp_n ifp_succ_n : IntFractPair K}
(nth_stream_eq : IntFractPair.stream v n = some ifp_n)
(succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n) : (ifp_succ_n.b : K) ≤ ifp_n.fr⁻¹ :=
by
suffices (⌊ifp_n.fr⁻¹⌋ : K) ≤ ifp_n.fr⁻¹ by
obtain ⟨_, ifp_n_fr⟩ := ifp_n
have : ifp_n_fr ≠ 0 := by
intro h
simp [h, IntFractPair.stream, nth_stream_eq] at succ_nth_stream_eq
have : IntFractPair.of ifp_n_fr⁻¹ = ifp_succ_n := by
simpa [this, IntFractPair.stream, nth_stream_eq, Option.coe_def] using succ_nth_stream_eq
rwa [← this]
exact floor_le ifp_n.fr⁻¹
