conv => rhs; rw [← Nat.mul_div_right n (Nat.zero_lt_succ b)]
case succ
n a b : ℕ
hab : a ≤ Nat.succ b
⊢ a * n / Nat.succ b ≤ n
case succ
n a b : ℕ
hab : a ≤ Nat.succ b
⊢ a * n / Nat.succ b ≤ Nat.succ b * n / Nat.succ b