cases hm
l m n : Nat
hm : m > 0
hln : l ≥ n
⊢ (l * m - n) % l = (l - n) % l
case refl
l n : Nat
hln : l ≥ n
⊢ (l * succ 0 - n) % l = (l - n) % l

case step
l n : Nat
hln : l ≥ n
m✝ : Nat
a✝ : Nat.le (succ 0) m✝
⊢ (l * succ m✝ - n) % l = (l - n) % l