proveit.numbers.
less_numeric_ints
Return True iff a < b. a and b must be numeric integer expressions.