proveit.numbers.
less_eq_numeric_ints
Return True iff a ≤ b. a and b must be numeric integer expressions.