a b : Int
H : 0 < b
⊢ a < b * div a b + b
a b : Int
H : 0 < b
⊢ a < (div a b + 1) * b
rw [Int.add_mul, Int.one_mul, Int.mul_comm]
no goals
a b : Int
H : 0 < b
⊢ a < b * div a b + b
exact Int.lt_add_of_sub_left_lt <| Int.mod_def .. ▸ mod_lt_of_pos _ H