{
  eliminate (eq_zero_or_ne_zero k) with hk hk
  {sorry}
  {
    eliminate (eq_zero_or_ne_zero (n - k)) with hnk hnk
    {
      sorry
    }
    {
      apply binomial_symmetry_helper
      {sorry}
      {sorry}
      {sorry}
    }
  }
}
case inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
⊢ (n C k) = (n C n - k)
no goals