case pos
m n k l : ℕ
n0 : n = 0
⊢ m / n = (m - m % n) / n

case neg
m n k l : ℕ
n0 : ¬n = 0
⊢ m / n = (m - m % n) / n
m n k l : ℕ
⊢ m / n = (m - m % n) / n
by_cases n0 : n = 0
no goals
case pos
m n k l : ℕ
n0 : n = 0
⊢ m / n = (m - m % n) / n
rw [n0, Nat.div_zero, Nat.div_zero]
case neg
m n k l : ℕ
n0 : ¬n = 0
this : m - m % n = n * (m / n)
⊢ m / n = (m - m % n) / n
case neg
m n k l : ℕ
n0 : ¬n = 0
⊢ m / n = (m - m % n) / n
have : m - m % n = n * (m / n) := by
  rw [tsub_eq_iff_eq_add_of_le (Nat.mod_le _ _), add_comm, mod_add_div]
no goals
case neg
m n k l : ℕ
n0 : ¬n = 0
this : m - m % n = n * (m / n)
⊢ m / n = (m - m % n) / n
rw [this, mul_div_right _ (Nat.pos_of_ne_zero n0)]
no goals
m n k l : ℕ
n0 : ¬n = 0
⊢ m - m % n = n * (m / n)
rw [tsub_eq_iff_eq_add_of_le (Nat.mod_le _ _), add_comm, mod_add_div]