a✝ b✝ m n k a b d : ℕ
hdb : d ∣ b
h : a < b
⊢ d * (a / d) < b
a✝ b✝ m n k a b d : ℕ
hdb : d ∣ b
h : a < b
⊢ a / d < b / d
rw [Nat.lt_div_iff_mul_lt hdb]
no goals
a✝ b✝ m n k a b d : ℕ
hdb : d ∣ b
h : a < b
⊢ d * (a / d) < b
exact lt_of_le_of_lt (mul_div_le a d) h