Lean4
theorem eq_of_xn_modEq_lem3 {i n} (npos : 0 < n) :
∀ {j}, i < j → j ≤ 2 * n → j ≠ n → ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2) → xn a1 i % xn a1 n < xn a1 j % xn a1 n
| 0, ij, _, _, _ => absurd ij (Nat.not_lt_zero _)
| j + 1, ij, j2n, jnn, ntriv =>
have lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = xn a1 n - xn a1 (2 * n - k) := fun k kn k2n =>
by
let k2nl :=
lt_of_add_lt_add_right <|
show 2 * n - k + k < n + k by
rw [tsub_add_cancel_of_le]
· rw [two_mul]
exact add_lt_add_left kn n
exact k2n
have xle : xn a1 (2 * n - k) ≤ xn a1 n := le_of_lt <| strictMono_x a1 k2nl
suffices xn a1 k % xn a1 n = xn a1 n - xn a1 (2 * n - k) by rw [this, Int.ofNat_sub xle]
rw [← Nat.mod_eq_of_lt (Nat.sub_lt (x_pos a1 n) (x_pos a1 (2 * n - k)))]
apply ModEq.add_right_cancel' (xn a1 (2 * n - k))
rw [tsub_add_cancel_of_le xle]
have t := xn_modEq_x2n_sub_lem a1 k2nl.le
rw [tsub_tsub_cancel_of_le k2n] at t
exact t.trans dvd_rfl.zero_modEq_nat
(lt_trichotomy j n).elim (fun jn : j < n => eq_of_xn_modEq_lem1 _ ij (lt_of_le_of_ne jn jnn)) fun o =>
o.elim
(fun jn : j = n => by
cases jn
apply Int.lt_of_ofNat_lt_ofNat
rw [lem2 (n + 1) (Nat.lt_succ_self _) j2n,
show 2 * n - (n + 1) = n - 1 by rw [two_mul, tsub_add_eq_tsub_tsub, add_tsub_cancel_right]]
refine lt_sub_left_of_add_lt (Int.ofNat_lt_ofNat_of_lt ?_)
rcases lt_or_eq_of_le <| Nat.le_of_succ_le_succ ij with lin | ein
· rw [Nat.mod_eq_of_lt (strictMono_x _ lin)]
have ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n :=
by
rw [← two_mul, mul_comm,
show xn a1 n = xn a1 (n - 1 + 1) by rw [tsub_add_cancel_of_le (succ_le_of_lt npos)], xn_succ]
exact le_trans (Nat.mul_le_mul_left _ a1) (Nat.le_add_right _ _)
have npm : (n - 1).succ = n := Nat.succ_pred_eq_of_pos npos
have il : i ≤ n - 1 := by
apply Nat.le_of_succ_le_succ
rw [npm]
exact lin
rcases lt_or_eq_of_le il with ill | ile
· exact lt_of_lt_of_le (Nat.add_lt_add_left (strictMono_x a1 ill) _) ll
· rw [ile]
apply lt_of_le_of_ne ll
rw [← two_mul]
exact fun e =>
ntriv <|
by
let ⟨a2, s1⟩ :=
@eq_of_xn_modEq_lem2 _ a1 (n - 1) (by rwa [tsub_add_cancel_of_le (succ_le_of_lt npos)])
have n1 : n = 1 := le_antisymm (tsub_eq_zero_iff_le.mp s1) npos
rw [ile, a2, n1]; exact ⟨rfl, rfl, rfl, rfl⟩
· rw [ein, Nat.mod_self, add_zero]
exact strictMono_x _ (Nat.pred_lt npos.ne'))
fun jn : j > n =>
have lem1 : j ≠ n → xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n → xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n :=
fun jn s =>
(lt_or_eq_of_le (Nat.le_of_succ_le_succ ij)).elim
(fun h =>
lt_trans
(eq_of_xn_modEq_lem3 npos h (le_of_lt (Nat.lt_of_succ_le j2n)) jn fun ⟨_, n1, _, j2⟩ => by
rw [n1, j2] at j2n; exact absurd j2n (by decide))
s)
fun h => by rw [h]; exact s
lem1 (_root_.ne_of_gt jn) <|
Int.lt_of_ofNat_lt_ofNat <|
by
rw [lem2 j jn (le_of_lt j2n), lem2 (j + 1) (Nat.le_succ_of_le jn) j2n]
refine sub_lt_sub_left (Int.ofNat_lt_ofNat_of_lt <| strictMono_x _ ?_) _
rw [Nat.sub_succ]
exact Nat.pred_lt (_root_.ne_of_gt <| tsub_pos_of_lt j2n)
