{ apply lt_of_not_le
  rewrite [← Nat.sub_eq_zero_iff_le]
  assumption }
case this
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k < n

n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
this : k < n
⊢ k ≤ n
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
this : k < n
⊢ k ≤ n