a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n :=
  lt_of_add_lt_add_right
    (let_fun this :=
      Eq.mpr (id (tsub_add_cancel_of_le k2n ▸ Eq.refl (2 * n - k + k < n + k)))
        (Eq.mpr (id (two_mul n ▸ Eq.refl (2 * n < n + k))) (add_lt_add_left kn n));
    this)
⊢ ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
⊢ ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
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
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n :=
  lt_of_add_lt_add_right
    (let_fun this :=
      Eq.mpr (id (tsub_add_cancel_of_le k2n ▸ Eq.refl (2 * n - k + k < n + k)))
        (Eq.mpr (id (two_mul n ▸ Eq.refl (2 * n < n + k))) (add_lt_add_left kn n));
    this)
xle : xn a1 (2 * n - k) ≤ xn a1 n
⊢ ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n :=
  lt_of_add_lt_add_right
    (let_fun this :=
      Eq.mpr (id (tsub_add_cancel_of_le k2n ▸ Eq.refl (2 * n - k + k < n + k)))
        (Eq.mpr (id (two_mul n ▸ Eq.refl (2 * n < n + k))) (add_lt_add_left kn n));
    this)
⊢ ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
have xle : xn a1 (2 * n - k) ≤ xn a1 n := le_of_lt <| strictMono_x a1 k2nl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n :=
  lt_of_add_lt_add_right
    (let_fun this :=
      Eq.mpr (id (tsub_add_cancel_of_le k2n ▸ Eq.refl (2 * n - k + k < n + k)))
        (Eq.mpr (id (two_mul n ▸ Eq.refl (2 * n < n + k))) (add_lt_add_left kn n));
    this)
xle : xn a1 (2 * n - k) ≤ xn a1 n
⊢ xn a1 k % xn a1 n = xn a1 n - xn a1 (2 * n - k)
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n :=
  lt_of_add_lt_add_right
    (let_fun this :=
      Eq.mpr (id (tsub_add_cancel_of_le k2n ▸ Eq.refl (2 * n - k + k < n + k)))
        (Eq.mpr (id (two_mul n ▸ Eq.refl (2 * n < n + k))) (add_lt_add_left kn n));
    this)
xle : xn a1 (2 * n - k) ≤ xn a1 n
⊢ ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
suffices xn a1 k % xn a1 n = xn a1 n - xn a1 (2 * n - k) by rw [this, Int.ofNat_sub xle]
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n :=
  lt_of_add_lt_add_right
    (let_fun this :=
      Eq.mpr (id (tsub_add_cancel_of_le k2n ▸ Eq.refl (2 * n - k + k < n + k)))
        (Eq.mpr (id (two_mul n ▸ Eq.refl (2 * n < n + k))) (add_lt_add_left kn n));
    this)
xle : xn a1 (2 * n - k) ≤ xn a1 n
⊢ xn a1 k % xn a1 n = (xn a1 n - xn a1 (2 * n - k)) % xn a1 n
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n :=
  lt_of_add_lt_add_right
    (let_fun this :=
      Eq.mpr (id (tsub_add_cancel_of_le k2n ▸ Eq.refl (2 * n - k + k < n + k)))
        (Eq.mpr (id (two_mul n ▸ Eq.refl (2 * n < n + k))) (add_lt_add_left kn n));
    this)
xle : xn a1 (2 * n - k) ≤ xn a1 n
⊢ xn a1 k % xn a1 n = xn a1 n - xn a1 (2 * n - k)
rw [← Nat.mod_eq_of_lt (Nat.sub_lt (x_pos a1 n) (x_pos a1 (2 * n - k)))]
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n :=
  lt_of_add_lt_add_right
    (let_fun this :=
      Eq.mpr (id (tsub_add_cancel_of_le k2n ▸ Eq.refl (2 * n - k + k < n + k)))
        (Eq.mpr (id (two_mul n ▸ Eq.refl (2 * n < n + k))) (add_lt_add_left kn n));
    this)
xle : xn a1 (2 * n - k) ≤ xn a1 n
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n - xn a1 (2 * n - k) + xn a1 (2 * n - k) [MOD xn a1 n]
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n :=
  lt_of_add_lt_add_right
    (let_fun this :=
      Eq.mpr (id (tsub_add_cancel_of_le k2n ▸ Eq.refl (2 * n - k + k < n + k)))
        (Eq.mpr (id (two_mul n ▸ Eq.refl (2 * n < n + k))) (add_lt_add_left kn n));
    this)
