n : ℕ
h : 0 < n
⊢ 2 ∣ centralBinom (succ (pred n))
n : ℕ
h : 0 < n
⊢ 2 ∣ centralBinom n
rw [← Nat.succ_pred_eq_of_pos h]
no goals
n : ℕ
h : 0 < n
⊢ 2 ∣ centralBinom (succ (pred n))
exact two_dvd_centralBinom_succ n.pred