Minimal lemmas about Z.gt, N.gt and co

 The use of these predicate isn't recommended, but let's at least
 allow converting > >=  and < <=

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14109 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 74 insertions, 5 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 2e3b7c49d..779391ed1 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -922,6 +922,44 @@ Set Inline Level 30. (* For inlining only t eq zero one two *)
 Include NProp
  <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
 
+(** Otherwise N stays associated with abstract_scope : (TODO FIX) *)
+Bind Scope N_scope with N.
+
+(** In generic statements, the predicates [lt] and [le] have been
+  favored, whereas [gt] and [ge] don't even exist in the abstract
+  layers. The use of [gt] and [ge] is hence not recommended. We provide
+  here the bare minimal results to related them with [lt] and [le]. *)
+
+Lemma gt_lt n m : n > m -> m < n.
+Proof.
+  unfold lt, gt. intros H. now rewrite <- compare_antisym, H.
+Qed.
+
+Lemma lt_gt n m : n < m -> m > n.
+Proof.
+  unfold lt, gt. intros H. now rewrite <- compare_antisym, H.
+Qed.
+
+Lemma gt_lt_iff n m : n > m <-> m < n.
+Proof.
+  split. apply gt_lt. apply lt_gt.
+Qed.
+
+Lemma ge_le n m : n >= m -> m <= n.
+Proof.
+  unfold le, ge. intros H. contradict H. now apply gt_lt.
+Qed.
+
+Lemma le_ge n m : n <= m -> m >= n.
+Proof.
+  unfold le, ge. intros H. contradict H. now apply lt_gt.
+Qed.
+
+Lemma ge_le_iff n m : n >= m <-> m <= n.
+Proof.
+  split. apply ge_le. apply le_ge.
+Qed.
+
 (** Auxiliary results about right shift on positive numbers,
     used in BinInt *)
 
@@ -1092,6 +1130,7 @@ Notation Nlog2_nonpos := N.log2_nonpos (only parsing).
 Notation Neven_spec := N.even_spec (only parsing).
 Notation Nodd_spec := N.odd_spec (only parsing).
 Notation Nlt_not_eq := N.lt_neq (only parsing).
+Notation Ngt_Nlt := N.gt_lt (only parsing).
 
 (** More complex compatibility facts, expressed as lemmas
     (to preserve scopes for instance) *)
@@ -1105,9 +1144,4 @@ Proof (N.mul_add_distr_l p n m).
 Lemma Nmult_reg_r n m p : p <> 0 -> n * p = m * p -> n = m.
 Proof (fun H => proj1 (N.mul_cancel_r n m p H)).
 
-Lemma Ngt_Nlt n m : n > m -> m < n.
-Proof.
-unfold Ngt, Nlt; intro H. now rewrite <- N.compare_antisym, H.
-Qed.
-
 (** Not kept : Ncompare_n_Sm Nplus_lt_cancel_l *)
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 62f5a0f78..04bb8d881 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1286,6 +1286,41 @@ Include ZProp
 (** Otherwise Z stays associated with abstract_scope : (TODO FIX) *)
 Bind Scope Z_scope with Z.
 
+(** In generic statements, the predicates [lt] and [le] have been
+  favored, whereas [gt] and [ge] don't even exist in the abstract
+  layers. The use of [gt] and [ge] is hence not recommended. We provide
+  here the bare minimal results to related them with [lt] and [le]. *)
+
+Lemma gt_lt n m : n > m -> m < n.
+Proof.
+  unfold lt, gt. intros H. now rewrite <- compare_antisym, H.
+Qed.
+
+Lemma lt_gt n m : n < m -> m > n.
+Proof.
+  unfold lt, gt. intros H. now rewrite <- compare_antisym, H.
+Qed.
+
+Lemma gt_lt_iff n m : n > m <-> m < n.
+Proof.
+  split. apply gt_lt. apply lt_gt.
+Qed.
+
+Lemma ge_le n m : n >= m -> m <= n.
+Proof.
+  unfold le, ge. intros H. contradict H. now apply gt_lt.
+Qed.
+
+Lemma le_ge n m : n <= m -> m >= n.
+Proof.
+  unfold le, ge. intros H. contradict H. now apply lt_gt.
+Qed.
+
+Lemma ge_le_iff n m : n >= m <-> m <= n.
+Proof.
+  split. apply ge_le. apply le_ge.
+Qed.
+
 (** TODO : to add in Numbers *)
 
 Lemma add_shuffle3 n m p : n + (m + p) = m + (n + p).