a✝ b✝ m n k a b : ℕ
hb : 0 < b
h : a / b = 0
⊢ a % b < b
a✝ b✝ m n k a b : ℕ
hb : 0 < b
h : a / b = 0
⊢ a < b
rw [← mod_add_div a b, h, mul_zero, add_zero]
no goals
a✝ b✝ m n k a b : ℕ
hb : 0 < b
h : a / b = 0
⊢ a % b < b
exact mod_lt _ hb
no goals
a✝ b✝ m n k a b : ℕ
hb : 0 < b
h : a < b
⊢ a / b = 0
rw [← mul_right_inj' hb.ne', ← @add_left_cancel_iff _ _ _ (a % b), mod_add_div, mod_eq_of_lt h,
  mul_zero, add_zero]