induction m, k using Nat.mod.inductionOn with rw [Nat.div_eq, Nat.mod_eq]
| base x y h => simp only [h, ite_false, Nat.mul_zero, Nat.add_zero]
| ind x y h IH =>
  simp only [h, and_self, ite_true]
  rw [Nat.mul_succ, ← Nat.add_assoc, IH, Nat.sub_add_cancel h.2]
m k : Nat
⊢ m % k + k * (m / k) = m
no goals