English
Let i > 0, i ≤ n and j ≤ 4n with h: xn(a1, j) ≡ xn(a1, i) (mod xn(a1, n)). Then either i = j or j + i = 4n.
Русский
Пусть i > 0, i ≤ n и j ≤ 4n; если xn(a1, j) ≡ xn(a1, i) (mod xn(a1, n)), то либо i = j, либо j + i = 4n.
LaTeX
$$$$ i > 0, i \\le n, j \\le 4n, \\ xn(a1, j) \\equiv xn(a1, i) \\pmod{ xn(a1, n) } \\implies i = j \\text{ or } i + j = 4n $$$$
Lean4
theorem eq_of_xn_modEq' {i j n} (ipos : 0 < i) (hin : i ≤ n) (j4n : j ≤ 4 * n) (h : xn a1 j ≡ xn a1 i [MOD xn a1 n]) :
j = i ∨ j + i = 4 * n :=
have i2n : i ≤ 2 * n := by apply le_trans hin; rw [two_mul]; apply Nat.le_add_left
(le_or_gt j (2 * n)).imp
(fun j2n : j ≤ 2 * n =>
eq_of_xn_modEq a1 j2n i2n h fun _ n1 =>
⟨fun _ i2 => by rw [n1, i2] at hin; exact absurd hin (by decide), fun _ i0 => _root_.ne_of_gt ipos i0⟩)
fun j2n : 2 * n < j =>
suffices i = 4 * n - j by rw [this, add_tsub_cancel_of_le j4n]
have j42n : 4 * n - j ≤ 2 * n := by cutsat
eq_of_xn_modEq a1 i2n j42n
(h.symm.trans <| by
let t := xn_modEq_x4n_sub a1 j42n
rwa [tsub_tsub_cancel_of_le j4n] at t)
(by cutsat)
