Merge branch 'robbert/positive_max_min' into 'master'

Add `min` and `max` infix notations for `positive`.

See merge request iris/stdpp!462

CHANGELOG.md

@@ -36,6 +36,7 @@ Coq 8.12 and 8.13 are no longer supported by this release.
 - Add `set_omap` function for finite sets and associated lemmas. (by Dorian
   Lesbre)
 - Add proof that `vec` is `Finite`. (by Herman Bergwerf.)
+- Add `min` and `max` infix notations for `positive`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).

stdpp/numbers.v

@@ -173,6 +173,8 @@ Notation "(≤)" := Pos.le (only parsing) : positive_scope.
 Notation "(<)" := Pos.lt (only parsing) : positive_scope.
 Notation "(~0)" := xO (only parsing) : positive_scope.
 Notation "(~1)" := xI (only parsing) : positive_scope.
+Infix "`max`" := Pos.max : positive_scope.
+Infix "`min`" := Pos.min : positive_scope.
 
 Global Arguments Pos.of_nat : simpl never.
 Global Arguments Pos.mul : simpl never.