proveit.numbers.
less_eq_numeric_rationals
Return True iff a ≤ b. a and b must be numeric rational expressions.