a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
h1 : xz a1 n ∣ ↑(Pell.d a1) * yz a1 n * yz a1 (n - j) + xz a1 j
⊢ xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]
have h1 : xz a1 n ∣ d a1 * yz a1 n * yz a1 (n - j) + xz a1 j := by
  rw [yz_sub _ h, mul_sub_left_distrib, sub_add_eq_add_sub]
  exact
    dvd_sub
      (by
        delta xz; delta yz
        rw [mul_comm (xn _ _ : ℤ)]
        exact_mod_cast (xn_modEq_x2n_add_lem _ n j))
      ((dvd_mul_right _ _).mul_left _)
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
h1 : xz a1 n ∣ ↑(Pell.d a1) * yz a1 n * yz a1 (n - j) + xz a1 j
⊢ xn a1 n * xn a1 (n - j) + (Pell.d a1 * yn a1 n * yn a1 (n - j) + xn a1 j) ≡ 0 + 0 [MOD xn a1 n]
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
h1 : xz a1 n ∣ ↑(Pell.d a1) * yz a1 n * yz a1 (n - j) + xz a1 j
⊢ xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]
rw [two_mul, add_tsub_assoc_of_le h, xn_add, add_assoc, ← zero_add 0]
no goals
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
h1 : xz a1 n ∣ ↑(Pell.d a1) * yz a1 n * yz a1 (n - j) + xz a1 j
⊢ xn a1 n * xn a1 (n - j) + (Pell.d a1 * yn a1 n * yn a1 (n - j) + xn a1 j) ≡ 0 + 0 [MOD xn a1 n]
exact
  (dvd_mul_right _ _).modEq_zero_nat.add
    (Int.coe_nat_dvd.1 <| by simpa [xz, yz] using h1).modEq_zero_nat
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ xz a1 n ∣ ↑(Pell.d a1) * yz a1 n * (xz a1 j * yz a1 n) + xz a1 j - ↑(Pell.d a1) * yz a1 n * (xz a1 n * yz a1 j)
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ xz a1 n ∣ ↑(Pell.d a1) * yz a1 n * yz a1 (n - j) + xz a1 j
rw [yz_sub _ h, mul_sub_left_distrib, sub_add_eq_add_sub]
no goals
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ xz a1 n ∣ ↑(Pell.d a1) * yz a1 n * (xz a1 j * yz a1 n) + xz a1 j - ↑(Pell.d a1) * yz a1 n * (xz a1 n * yz a1 j)
exact
  dvd_sub
    (by
      delta xz; delta yz
      rw [mul_comm (xn _ _ : ℤ)]
      exact_mod_cast (xn_modEq_x2n_add_lem _ n j))
    ((dvd_mul_right _ _).mul_left _)
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ ↑(xn a1 n) ∣ ↑(Pell.d a1) * yz a1 n * (↑(xn a1 j) * yz a1 n) + ↑(xn a1 j)
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ xz a1 n ∣ ↑(Pell.d a1) * yz a1 n * (xz a1 j * yz a1 n) + xz a1 j
delta xz
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ ↑(xn a1 n) ∣ ↑(Pell.d a1) * ↑(yn a1 n) * (↑(xn a1 j) * ↑(yn a1 n)) + ↑(xn a1 j)
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ ↑(xn a1 n) ∣ ↑(Pell.d a1) * yz a1 n * (↑(xn a1 j) * yz a1 n) + ↑(xn a1 j)
delta yz
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ ↑(xn a1 n) ∣ ↑(Pell.d a1) * ↑(yn a1 n) * (↑(yn a1 n) * ↑(xn a1 j)) + ↑(xn a1 j)
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ ↑(xn a1 n) ∣ ↑(Pell.d a1) * ↑(yn a1 n) * (↑(xn a1 j) * ↑(yn a1 n)) + ↑(xn a1 j)
rw [mul_comm (xn _ _ : ℤ)]
no goals
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ ↑(xn a1 n) ∣ ↑(Pell.d a1) * ↑(yn a1 n) * (↑(yn a1 n) * ↑(xn a1 j)) + ↑(xn a1 j)
exact_mod_cast (xn_modEq_x2n_add_lem _ n j)
no goals
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
h1 : xz a1 n ∣ ↑(Pell.d a1) * yz a1 n * yz a1 (n - j) + xz a1 j
⊢ ↑(xn a1 n) ∣ ↑(Pell.d a1 * yn a1 n * yn a1 (n - j) + xn a1 j)
simpa [xz, yz] using h1