Library Coq.NArith.Pminmax
Maximum and Minimum of two positive numbers
Local Open Scope positive_scope.
The functions Pmax and Pmin implement indeed
a maximum and a minimum
We obtain hence all the generic properties of max and min.
Properties specific to the positive domain
Simplifications
Compatibilities (consequences of monotonicity)