Comparability in a numDomainType

amounts to the difference being real, and consequences

2 files changed, 22 insertions, 2 deletions

diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index edcca42..69fc44e 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -3761,6 +3761,9 @@ Variables (subS : zmodPred S) (kS : keyed_pred subS).
 Lemma rpredB : {in kS &, forall u v, u - v \in kS}.
 Proof. by move=> u v Su Sv; rewrite /= rpredD ?rpredN. Qed.
 
+Lemma rpredBC u v : u - v \in kS = (v - u \in kS).
+Proof. by rewrite -rpredN opprB. Qed.
+
 Lemma rpredMNn n : {in kS, forall u, u *- n \in kS}.
 Proof. by move=> u Su; rewrite /= rpredN rpredMn. Qed.
 
@@ -5800,6 +5803,7 @@ Definition rpred_sum := rpred_sum.
 Definition rpredMn := rpredMn.
 Definition rpredN := rpredN.
 Definition rpredB := rpredB.
+Definition rpredBC := rpredBC.
 Definition rpredMNn := rpredMNn.
 Definition rpredDr := rpredDr.
 Definition rpredDl := rpredDl.
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 45a79b8..b3df199 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -1496,6 +1496,23 @@ Definition subr_lte0 := (subr_le0, subr_lt0).
 Definition subr_gte0 := (subr_ge0, subr_gt0).
 Definition subr_cp0 := (subr_lte0, subr_gte0).
 
+(* Comparability in a numDomain *)
+
+Lemma comparabler0 x : (x >=< 0)%R = (x \is Num.real).
+Proof. by rewrite comparable_sym. Qed.
+
+Lemma subr_comparable0 x y : (x - y >=< 0)%R = (x >=< y)%R.
+Proof. by rewrite /comparable subr_ge0 subr_le0. Qed.
+
+Lemma comparablerE x y : (x >=< y)%R = (x - y \is Num.real).
+Proof. by rewrite -comparabler0 subr_comparable0. Qed.
+
+Lemma  comparabler_trans : transitive (comparable : rel R).
+Proof.
+move=> y x z; rewrite !comparablerE => xBy_real yBz_real.
+by have := rpredD xBy_real yBz_real; rewrite addrA addrNK.
+Qed.
+
 (* Ordered ring properties. *)
 
 Definition lter01 := (ler01, ltr01).
@@ -1622,9 +1639,8 @@ Proof. exact: rpredB. Qed.
 Lemma realN : {mono (@GRing.opp R) : x /  x \is real}.
 Proof. exact: rpredN. Qed.
 
-(* :TODO: add a rpredBC in ssralg *)
 Lemma realBC x y : (x - y \is real) = (y - x \is real).
-Proof. by rewrite -realN opprB. Qed.
+Proof. exact: rpredBC. Qed.
 
 Lemma realD : {in real &, forall x y, x + y \is real}.
 Proof. exact: rpredD. Qed.