English
If i ≤ j ≤ 2n and xn(a1, i) ≡ xn(a1, j) (mod xn(a1, n)) and there is no degenerate case (a = 2, n = 1, i = 0, j = 2), then i = j.
Русский
Если i ≤ j ≤ 2n и xn(a1, i) ≡ xn(a1, j) (mod xn(a1, n)), и не существует вырожденного случая (a = 2, n = 1, i = 0, j = 2), тогда i = j.
LaTeX
$$$$ i \\le j \\le 2n, \\ xn(a1,i) \\equiv xn(a1,j) \\pmod{ xn(a1,n) } \\implies i = j $$$$
Lean4
theorem eq_of_xn_modEq_le {i j n} (ij : i ≤ j) (j2n : j ≤ 2 * n) (h : xn a1 i ≡ xn a1 j [MOD xn a1 n])
(ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)) : i = j :=
if npos : n = 0 then by simp_all
else
(lt_or_eq_of_le ij).resolve_left fun ij' =>
if jn : j = n then by
refine _root_.ne_of_gt ?_ h
rw [jn, Nat.mod_self]
have x0 : 0 < xn a1 0 % xn a1 n :=
by
rw [Nat.mod_eq_of_lt (strictMono_x a1 (Nat.pos_of_ne_zero npos))]
exact Nat.succ_pos _
rcases i with - | i
· exact x0
rw [jn] at ij'
exact
x0.trans
(eq_of_xn_modEq_lem3 _ (Nat.pos_of_ne_zero npos) (Nat.succ_pos _) (le_trans ij j2n) (_root_.ne_of_lt ij')
fun ⟨_, n1, _, i2⟩ => by rw [n1, i2] at ij'; exact absurd ij' (by decide))
else _root_.ne_of_lt (eq_of_xn_modEq_lem3 a1 (Nat.pos_of_ne_zero npos) ij' j2n jn ntriv) h
