proveit.numbers.
less_numeric_rationals
Return True iff a < b. a and b must be numeric rational expressions.