English
For a > 1 and i, j ≤ 2n with h: xn(a1,i) ≡ xn(a1, j) mod xn(a1, n), and a nondegeneracy condition, then i = j.
Русский
Для a > 1 и i, j ≤ 2n с условием непроваленности, если xn(a1,i) ≡ xn(a1, j) (mod xn(a1, n)), тогда i = j.
LaTeX
$$$$ i, j \\le 2n, \\ xn(a1,i) \\equiv xn(a1,j) \\pmod{ xn(a1,n) } \\implies i = j $$$$
Lean4
theorem eq_of_xn_modEq {i j n} (i2n : i ≤ 2 * n) (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 = 2 → j ≠ 0)) : i = j :=
(le_total i j).elim (fun ij => eq_of_xn_modEq_le a1 ij j2n h fun ⟨a2, n1, i0, j2⟩ => (ntriv a2 n1).left i0 j2)
fun ij => (eq_of_xn_modEq_le a1 ij i2n h.symm fun ⟨a2, n1, j0, i2⟩ => (ntriv a2 n1).right i2 j0).symm