xle : xn a1 (2 * n - k) ≤ xn a1 n
⊢ xn a1 k % xn a1 n = (xn a1 n - xn a1 (2 * n - k)) % xn a1 n
apply ModEq.add_right_cancel' (xn a1 (2 * n - k))
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n :=
  lt_of_add_lt_add_right
    (let_fun this :=
      Eq.mpr (id (tsub_add_cancel_of_le k2n ▸ Eq.refl (2 * n - k + k < n + k)))
        (Eq.mpr (id (two_mul n ▸ Eq.refl (2 * n < n + k))) (add_lt_add_left kn n));
    this)
xle : xn a1 (2 * n - k) ≤ xn a1 n
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n [MOD xn a1 n]
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n :=
  lt_of_add_lt_add_right
    (let_fun this :=
      Eq.mpr (id (tsub_add_cancel_of_le k2n ▸ Eq.refl (2 * n - k + k < n + k)))
        (Eq.mpr (id (two_mul n ▸ Eq.refl (2 * n < n + k))) (add_lt_add_left kn n));
    this)
xle : xn a1 (2 * n - k) ≤ xn a1 n
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n - xn a1 (2 * n - k) + xn a1 (2 * n - k) [MOD xn a1 n]
rw [tsub_add_cancel_of_le xle]
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n :=
  lt_of_add_lt_add_right
    (let_fun this :=
      Eq.mpr (id (tsub_add_cancel_of_le k2n ▸ Eq.refl (2 * n - k + k < n + k)))
        (Eq.mpr (id (two_mul n ▸ Eq.refl (2 * n < n + k))) (add_lt_add_left kn n));
    this)
xle : xn a1 (2 * n - k) ≤ xn a1 n
t : xn a1 (2 * n - (2 * n - k)) + xn a1 (2 * n - k) ≡ 0 [MOD xn a1 n]
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n [MOD xn a1 n]
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n :=
  lt_of_add_lt_add_right
    (let_fun this :=
      Eq.mpr (id (tsub_add_cancel_of_le k2n ▸ Eq.refl (2 * n - k + k < n + k)))
        (Eq.mpr (id (two_mul n ▸ Eq.refl (2 * n < n + k))) (add_lt_add_left kn n));
    this)
xle : xn a1 (2 * n - k) ≤ xn a1 n
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n [MOD xn a1 n]
have t := xn_modEq_x2n_sub_lem a1 k2nl.le
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n :=
  lt_of_add_lt_add_right
    (let_fun this :=
      Eq.mpr (id (tsub_add_cancel_of_le k2n ▸ Eq.refl (2 * n - k + k < n + k)))
        (Eq.mpr (id (two_mul n ▸ Eq.refl (2 * n < n + k))) (add_lt_add_left kn n));
    this)
xle : xn a1 (2 * n - k) ≤ xn a1 n
t : xn a1 k + xn a1 (2 * n - k) ≡ 0 [MOD xn a1 n]
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n [MOD xn a1 n]
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n :=
  lt_of_add_lt_add_right
    (let_fun this :=
      Eq.mpr (id (tsub_add_cancel_of_le k2n ▸ Eq.refl (2 * n - k + k < n + k)))
        (Eq.mpr (id (two_mul n ▸ Eq.refl (2 * n < n + k))) (add_lt_add_left kn n));
    this)
xle : xn a1 (2 * n - k) ≤ xn a1 n
t : xn a1 (2 * n - (2 * n - k)) + xn a1 (2 * n - k) ≡ 0 [MOD xn a1 n]
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n [MOD xn a1 n]
rw [tsub_tsub_cancel_of_le k2n] at t
no goals
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n :=
  lt_of_add_lt_add_right
    (let_fun this :=
      Eq.mpr (id (tsub_add_cancel_of_le k2n ▸ Eq.refl (2 * n - k + k < n + k)))
        (Eq.mpr (id (two_mul n ▸ Eq.refl (2 * n < n + k))) (add_lt_add_left kn n));
    this)
xle : xn a1 (2 * n - k) ≤ xn a1 n
t : xn a1 k + xn a1 (2 * n - k) ≡ 0 [MOD xn a1 n]
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n [MOD xn a1 n]
exact t.trans dvd_rfl.zero_modEq_nat
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
⊢ 2 * n < n + k

a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
⊢ k ≤ 2 * n
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
⊢ 2 * n - k + k < n + k
rw [tsub_add_cancel_of_le]
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
⊢ n + n < n + k

a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
⊢ k ≤ 2 * n
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
⊢ 2 * n < n + k

a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
⊢ k ≤ 2 * n
rw [two_mul]
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
⊢ k ≤ 2 * n
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
⊢ n + n < n + k

