{
  eliminate h with n0 h
  have : n ≠ 0 := by linarith 
  simp [Choose]
  rewrite [h, Nat.factorial_succ]
  simp
  rewrite [Nat.mul_div_cancel]
  {linarith}
  {apply Nat.factorial_pos}
}
case inr
n : ℕ
h : ∃ n0, n = n0 + 1
⊢ (n C 1) = n
no goals