n : ℕ
h_s : coprime (n + 1) (2 * n + 1)
⊢ n + 1 ∣ centralBinom n
n : ℕ
⊢ n + 1 ∣ centralBinom n
have h_s : (n + 1).coprime (2 * n + 1) := by
  rw [two_mul, add_assoc, coprime_add_self_right, coprime_self_add_left]
  exact coprime_one_left n
n : ℕ
h_s : coprime (n + 1) (2 * n + 1)
⊢ n + 1 ∣ (2 * n + 1) * centralBinom n
n : ℕ
h_s : coprime (n + 1) (2 * n + 1)
⊢ n + 1 ∣ centralBinom n
apply h_s.dvd_of_dvd_mul_left
n : ℕ
h_s : coprime (n + 1) (2 * n + 1)
⊢ 2 * (n + 1) ∣ 2 * ((2 * n + 1) * centralBinom n)
n : ℕ
h_s : coprime (n + 1) (2 * n + 1)
⊢ n + 1 ∣ (2 * n + 1) * centralBinom n
apply Nat.dvd_of_mul_dvd_mul_left zero_lt_two
n : ℕ
h_s : coprime (n + 1) (2 * n + 1)
⊢ (n + 1) * 2 ∣ (n + 1) * centralBinom (n + 1)
n : ℕ
h_s : coprime (n + 1) (2 * n + 1)
⊢ 2 * (n + 1) ∣ 2 * ((2 * n + 1) * centralBinom n)
rw [← mul_assoc, ← succ_mul_centralBinom_succ, mul_comm]
no goals
n : ℕ
h_s : coprime (n + 1) (2 * n + 1)
⊢ (n + 1) * 2 ∣ (n + 1) * centralBinom (n + 1)
exact mul_dvd_mul_left _ (two_dvd_centralBinom_succ n)
n : ℕ
⊢ coprime 1 n
n : ℕ
⊢ coprime (n + 1) (2 * n + 1)
rw [two_mul, add_assoc, coprime_add_self_right, coprime_self_add_left]
no goals
n : ℕ
⊢ coprime 1 n
exact coprime_one_left n