cases n.eq_zero_or_pos
l m n : Nat
hm : m > 0
⊢ l % (m * n) / m = l / m % n
case inl
l m n : Nat
hm : m > 0
h✝ : n = 0
⊢ l % (m * n) / m = l / m % n

case inr
l m n : Nat
hm : m > 0
h✝ : n > 0
⊢ l % (m * n) / m = l / m % n