a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
⊢ k ≤ 2 * n
exact add_lt_add_left kn n
no goals
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
⊢ k ≤ 2 * n
exact k2n
no goals
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n :=
  lt_of_add_lt_add_right
    (let_fun this :=
      Eq.mpr (id (tsub_add_cancel_of_le k2n ▸ Eq.refl (2 * n - k + k < n + k)))
        (Eq.mpr (id (two_mul n ▸ Eq.refl (2 * n < n + k))) (add_lt_add_left kn n));
    this)
xle : xn a1 (2 * n - k) ≤ xn a1 n
this : xn a1 k % xn a1 n = xn a1 n - xn a1 (2 * n - k)
⊢ ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
rw [this, Int.ofNat_sub xle]
case refl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
⊢ xn a1 i % xn a1 n < xn a1 (n + 1) % xn a1 n
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
o : j = n ∨ n < j
jn : j = n
⊢ xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n
cases jn
case refl.a
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
⊢ ↑(xn a1 i % xn a1 n) < ↑(xn a1 (n + 1) % xn a1 n)
case refl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
⊢ xn a1 i % xn a1 n < xn a1 (n + 1) % xn a1 n
apply Int.lt_of_ofNat_lt_ofNat
case refl.a
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
⊢ ↑(xn a1 i % xn a1 n) < ↑(xn a1 n) - ↑(xn a1 (n - 1))
case refl.a
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
⊢ ↑(xn a1 i % xn a1 n) < ↑(xn a1 (n + 1) % xn a1 n)
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]]
case refl.a
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
⊢ xn a1 (n - 1) + xn a1 i % xn a1 n < xn a1 n
case refl.a
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
⊢ ↑(xn a1 i % xn a1 n) < ↑(xn a1 n) - ↑(xn a1 (n - 1))
refine' lt_sub_left_of_add_lt (Int.ofNat_lt_ofNat_of_lt _)
case refl.a.inl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
⊢ xn a1 (n - 1) + xn a1 i % xn a1 n < xn a1 n

case refl.a.inr
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
ein : i = n
⊢ xn a1 (n - 1) + xn a1 i % xn a1 n < xn a1 n
case refl.a
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
⊢ xn a1 (n - 1) + xn a1 i % xn a1 n < xn a1 n
cases' lt_or_eq_of_le <| Nat.le_of_succ_le_succ ij with lin ein
no goals
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
⊢ 2 * n - (n + 1) = n - 1
rw [two_mul, tsub_add_eq_tsub_tsub, add_tsub_cancel_right]
case refl.a.inl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
⊢ xn a1 (n - 1) + xn a1 i < xn a1 n
case refl.a.inl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
⊢ xn a1 (n - 1) + xn a1 i % xn a1 n < xn a1 n
rw [Nat.mod_eq_of_lt (strictMono_x _ lin)]
case refl.a.inl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
⊢ xn a1 (n - 1) + xn a1 i < xn a1 n
case refl.a.inl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
⊢ xn a1 (n - 1) + xn a1 i < xn a1 n
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 _ _)
case refl.a.inl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
⊢ xn a1 (n - 1) + xn a1 i < xn a1 n
case refl.a.inl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
⊢ xn a1 (n - 1) + xn a1 i < xn a1 n
have npm : (n - 1).succ = n := Nat.succ_pred_eq_of_pos npos
case refl.a.inl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
il : i ≤ n - 1
⊢ xn a1 (n - 1) + xn a1 i < xn a1 n
case refl.a.inl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
⊢ xn a1 (n - 1) + xn a1 i < xn a1 n
have il : i ≤ n - 1 := by
  apply Nat.le_of_succ_le_succ
  rw [npm]
  exact lin
case refl.a.inl.inl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
il : i ≤ n - 1
ill : i < n - 1
⊢ xn a1 (n - 1) + xn a1 i < xn a1 n

