English
If the (n+1)-th stream element is ifp_succ_n, then its integer part b is at least 1, i.e., 1 ≤ ifp_succ_n.b.
Русский
Если (n+1)-й элемент потока равен ifp_succ_n, тогда его целая часть b не меньше единицы: 1 ≤ ifp_succ_n.b.
LaTeX
$$$\\\\forall {K} {v} {n} \\\\[Field K] \\\\[LinearOrder K] \\\\[IsStrictOrderedRing K] \\\\[FloorRing K], \\\\forall ifp_succ_n : GenContFract.IntFractPair K, \\\\big(IntFractPair.stream v (n+1) = Some \\\\mathbf{ifp_succ_n} \\\\Rightarrow 1 \\le \\\\mathbf{ifp_succ_n}.b\\\\)$$$
Lean4
/-- Shows that the integer parts of the stream are at least one. -/
theorem one_le_succ_nth_stream_b {ifp_succ_n : IntFractPair K}
(succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n) : 1 ≤ ifp_succ_n.b :=
by
obtain ⟨ifp_n, nth_stream_eq, stream_nth_fr_ne_zero, ⟨-⟩⟩ :
∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n :=
succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq
rw [IntFractPair.of, le_floor, cast_one,
one_le_inv₀ ((nth_stream_fr_nonneg nth_stream_eq).lt_of_ne' stream_nth_fr_ne_zero)]
exact (nth_stream_fr_lt_one nth_stream_eq).le
