{
  sorry
}
case inl
n k : ℕ
hk_le_n : k ≤ n
hn : n = 0
⊢ (n C k) = (n C n - k)

case inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
⊢ (n C k) = (n C n - k)
case inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
⊢ (n C k) = (n C n - k)