n : ℕ
⊢ centralBinom (n + 1) = 2 * choose (n + 1 + n) n
n : ℕ
⊢ 2 ∣ centralBinom (n + 1)
use (n + 1 + n).choose n
no goals
n : ℕ
⊢ centralBinom (n + 1) = 2 * choose (n + 1 + n) n
rw [centralBinom_eq_two_mul_choose, two_mul, ← add_assoc,
    choose_succ_succ' (n + 1 + n) n, choose_symm_add, ← two_mul]