Better visibility of the inductive CompSpec used to specify comparison functions

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

1 files changed, 17 insertions, 0 deletions

diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index 20cfb43a3..7e3523a8c 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -857,6 +857,15 @@ Proof.
   symmetry; apply Pcompare_antisym.
 Qed.
 
+Lemma Pcompare_spec : forall p q, CompSpec eq Plt p q ((p ?= q) Eq).
+Proof.
+  intros. destruct ((p ?= q) Eq) as [ ]_eqn; constructor.
+  apply Pcompare_Eq_eq; auto.
+  auto.
+  apply ZC1; auto.
+Qed.
+
+
 (** Comparison and the successor *)
 
 Lemma Pcompare_p_Sp : forall p : positive, (p ?= Psucc p) Eq = Lt.
@@ -932,6 +941,14 @@ Proof.
   destruct (Pcompare_p_Sq n m) as (H',_); destruct (H' H); subst; auto.
 Qed.
 
+Lemma Ple_lteq : forall p q, p <= q <-> p < q \/ p = q.
+Proof.
+  unfold Ple, Plt. intros.
+  generalize (Pcompare_eq_iff p q).
+  destruct ((p ?= q) Eq); intuition; discriminate.
+Qed.
+
+
 (**********************************************************************)
 (** Properties of subtraction on binary positive numbers *)