Library Coq.Reals.Rminmax
Maximum and Minimum of two real numbers
Local Open Scope R_scope.
The functions Rmax and Rmin implement indeed
a maximum and a minimum
We obtain hence all the generic properties of max and min.
Properties specific to the R domain
Compatibilities (consequences of monotonicity)
Anti-monotonicity swaps the role of min and max