have := (Nat.div_lt_iff_lt_mul ‹c>0›).mp hlt
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
this : c > 0
⊢ a / c ≤ b / c
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
this✝ : c > 0
this : b < a / c * c
⊢ a / c ≤ b / c