apply Nat.lt_of_le_of_lt (m := m - k - n)
m k n : Nat
hkm : k < m
hn : n > 0
⊢ m - (k + n) < m - k
case h₁
m k n : Nat
hkm : k < m
hn : n > 0
⊢ m - (k + n) ≤ m - k - n

case h₂
m k n : Nat
hkm : k < m
hn : n > 0
⊢ m - k - n < m - k