case inr hm =>
cases n.eq_zero_or_pos
case inl hn =>
  cases hn; simp [Nat.mod_zero]
case inr hn =>
  conv =>
    rhs;
    rw [←Nat.div_add_mod l (m*n)]
    rw [Nat.add_comm, Nat.mul_assoc, Nat.add_mul_div_left _ _ hm]
    rw [Nat.add_mul_mod_self_left]
  apply (Nat.mod_eq_of_lt ?_).symm
  apply (div_lt_iff_lt_mul hm).mpr
  rw [Nat.mul_comm]
  exact Nat.mod_lt l (Nat.mul_pos hn hm)
l m n : Nat
hm : m > 0
⊢ l % (m * n) / m = l / m % n
no goals