case h
m : ℕ
⊢ 2 * m + 1 = m + 1 + m
m : ℕ
⊢ choose (2 * m + 1) (m + 1) = choose (2 * m + 1) m
apply choose_symm_of_eq_add
no goals
case h
m : ℕ
⊢ 2 * m + 1 = m + 1 + m
rw [add_comm m 1, add_assoc 1 m m, add_comm (2 * m) 1, two_mul m]