diff options
Diffstat (limited to 'mathcomp/ssreflect')
| -rw-r--r-- | mathcomp/ssreflect/order.v | 14 |
1 files changed, 12 insertions, 2 deletions
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. |