{sorry}
case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k ≠ 0

case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n - k ≠ 0
case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n - k ≠ 0