m n k a b : ℕ
hb : 0 < b
⊢ a / b < succ (a / b)
m n k a b : ℕ
hb : 0 < b
⊢ a < a / b * b + b
rw [← Nat.succ_mul, ← Nat.div_lt_iff_lt_mul hb]
no goals
m n k a b : ℕ
hb : 0 < b
⊢ a / b < succ (a / b)
exact Nat.lt_succ_self _