Add maximum of two real numbers to iset.mm (#2386)
Add maximum of two real numbers to iset.mm (#2386)

Includes maxcom which has a very simple proof but which seems worth
stating because it signifies "the maximum of two reals is commutative".

Includes maxabsle which shows that the maximum expressed in terms of
absolute value is an upper bound for { A , B }

Includes maxabslemab which is part of the least upper bound proof.
Includes maxabslemlub whch shows that the maximum expressed in terms of
absolute value is a least upper bound.

Includes maxabs which is the key result which gives a closed form (in
terms of absolute value) for the maximum of two real numbers.

Includes maxabslemval which is another way to state the existence of the
supremum.

Includes maxleim which is the value of the supremum when we know which
value is larger. Also includes maxleb a biconditional version thereof.

Includes maxle1 and maxle2 which say that each number is no greater
than their maximum.

Includes maxleast which says the maximum is a least upper bound.

Includes maxcl which says the maximum is a real number.

Includes dfabsmax whch is an equality for the absolute value of a real
number in terms of maximum.
metamath/set.mm,metamath/set.mm,metamath/set.mm