Deplacement de lemmes de IntMap vers ZArith

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

2 files changed, 46 insertions, 44 deletions

diff --git a/theories/IntMap/Adalloc.v b/theories/IntMap/Adalloc.v
index 32bebd257..e348cfafb 100644
--- a/theories/IntMap/Adalloc.v
+++ b/theories/IntMap/Adalloc.v
@@ -224,50 +224,6 @@ Section AdAlloc.
   (** Moreover, this is optimal: all addresses below [(ad_alloc_opt m)]
       are in [dom m]: *)
 
-  Lemma convert_xH : (convert xH)=(1).
-  Proof.
-    Reflexivity.
-  Qed.
-
-  Lemma positive_to_nat_mult : (p:positive) (n,m:nat)
-      (positive_to_nat p (mult m n))=(mult m (positive_to_nat p n)).
-  Proof.
-    Induction p. Intros. Simpl. Rewrite mult_plus_distr_r. Rewrite <- (mult_plus_distr_r m n n).
-    Rewrite (H (plus n n) m). Reflexivity.
-    Intros. Simpl. Rewrite <- (mult_plus_distr_r m n n). Apply H.
-    Trivial.
-  Qed.
-
-  Lemma positive_to_nat_2 : (p:positive)
-      (positive_to_nat p (2))=(mult (2) (positive_to_nat p (1))).
-  Proof.
-    Intros. Rewrite <- positive_to_nat_mult. Reflexivity.
-  Qed.
-
-  Lemma positive_to_nat_4 : (p:positive)
-      (positive_to_nat p (4))=(mult (2) (positive_to_nat p (2))).
-  Proof.
-    Intros. Rewrite <- positive_to_nat_mult. Reflexivity.
-  Qed.
-
-  Lemma convert_xO : (p:positive) (convert (xO p))=(mult (2) (convert p)).
-  Proof.
-    Induction p. Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2.
-    Rewrite positive_to_nat_4. Rewrite H. Simpl. Rewrite <- plus_Snm_nSm. Reflexivity.
-    Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2. Rewrite positive_to_nat_4.
-    Rewrite H. Reflexivity.
-    Reflexivity.
-  Qed.
-
-  Lemma convert_xI : (p:positive) (convert (xI p))=(S (mult (2) (convert p))).
-  Proof.
-    Induction p. Unfold convert. Simpl. Intro p0. Intro. Rewrite positive_to_nat_2.
-    Rewrite positive_to_nat_4. Inversion H. Rewrite H1. Rewrite <- plus_Snm_nSm. Reflexivity.
-    Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2. Rewrite positive_to_nat_4.
-    Inversion H. Rewrite H1. Reflexivity.
-    Reflexivity.
-  Qed.
-
   Lemma nat_of_ad_double : (a:ad) (nat_of_ad (ad_double a))=(mult (2) (nat_of_ad a)).
   Proof.
     Induction a. Trivial.
diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v
index 55ccb93e6..4ddc6f1cf 100644
--- a/theories/ZArith/fast_integer.v
+++ b/theories/ZArith/fast_integer.v
@@ -785,6 +785,52 @@ Rewrite le_plus_minus_r; [
 | Apply lt_le_weak; Exact (compare_convert_SUPERIEUR x y H)].
 Qed.
 
+(** Misc properties of the injection from positive to nat *)
+
+Lemma convert_xH : (convert xH)=(1).
+Proof.
+  Reflexivity.
+Qed.
+
+Lemma positive_to_nat_mult : (p:positive) (n,m:nat)
+    (positive_to_nat p (mult m n))=(mult m (positive_to_nat p n)).
+Proof.
+  Induction p. Intros. Simpl. Rewrite mult_plus_distr_r. Rewrite <- (mult_plus_distr_r m n n).
+  Rewrite (H (plus n n) m). Reflexivity.
+  Intros. Simpl. Rewrite <- (mult_plus_distr_r m n n). Apply H.
+  Trivial.
+Qed.
+
+Lemma positive_to_nat_2 : (p:positive)
+    (positive_to_nat p (2))=(mult (2) (positive_to_nat p (1))).
+Proof.
+  Intros. Rewrite <- positive_to_nat_mult. Reflexivity.
+Qed.
+
+Lemma positive_to_nat_4 : (p:positive)
+    (positive_to_nat p (4))=(mult (2) (positive_to_nat p (2))).
+Proof.
+  Intros. Rewrite <- positive_to_nat_mult. Reflexivity.
+Qed.
+
+Lemma convert_xO : (p:positive) (convert (xO p))=(mult (2) (convert p)).
+Proof.
+  Induction p. Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2.
+  Rewrite positive_to_nat_4. Rewrite H. Simpl. Rewrite <- plus_Snm_nSm. Reflexivity.
+  Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2. Rewrite positive_to_nat_4.
+  Rewrite H. Reflexivity.
+  Reflexivity.
+Qed.
+
+Lemma convert_xI : (p:positive) (convert (xI p))=(S (mult (2) (convert p))).
+Proof.
+  Induction p. Unfold convert. Simpl. Intro p0. Intro. Rewrite positive_to_nat_2.
+  Rewrite positive_to_nat_4. Inversion H. Rewrite H1. Rewrite <- plus_Snm_nSm. Reflexivity.
+  Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2. Rewrite positive_to_nat_4.
+  Inversion H. Rewrite H1. Reflexivity.
+  Reflexivity.
+Qed.
+
 (** Addition on integers *)
 Definition Zplus := [x,y:Z]
   <Z>Cases x of