proveit.numbers.
number_ordering
Return a conjunction of number ordering relations with a total-ordering style; for example, a < b <= c = d < e