comparable_big lemma in order.v

2 files changed, 14 insertions, 4 deletions

diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index c28aec2..36498b3 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -1786,8 +1786,8 @@ Lemma min_real : {in real &, forall x y, min x y \is real}.
 Proof. by move=> x y ? ?; case: real_leP. Qed.
 
 Lemma bigmax_real I x0 (r : seq I) (P : pred I) (f : I -> R):
-  x0 \is real -> {in P, forall t : I, f t \is real} ->
-  \big[max/x0]_(t <- r | P t) f t \is real.
+  x0 \is real -> {in P, forall i : I, f i \is real} ->
+  \big[max/x0]_(i <- r | P i) f i \is real.
 Proof.
 by move=> x0r Pr; elim/big_rec : _ => // i x Pi xr; rewrite max_real ?Pr.
 Qed.
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index b9ed011..c90bc53 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -1146,7 +1146,7 @@ Notation "< y :> T" := (< (y : T)) (only parsing) : order_scope.
 Notation "> y" := (lt y) : order_scope.
 Notation "> y :> T" := (> (y : T)) (only parsing) : order_scope.
 
-Notation ">=< y" := (comparable y) : order_scope.
+Notation ">=< y" := ([pred x | comparable x y]) : order_scope.
 Notation ">=< y :> T" := (>=< (y : T)) (only parsing) : order_scope.
 
 Notation "x <= y" := (le x y) : order_scope.
@@ -1172,7 +1172,7 @@ Notation "x < y ?<= 'if' C" := (lteif x y C) : order_scope.
 Notation "x < y ?<= 'if' C :> T" := ((x : T) < (y : T) ?<= if C)
   (only parsing) : order_scope.
 
-Notation ">=< x" := (comparable x) : order_scope.
+Notation ">=< x" := ([pred y | comparable y x]) : order_scope.
 Notation ">=< x :> T" := (>=< (x : T)) (only parsing) : order_scope.
 Notation "x >=< y" := (comparable x y) : order_scope.
 
@@ -3231,6 +3231,16 @@ Lemma nmono_leif (f : T -> T) C :
   forall x y, (f x <= f y ?= iff C) = (y <= x ?= iff C).
 Proof. by move=> mf x y; rewrite /leif !eq_le !mf. Qed.
 
+Section comparable_big.
+Variables op : T -> T -> T.
+Hypothesis op_comparable : forall z, {in >=< z &, forall x y, op x y >=< z}.
+
+Lemma comparable_big x x0 I (P : pred I) F (s : seq I) :
+  x0 >=< x -> {in P, forall t, F t >=< x} ->
+  \big[op/x0]_(i <- s | P i) F i >=< x.
+Proof. by move=> ? ?; elim/big_ind : _ => // y z; exact: op_comparable. Qed.
+End comparable_big.
+
 End POrderTheory.
 
 Section ContraTheory.