Redefine \min and \max in function_scope

classical/mathcomp_extra.v

@@ -15,8 +15,6 @@ From mathcomp Require Import finset interval.
 (******************************************************************************)
 (* This files contains lemmas and definitions missing from MathComp.          *)
 (*                                                                            *)
-(*               f \max g := fun x => Num.max (f x) (g x)                     *)
-(*               f \min g := fun x => Num.min (f x) (g x)                     *)
 (*                oflit f := Some \o f                                        *)
 (*          pred_oapp T D := [pred x | oapp (mem D) false x]                  *)
 (*                 f \* g := fun x => f x * g x                               *)
@@ -39,10 +37,12 @@ Unset Printing Implicit Defensive.
 Reserved Notation "f \* g" (at level 40, left associativity).
 Reserved Notation "f \- g" (at level 50, left associativity).
 Reserved Notation "\- f"  (at level 35, f at level 35).
-Reserved Notation "f \max g" (at level 50, left associativity).
 
 Number Notation positive Pos.of_num_int Pos.to_num_uint : AC_scope.
 
+Notation "f \min g" := (Order.min_fun f g) : function_scope.
+Notation "f \max g" := (Order.max_fun f g) : function_scope.
+
 Lemma all_sig2_cond {I : Type} {T : Type} (D : pred I)
    (P Q : I -> T -> Prop) : T ->
     (forall x : I, D x -> {y : T | P x y & Q x y}) ->
@@ -305,10 +305,6 @@ Qed.
 Lemma eqbLR (b1 b2 : bool) : b1 = b2 -> b1 -> b2.
 Proof. by move->. Qed.
 
-Definition max_fun T (R : numDomainType) (f g : T -> R) x := Num.max (f x) (g x).
-Notation "f \max g" := (max_fun f g) : ring_scope.
-Arguments max_fun {T R} _ _ _ /.
-
 Lemma gtr_opp (R : numDomainType) (r : R) : (0 < r)%R -> (- r < r)%R.
 Proof. by move=> n0; rewrite -subr_lt0 -opprD oppr_lt0 addr_gt0. Qed.
 
@@ -831,12 +827,6 @@ rewrite horner_poly !big_ord_recr !big_ord0/= !Monoid.simpm/= expr1.
 by rewrite -mulrA -expr2 addrC addrA addrAC.
 Qed.
 
-Reserved Notation "f \min g" (at level 50, left associativity).
-
-Definition min_fun T (R : numDomainType) (f g : T -> R) x := Num.min (f x) (g x).
-Notation "f \min g" := (min_fun f g) : ring_scope.
-Arguments min_fun {T R} _ _ _ /.
-
 (* NB: Coq 8.17.0 generalizes dependent_choice from Set to Type
    making the following lemma redundant *)
 Section dependent_choice_Type.