cases b with
| zero => simp
| succ b =>
  conv => rhs; rw [← Nat.mul_div_right n (Nat.zero_lt_succ b)]
  apply Nat.div_le_div_right
  exact Nat.mul_le_mul_right _ hab
n a b : ℕ
hab : a ≤ b
⊢ a * n / b ≤ n
no goals