Add small utility lemmas about nat/P/Z/Q arithmetic.

 Initial patch by Eelis van der Weegen, minor adaptations by myself

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

1 files changed, 23 insertions, 0 deletions

diff --git a/theories/PArith/Pnat.v b/theories/PArith/Pnat.v
index 715c4484d..b3f2493b2 100644
--- a/theories/PArith/Pnat.v
+++ b/theories/PArith/Pnat.v
@@ -227,6 +227,13 @@ rewrite nat_of_P_compare_morphism.
 apply <- nat_compare_eq_iff; auto.
 Qed.
 
+(** Stating this bidirectionally lets us reason equationally with it: *)
+
+Lemma nat_of_P_inj_iff : forall p q, nat_of_P p = nat_of_P q <-> p = q.
+Proof.
+ split; intro. now apply nat_of_P_inj. now subst.
+Qed.
+
 (** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed
     from [compare] on [positive])
 
@@ -240,6 +247,22 @@ Proof.
  apply -> nat_compare_lt; auto.
 Qed.
 
+(** Again, stating this bidirectionally lets us reason equationally with it: *)
+
+Lemma Plt_lt : forall p q, Plt p q <-> lt (nat_of_P p) (nat_of_P q).
+Proof.
+ intros. unfold Plt. rewrite nat_of_P_compare_morphism.
+ apply iff_sym, nat_compare_lt.
+Qed.
+
+(** And the same for Ple *)
+
+Lemma Ple_le : forall p q, Ple p q <-> le (nat_of_P p) (nat_of_P q).
+Proof.
+ intros. unfold Ple. rewrite nat_of_P_compare_morphism.
+ apply iff_sym, nat_compare_le.
+Qed.
+
 (** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed
     from [compare] on [positive])