induction a with
| zero => rfl
| succ n ih => 
  cases n with
  | zero => rfl
  | succ n =>
    rw [Nat.choose,Nat.choose_one_right,mul_add,ih]
    rw [succ_sub_succ_eq_sub,tsub_zero,mul_comm _ n,← add_mul];
    congr; rw [add_comm]
a : ℕ
⊢ 2 * Nat.choose a 2 = a * (a - 1)
no goals