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