Library Coq.NArith.Nminmax
Maximum and Minimum of two N numbers
Local Open Scope N_scope.
The functions Nmax and Nmin 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)