no goals
m n a✝ b✝ c✝ d a b c : ℕ
hb0 : b = 0
⊢ a / b % c = a % (b * c) / b
simp [hb0]
no goals
m n a✝ b✝ c✝ d a b c : ℕ
hb0 : ¬b = 0
⊢ a / b % c = a % (b * c) / b
rw [← @add_right_cancel_iff _ _ _ (c * (a / b / c)), mod_add_div, Nat.div_div_eq_div_mul, ←
  mul_right_inj' hb0, ← @add_left_cancel_iff _ _ _ (a % b), mod_add_div, mul_add, ←
  @add_left_cancel_iff _ _ _ (a % (b * c) % b), add_left_comm, ← add_assoc (a % (b * c) % b),
  mod_add_div, ← mul_assoc, mod_add_div, mod_mul_right_mod]