From 1cacfb8f5dd8307adbc48b67474055ce455a168d Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 12 Sep 2020 17:02:00 +0900 Subject: lemma used in mathcomp-analysis Co-authored-by: Cyril Cohen Co-authored-by: Kazuhiko Sakaguchi --- mathcomp/algebra/ssrnum.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) (limited to 'mathcomp') diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 2eefe8e..c28aec2 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -1779,6 +1779,26 @@ move=> hx; rewrite -[X in `|X|]subr0; case: (@real_ltgtP 0 x); by rewrite ?subr0 ?sub0r //; constructor. Qed. +Lemma max_real : {in real &, forall x y, max x y \is real}. +Proof. by move=> x y ? ?; case: real_leP. Qed. + +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. +Proof. +by move=> x0r Pr; elim/big_rec : _ => // i x Pi xr; rewrite max_real ?Pr. +Qed. + +Lemma bigmin_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[min/x0]_(t <- r | P t) f t \is real. +Proof. +by move=> x0r Pr; elim/big_rec : _ => // i x Pi xr; rewrite min_real ?Pr. +Qed. + Lemma real_neqr_lt : {in real &, forall x y, (x != y) = (x < y) || (y < x)}. Proof. by move=> * /=; case: real_ltgtP. Qed. -- cgit v1.2.3 From e2fb620d4a2bb6da26d344b69f22befdde09b1d0 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 16 Sep 2020 01:33:27 +0900 Subject: comparable_big lemma in order.v --- mathcomp/algebra/ssrnum.v | 4 ++-- mathcomp/ssreflect/order.v | 14 ++++++++++++-- 2 files changed, 14 insertions(+), 4 deletions(-) (limited to 'mathcomp') 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. -- cgit v1.2.3 From bf736cf6aaec0bca0d0202b8686d253123bf4af2 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Sat, 26 Sep 2020 23:52:48 +0200 Subject: Reorganizing relation between comparability/real and big --- mathcomp/algebra/ssrnum.v | 29 +++++++++++++++++++---------- mathcomp/ssreflect/order.v | 41 +++++++++++++++++++++-------------------- 2 files changed, 40 insertions(+), 30 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 36498b3..3c88ef0 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -1479,6 +1479,19 @@ rewrite sqrf_eq1 => /orP[/eqP //|]; rewrite -ger0_def le0r oppr_eq0 oner_eq0. by move/(addr_gt0 ltr01); rewrite subrr ltxx. Qed. +Lemma big_real x0 op I (P : pred I) F (s : seq I) : + {in real &, forall x y, op x y \is real} -> x0 \is real -> + {in P, forall i, F i \is real} -> \big[op/x0]_(i <- s | P i) F i \is real. +Proof. exact: comparable_bigr. Qed. + +Lemma sum_real I (P : pred I) (F : I -> R) (s : seq I) : + {in P, forall i, F i \is real} -> \sum_(i <- s | P i) F i \is real. +Proof. by apply/big_real; [apply: rpredD | apply: rpred0]. Qed. + +Lemma prod_real I (P : pred I) (F : I -> R) (s : seq I) : + {in P, forall i, F i \is real} -> \prod_(i <- s | P i) F i \is real. +Proof. by apply/big_real; [apply: rpredM | apply: rpred1]. Qed. + Section NormedZmoduleTheory. Variable V : normedZmodType R. @@ -1780,24 +1793,20 @@ by rewrite ?subr0 ?sub0r //; constructor. Qed. Lemma max_real : {in real &, forall x y, max x y \is real}. -Proof. by move=> x y ? ?; case: real_leP. Qed. +Proof. exact: comparable_maxr. Qed. Lemma min_real : {in real &, forall x y, min x y \is real}. -Proof. by move=> x y ? ?; case: real_leP. Qed. +Proof. exact: comparable_minr. Qed. Lemma bigmax_real I x0 (r : seq I) (P : pred I) (f : I -> R): 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. +Proof. exact/big_real/max_real. Qed. Lemma bigmin_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[min/x0]_(t <- r | P t) f t \is real. -Proof. -by move=> x0r Pr; elim/big_rec : _ => // i x Pi xr; rewrite min_real ?Pr. -Qed. + x0 \is real -> {in P, forall i : I, f i \is real} -> + \big[min/x0]_(i <- r | P i) f i \is real. +Proof. exact/big_real/min_real. Qed. Lemma real_neqr_lt : {in real &, forall x y, (x != y) = (x < y) || (y < x)}. Proof. by move=> * /=; case: real_ltgtP. Qed. diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index c90bc53..cdc181c 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -2973,17 +2973,17 @@ Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP. Qed. Lemma max_maxxK x y : max x (max x y) = max x y. Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP. Qed. -Lemma comparable_minl x y z : x >=< z -> y >=< z -> min x y >=< z. -Proof. by move=> cmp_xz cmp_yz; rewrite /min; case: ifP. Qed. +Lemma comparable_minl z : {in >=< z &, forall x y, min x y >=< z}. +Proof. by move=> x y cmp_xz cmp_yz; rewrite /min; case: ifP. Qed. -Lemma comparable_minr x y z : z >=< x -> z >=< y -> z >=< min x y. -Proof. by move=> cmp_xz cmp_yz; rewrite /min; case: ifP. Qed. +Lemma comparable_minr z : {in >=<%O z &, forall x y, z >=< min x y}. +Proof. by move=> x y cmp_xz cmp_yz; rewrite /min; case: ifP. Qed. -Lemma comparable_maxl x y z : x >=< z -> y >=< z -> max x y >=< z. -Proof. by move=> cmp_xz cmp_yz; rewrite /max; case: ifP. Qed. +Lemma comparable_maxl z : {in >=< z &, forall x y, max x y >=< z}. +Proof. by move=> x y cmp_xz cmp_yz; rewrite /max; case: ifP. Qed. -Lemma comparable_maxr x y z : z >=< x -> z >=< y -> z >=< max x y. -Proof. by move=> cmp_xz cmp_yz; rewrite /max; case: ifP. Qed. +Lemma comparable_maxr z : {in >=<%O z &, forall x y, z >=< max x y}. +Proof. by move=> x y cmp_xz cmp_yz; rewrite /max; case: ifP. Qed. Section Comparable2. Variables (z x y : T) (cmp_xy : x >=< y). @@ -3165,7 +3165,7 @@ Lemma comparable_minACA x y z t : Proof. move=> xy xz xt yz yt zt; rewrite comparable_minA// ?comparable_minl//. rewrite [min _ z]comparable_minAC// -comparable_minA// ?comparable_minl//. -by rewrite comparable_sym. +by rewrite inE comparable_sym. Qed. Lemma comparable_maxACA x y z t : @@ -3174,7 +3174,7 @@ Lemma comparable_maxACA x y z t : Proof. move=> xy xz xt yz yt zt; rewrite comparable_maxA// ?comparable_maxl//. rewrite [max _ z]comparable_maxAC// -comparable_maxA// ?comparable_maxl//. -by rewrite comparable_sym. +by rewrite inE comparable_sym. Qed. Lemma comparable_max_minr x y z : x >=< y -> x >=< z -> y >=< z -> @@ -3226,22 +3226,23 @@ Lemma nmono_in_leif (A : {pred T}) (f : T -> T) C : {in A &, forall x y, (f x <= f y ?= iff C) = (y <= x ?= iff C)}. Proof. by move=> mf x y Ax Ay; rewrite /leif !eq_le !mf. Qed. -Lemma nmono_leif (f : T -> T) C : - {mono f : x y /~ x <= y} -> +Lemma nmono_leif (f : T -> T) C : {mono f : x y /~ x <= y} -> 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_bigl x x0 op I (P : pred I) F (s : seq I) : + {in >=< x &, forall y z, op y z >=< x} -> x0 >=< x -> + {in P, forall i, F i >=< x} -> \big[op/x0]_(i <- s | P i) F i >=< x. +Proof. by move=> *; elim/big_ind : _. Qed. -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. +Lemma comparable_bigr x x0 op I (P : pred I) F (s : seq I) : + {in >=<%O x &, forall y z, x >=< op y z} -> x >=< x0 -> + {in P, forall i, x >=< F i} -> x >=< \big[op/x0]_(i <- s | P i) F i. +Proof. by move=> *; elim/big_ind : _. Qed. End POrderTheory. +Hint Resolve comparable_minr comparable_minl : core. +Hint Resolve comparable_maxr comparable_maxl : core. Section ContraTheory. Context {disp1 disp2 : unit} {T1 : porderType disp1} {T2 : porderType disp2}. -- cgit v1.2.3 From f5840a92d26d4436582e05b60bcd6fcf2a2a18ff Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Sun, 27 Sep 2020 13:35:39 +0200 Subject: Fixing and documenting the change of meaning of `>=< y` --- mathcomp/ssreflect/order.v | 46 +++++++++++++++++----------------------------- 1 file changed, 17 insertions(+), 29 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index cdc181c..da4d59d 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -419,7 +419,7 @@ Reserved Notation ">= y :> T" (at level 35, y at next level). Reserved Notation "< y :> T" (at level 35, y at next level). Reserved Notation "> y :> T" (at level 35, y at next level). Reserved Notation "x >=< y" (at level 70, no associativity). -Reserved Notation ">=< x" (at level 35). +Reserved Notation ">=< y" (at level 35). Reserved Notation ">=< y :> T" (at level 35, y at next level). Reserved Notation "x >< y" (at level 70, no associativity). Reserved Notation ">< x" (at level 35). @@ -454,7 +454,7 @@ Reserved Notation ">=^d y :> T" (at level 35, y at next level). Reserved Notation "<^d y :> T" (at level 35, y at next level). Reserved Notation ">^d y :> T" (at level 35, y at next level). Reserved Notation "x >=<^d y" (at level 70, no associativity). -Reserved Notation ">=<^d x" (at level 35). +Reserved Notation ">=<^d y" (at level 35). Reserved Notation ">=<^d y :> T" (at level 35, y at next level). Reserved Notation "x ><^d y" (at level 70, no associativity). Reserved Notation "><^d x" (at level 35). @@ -1146,9 +1146,6 @@ 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" := ([pred x | comparable x y]) : order_scope. -Notation ">=< y :> T" := (>=< (y : T)) (only parsing) : order_scope. - Notation "x <= y" := (le x y) : order_scope. Notation "x <= y :> T" := ((x : T) <= (y : T)) (only parsing) : order_scope. Notation "x >= y" := (y <= x) (only parsing) : order_scope. @@ -1172,12 +1169,12 @@ 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" := ([pred y | comparable y x]) : order_scope. -Notation ">=< x :> T" := (>=< (x : T)) (only parsing) : order_scope. +Notation ">=< y" := [pred x | comparable x y] : order_scope. +Notation ">=< y :> T" := (>=< (y : T)) (only parsing) : order_scope. Notation "x >=< y" := (comparable x y) : order_scope. -Notation ">< x" := (fun y => ~~ (comparable x y)) : order_scope. -Notation ">< x :> T" := (>< (x : T)) (only parsing) : order_scope. +Notation ">< y" := [pred x | ~~ comparable x y] : order_scope. +Notation ">< y :> T" := (>< (y : T)) (only parsing) : order_scope. Notation "x >< y" := (~~ (comparable x y)) : order_scope. Notation "[ 'arg' 'min_' ( i < i0 | P ) F ]" := @@ -2541,9 +2538,6 @@ Notation "<^d y :> T" := (<^d (y : T)) (only parsing) : order_scope. Notation ">^d y" := (<^d%O y) : order_scope. Notation ">^d y :> T" := (>^d (y : T)) (only parsing) : order_scope. -Notation ">=<^d y" := (>=<^d%O y) : order_scope. -Notation ">=<^d y :> T" := (>=<^d (y : T)) (only parsing) : order_scope. - Notation "x <=^d y" := (<=^d%O x y) : order_scope. Notation "x <=^d y :> T" := ((x : T) <=^d (y : T)) (only parsing) : order_scope. Notation "x >=^d y" := (y <=^d x) (only parsing) : order_scope. @@ -2568,11 +2562,11 @@ Notation "x <^d y ?<= 'if' C :> T" := ((x : T) <^d (y : T) ?<= if C) (only parsing) : order_scope. Notation ">=<^d x" := (>=<^d%O x) : order_scope. -Notation ">=<^d x :> T" := (>=<^d (x : T)) (only parsing) : order_scope. +Notation ">=<^d y :> T" := (>=<^d (y : T)) (only parsing) : order_scope. Notation "x >=<^d y" := (>=<^d%O x y) : order_scope. -Notation "><^d x" := (fun y => ~~ (>=<^d%O x y)) : order_scope. -Notation "><^d x :> T" := (><^d (x : T)) (only parsing) : order_scope. +Notation "><^d y" := [pred x | ~~ dual_comparable x y] : order_scope. +Notation "><^d y :> T" := (><^d (y : T)) (only parsing) : order_scope. Notation "x ><^d y" := (~~ (><^d%O x y)) : order_scope. Notation "x `&^d` y" := (dual_meet x y) : order_scope. @@ -5796,9 +5790,6 @@ Notation "<^p y :> T" := (<^p (y : T)) (only parsing) : order_scope. Notation ">^p y" := (<^p%O y) : order_scope. Notation ">^p y :> T" := (>^p (y : T)) (only parsing) : order_scope. -Notation ">=<^p y" := (>=<^p%O y) : order_scope. -Notation ">=<^p y :> T" := (>=<^p (y : T)) (only parsing) : order_scope. - Notation "x <=^p y" := (<=^p%O x y) : order_scope. Notation "x <=^p y :> T" := ((x : T) <=^p (y : T)) (only parsing) : order_scope. Notation "x >=^p y" := (y <=^p x) (only parsing) : order_scope. @@ -5818,12 +5809,12 @@ Notation "x <=^p y ?= 'iff' C" := ( T" := ((x : T) <=^p (y : T) ?= iff C) (only parsing) : order_scope. -Notation ">=<^p x" := (>=<^p%O x) : order_scope. -Notation ">=<^p x :> T" := (>=<^p (x : T)) (only parsing) : order_scope. +Notation ">=<^p y" := [pred x | >=<^p%O x y] : order_scope. +Notation ">=<^p y :> T" := (>=<^p (y : T)) (only parsing) : order_scope. Notation "x >=<^p y" := (>=<^p%O x y) : order_scope. -Notation "><^p x" := (fun y => ~~ (>=<^p%O x y)) : order_scope. -Notation "><^p x :> T" := (><^p (x : T)) (only parsing) : order_scope. +Notation "><^p y" := [pred x | ~~ (>=<^p%O x y)] : order_scope. +Notation "><^p y :> T" := (><^p (y : T)) (only parsing) : order_scope. Notation "x ><^p y" := (~~ (><^p%O x y)) : order_scope. Notation "x `&^p` y" := (@meet prod_display _ x y) : order_scope. @@ -5909,9 +5900,6 @@ Notation "<^l y :> T" := (<^l (y : T)) (only parsing) : order_scope. Notation ">^l y" := (<^l%O y) : order_scope. Notation ">^l y :> T" := (>^l (y : T)) (only parsing) : order_scope. -Notation ">=<^l y" := (>=<^l%O y) : order_scope. -Notation ">=<^l y :> T" := (>=<^l (y : T)) (only parsing) : order_scope. - Notation "x <=^l y" := (<=^l%O x y) : order_scope. Notation "x <=^l y :> T" := ((x : T) <=^l (y : T)) (only parsing) : order_scope. Notation "x >=^l y" := (y <=^l x) (only parsing) : order_scope. @@ -5931,12 +5919,12 @@ Notation "x <=^l y ?= 'iff' C" := ( T" := ((x : T) <=^l (y : T) ?= iff C) (only parsing) : order_scope. -Notation ">=<^l x" := (>=<^l%O x) : order_scope. -Notation ">=<^l x :> T" := (>=<^l (x : T)) (only parsing) : order_scope. +Notation ">=<^l y" := [pred x | >=<^l%O x y] : order_scope. +Notation ">=<^l y :> T" := (>=<^l (y : T)) (only parsing) : order_scope. Notation "x >=<^l y" := (>=<^l%O x y) : order_scope. -Notation "><^l x" := (fun y => ~~ (>=<^l%O x y)) : order_scope. -Notation "><^l x :> T" := (><^l (x : T)) (only parsing) : order_scope. +Notation "><^l y" := [pred x | ~~ (>=<^l%O x y)] : order_scope. +Notation "><^l y :> T" := (><^l (y : T)) (only parsing) : order_scope. Notation "x ><^l y" := (~~ (><^l%O x y)) : order_scope. Notation meetlexi := (@meet lexi_display _). -- cgit v1.2.3 From d02fbd82f7bfe06c37dfe5edb05d0ed36a82811b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 12 Oct 2020 12:55:06 +0900 Subject: fix the >=< notation in ssrnum as well --- mathcomp/algebra/ssrnum.v | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 3c88ef0..0244891 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -464,9 +464,6 @@ Notation "< y :> T" := (< (y : T)) (only parsing) : ring_scope. Notation "> y" := (lt y) : ring_scope. Notation "> y :> T" := (> (y : T)) (only parsing) : ring_scope. -Notation ">=< y" := (comparable y) : ring_scope. -Notation ">=< y :> T" := (>=< (y : T)) (only parsing) : ring_scope. - Notation "x <= y" := (le x y) : ring_scope. Notation "x <= y :> T" := ((x : T) <= (y : T)) (only parsing) : ring_scope. Notation "x >= y" := (y <= x) (only parsing) : ring_scope. @@ -490,12 +487,12 @@ Notation "x < y ?<= 'if' C" := (lterif x y C) : ring_scope. Notation "x < y ?<= 'if' C :> R" := ((x : R) < (y : R) ?<= if C) (only parsing) : ring_scope. -Notation ">=< x" := (comparable x) : ring_scope. -Notation ">=< x :> T" := (>=< (x : T)) (only parsing) : ring_scope. +Notation ">=< y" := [pred x | comparable x y] : ring_scope. +Notation ">=< y :> T" := (>=< (y : T)) (only parsing) : ring_scope. Notation "x >=< y" := (comparable x y) : ring_scope. -Notation ">< x" := (fun y => ~~ (comparable x y)) : ring_scope. -Notation ">< x :> T" := (>< (x : T)) (only parsing) : ring_scope. +Notation ">< y" := [pred x | ~~ comparable x y] : ring_scope. +Notation ">< y :> T" := (>< (y : T)) (only parsing) : ring_scope. Notation "x >< y" := (~~ (comparable x y)) : ring_scope. Canonical Rpos_keyed. -- cgit v1.2.3