English
Let i < j ≤ n. Then xn(a1, i) ≡ xn(a1, j) (mod xn(a1, n)) cannot hold in the simple monotone subrange; in particular, if i < j then xn(a1, i) mod xn(a1, n) < xn(a1, j) mod xn(a1, n).
Русский
Пусть i < j ≤ n. Тогда xn(a1, i) ≡ xn(a1, j) (mod xn(a1, n)) невозможно в рассматриваемом диапазоне; следовательно, остатки удовлетворяют xn(a1, i) mod xn(a1, n) < xn(a1, j) mod xn(a1, n).
LaTeX
$$$$ xn(a1, i) \\bmod xn(a1, n) < xn(a1, j) \\bmod xn(a1, n) \\quad \\text{for } i < j \le n $$$$
Lean4
theorem eq_of_xn_modEq_lem1 {i n} : ∀ {j}, i < j → j < n → xn a1 i % xn a1 n < xn a1 j % xn a1 n
| 0, ij, _ => absurd ij (Nat.not_lt_zero _)
| j + 1, ij, jn =>
by
suffices xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n from
(lt_or_eq_of_le (Nat.le_of_succ_le_succ ij)).elim (fun h => lt_trans (eq_of_xn_modEq_lem1 h (le_of_lt jn)) this)
fun h => by rw [h]; exact this
rw [Nat.mod_eq_of_lt (strictMono_x _ (Nat.lt_of_succ_lt jn)), Nat.mod_eq_of_lt (strictMono_x _ jn)]
exact strictMono_x _ (Nat.lt_succ_self _)
