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

1 files changed, 0 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.