no goals
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
⊢ 2 * n ≤ 2 * n
rw [Nat.succ_mul]
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ xn a1 (4 * n - j) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n]
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ xn a1 (4 * n - j) + xn a1 (2 * n - j) ≡ xn a1 j + xn a1 (2 * n - j) [MOD xn a1 n]
refine' @ModEq.trans _ _ 0 _ _ (by rw [add_comm]; exact (xn_modEq_x2n_sub _ h).symm)
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ xn a1 (2 * n + (2 * n - j)) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n]
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ xn a1 (4 * n - j) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n]
rw [show 4 * n = 2 * n + 2 * n from right_distrib 2 2 n, add_tsub_assoc_of_le h']
no goals
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ xn a1 (2 * n + (2 * n - j)) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n]
apply xn_modEq_x2n_add
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ 0 ≡ xn a1 (2 * n - j) + xn a1 j [MOD xn a1 n]
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ 0 ≡ xn a1 j + xn a1 (2 * n - j) [MOD xn a1 n]
rw [add_comm]
no goals
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ 0 ≡ xn a1 (2 * n - j) + xn a1 j [MOD xn a1 n]
exact (xn_modEq_x2n_sub _ h).symm