English
The nth element of the stream is computed by the recurrence relating successive ifp_n and ifp_{n+1}.
Русский
n-й элемент потока вычисляется по рецуррентному соотношению между successive ifp_n и ifp_{n+1}.
LaTeX
$$$\\text{stream}(q,n) = \\text{some } ifp_n \\Rightarrow \\text{recurrence between } ifp_n \\text{ and } ifp_{n+1}$$$
Lean4
theorem stream_nth_fr_num_le_fr_num_sub_n_rat :
∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - n :=
by
induction n with
| zero =>
intro ifp_zero stream_zero_eq
have : IntFractPair.of q = ifp_zero := by injection stream_zero_eq
simp [le_refl, this.symm]
| succ n IH =>
intro ifp_succ_n stream_succ_nth_eq
suffices ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - n
by
rw [Int.natCast_succ, sub_add_eq_sub_sub]
solve_by_elim [le_sub_right_of_add_le]
rcases succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq with ⟨ifp_n, stream_nth_eq, -⟩
have : ifp_succ_n.fr.num < ifp_n.fr.num := stream_succ_nth_fr_num_lt_nth_fr_num_rat stream_nth_eq stream_succ_nth_eq
exact le_trans this (IH stream_nth_eq)