case refl.a.inl.inr
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
il : i ≤ n - 1
ile : i = n - 1
⊢ xn a1 (n - 1) + xn a1 i < xn a1 n
case refl.a.inl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
il : i ≤ n - 1
⊢ xn a1 (n - 1) + xn a1 i < xn a1 n
cases' lt_or_eq_of_le il with ill ile
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
⊢ xn a1 (n - 1) * 2 ≤ xn a1 (n - 1) * a + Pell.d a1 * yn a1 (n - 1)
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
⊢ xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
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]
no goals
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
⊢ xn a1 (n - 1) * 2 ≤ xn a1 (n - 1) * a + Pell.d a1 * yn a1 (n - 1)
exact le_trans (Nat.mul_le_mul_left _ a1) (Nat.le_add_right _ _)
no goals
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
⊢ xn a1 n = xn a1 (n - 1 + 1)
rw [tsub_add_cancel_of_le (succ_le_of_lt npos)]
case a
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
⊢ succ i ≤ succ (n - 1)
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
⊢ i ≤ n - 1
apply Nat.le_of_succ_le_succ
case a
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
⊢ succ i ≤ n
case a
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
⊢ succ i ≤ succ (n - 1)
rw [npm]
no goals
case a
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
⊢ succ i ≤ n
exact lin
no goals
case refl.a.inl.inl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
il : i ≤ n - 1
ill : i < n - 1
⊢ xn a1 (n - 1) + xn a1 i < xn a1 n
exact lt_of_lt_of_le (Nat.add_lt_add_left (strictMono_x a1 ill) _) ll
case refl.a.inl.inr
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
il : i ≤ n - 1
ile : i = n - 1
⊢ xn a1 (n - 1) + xn a1 (n - 1) < xn a1 n
case refl.a.inl.inr
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
il : i ≤ n - 1
ile : i = n - 1
⊢ xn a1 (n - 1) + xn a1 i < xn a1 n
rw [ile]
case refl.a.inl.inr
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
il : i ≤ n - 1
ile : i = n - 1
⊢ xn a1 (n - 1) + xn a1 (n - 1) ≠ xn a1 n
case refl.a.inl.inr
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
il : i ≤ n - 1
ile : i = n - 1
⊢ xn a1 (n - 1) + xn a1 (n - 1) < xn a1 n
apply lt_of_le_of_ne ll
case refl.a.inl.inr
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
il : i ≤ n - 1
ile : i = n - 1
⊢ 2 * xn a1 (n - 1) ≠ xn a1 n
case refl.a.inl.inr
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
il : i ≤ n - 1
ile : i = n - 1
⊢ xn a1 (n - 1) + xn a1 (n - 1) ≠ xn a1 n
rw [← two_mul]
no goals
case refl.a.inl.inr
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
il : i ≤ n - 1
ile : i = n - 1
⊢ 2 * xn a1 (n - 1) ≠ xn a1 n
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⟩
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
il : i ≤ n - 1
ile : i = n - 1
e : 2 * xn a1 (n - 1) = xn a1 n
a2 : a = 2
s1 : n - 1 = 0
⊢ a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
il : i ≤ n - 1
ile : i = n - 1
e : 2 * xn a1 (n - 1) = xn a1 n
⊢ a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2
let ⟨a2, s1⟩ :=
  @eq_of_xn_modEq_lem2 _ a1 (n - 1)
    (by rwa [tsub_add_cancel_of_le (succ_le_of_lt npos)])
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
il : i ≤ n - 1
ile : i = n - 1
e : 2 * xn a1 (n - 1) = xn a1 n
a2 : a = 2
s1 : n - 1 = 0
n1 : n = 1
⊢ a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
il : i ≤ n - 1
ile : i = n - 1
e : 2 * xn a1 (n - 1) = xn a1 n
a2 : a = 2
s1 : n - 1 = 0
⊢ a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2
have n1 : n = 1 := le_antisymm (tsub_eq_zero_iff_le.mp s1) npos
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
il : i ≤ n - 1
ile : i = n - 1
e : 2 * xn a1 (n - 1) = xn a1 n
a2 : a = 2
s1 : n - 1 = 0
n1 : n = 1
⊢ 2 = 2 ∧ 1 = 1 ∧ 1 - 1 = 0 ∧ 1 + 1 = 2
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
il : i ≤ n - 1
ile : i = n - 1
e : 2 * xn a1 (n - 1) = xn a1 n
a2 : a = 2
s1 : n - 1 = 0
n1 : n = 1
⊢ a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2
rw [ile, a2, n1]
no goals
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
il : i ≤ n - 1
ile : i = n - 1
e : 2 * xn a1 (n - 1) = xn a1 n
a2 : a = 2
s1 : n - 1 = 0
n1 : n = 1
⊢ 2 = 2 ∧ 1 = 1 ∧ 1 - 1 = 0 ∧ 1 + 1 = 2
exact ⟨rfl, rfl, rfl, rfl⟩
no goals
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : succ (n - 1) = n
il : i ≤ n - 1
ile : i = n - 1
e : 2 * xn a1 (n - 1) = xn a1 n
⊢ 2 * xn a1 (n - 1) = xn a1 (n - 1 + 1)
rwa [tsub_add_cancel_of_le (succ_le_of_lt npos)]
case refl.a.inr
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
ein : i = n
⊢ xn a1 (n - 1) < xn a1 n
case refl.a.inr
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
ein : i = n
⊢ xn a1 (n - 1) + xn a1 i % xn a1 n < xn a1 n
rw [ein, Nat.mod_self, add_zero]
no goals
case refl.a.inr
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
ein : i = n
⊢ xn a1 (n - 1) < xn a1 n
exact strictMono_x _ (Nat.pred_lt npos.ne')
a : ℕ
a1✝ : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : 2 + 1 ≤ 2 * 1
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1✝ k % xn a1✝ n) = ↑(xn a1✝ n) - ↑(xn a1✝ (2 * n - k))
o : j = n ∨ n < j
jn✝ : j > n
jn : j ≠ n
s : xn a1✝ j % xn a1✝ n < xn a1✝ (j + 1) % xn a1✝ n
h : i < j
x✝ : a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2
a1 : a = 2
n1 : n = 1
i0 : i = 0
j2 : j = 2
⊢ False
a : ℕ
a1✝ : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1✝ k % xn a1✝ n) = ↑(xn a1✝ n) - ↑(xn a1✝ (2 * n - k))
o : j = n ∨ n < j
jn✝ : j > n
jn : j ≠ n
s : xn a1✝ j % xn a1✝ n < xn a1✝ (j + 1) % xn a1✝ n
h : i < j
x✝ : a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2
a1 : a = 2
n1 : n = 1
i0 : i = 0
j2 : j = 2
⊢ False
rw [n1, j2] at j2n
no goals
a : ℕ
a1✝ : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : 2 + 1 ≤ 2 * 1
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1✝ k % xn a1✝ n) = ↑(xn a1✝ n) - ↑(xn a1✝ (2 * n - k))
o : j = n ∨ n < j
jn✝ : j > n
jn : j ≠ n
s : xn a1✝ j % xn a1✝ n < xn a1✝ (j + 1) % xn a1✝ n
h : i < j
x✝ : a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2
a1 : a = 2
n1 : n = 1
i0 : i = 0
j2 : j = 2
⊢ False
exact absurd j2n (by decide)
no goals
a : ℕ
a1✝ : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : 2 + 1 ≤ 2 * 1
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1✝ k % xn a1✝ n) = ↑(xn a1✝ n) - ↑(xn a1✝ (2 * n - k))
o : j = n ∨ n < j
jn✝ : j > n
jn : j ≠ n
s : xn a1✝ j % xn a1✝ n < xn a1✝ (j + 1) % xn a1✝ n
h : i < j
x✝ : a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2
a1 : a = 2
n1 : n = 1
i0 : i = 0
j2 : j = 2
⊢ ¬2 + 1 ≤ 2 * 1
decide
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
o : j = n ∨ n < j
jn✝ : j > n
jn : j ≠ n
s : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
h : i = j
⊢ xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
o : j = n ∨ n < j
jn✝ : j > n
jn : j ≠ n
s : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
h : i = j
⊢ xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n
rw [h]
no goals
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
o : j = n ∨ n < j
jn✝ : j > n
jn : j ≠ n
s : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
h : i = j
⊢ xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
exact s
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
o : j = n ∨ n < j
jn : j > n
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
⊢ ↑(xn a1 n) - ↑(xn a1 (2 * n - j)) < ↑(xn a1 n) - ↑(xn a1 (2 * n - (j + 1)))
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
o : j = n ∨ n < j
jn : j > n
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
⊢ ↑(xn a1 j % xn a1 n) < ↑(xn a1 (j + 1) % xn a1 n)
rw [lem2 j jn (le_of_lt j2n), lem2 (j + 1) (Nat.le_succ_of_le jn) j2n]
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
o : j = n ∨ n < j
jn : j > n
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
⊢ 2 * n - (j + 1) < 2 * n - j
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
o : j = n ∨ n < j
jn : j > n
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
⊢ ↑(xn a1 n) - ↑(xn a1 (2 * n - j)) < ↑(xn a1 n) - ↑(xn a1 (2 * n - (j + 1)))
refine' sub_lt_sub_left (Int.ofNat_lt_ofNat_of_lt <| strictMono_x _ _) _
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
o : j = n ∨ n < j
jn : j > n
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
⊢ pred (2 * n - j) < 2 * n - j
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
o : j = n ∨ n < j
jn : j > n
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
⊢ 2 * n - (j + 1) < 2 * n - j
rw [Nat.sub_succ]
no goals
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ (k : ℕ), k > n → k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
o : j = n ∨ n < j
jn : j > n
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
⊢ pred (2 * n - j) < 2 * n - j
exact Nat.pred_lt (_root_.ne_of_gt <| tsub_pos_of_lt j2n)