Un gros coup de lifting pour IntMap:

 * le type ad des adresses est maintenant un alias vers 
   le N de NArith, qui lui est isomorphe. 

 * toutes les operations sur ces adresses (p.ex. un xor 
   bit a bit) sont maintenant dans de nouveaux fichiers du 
   repertoire NArith. 
 
 * Intmap utilise maintenant le meme type option que le 
   reste du monde
 
 * etc etc...

Tout ceci ne preserve pas forcement la compatibilite. Les 4 contribs
utilisant Intmap sont adaptees en consequence. Me demander si besoin 
ma moulinette d'adaptation (incomplete). 



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

1 files changed, 22 insertions, 0 deletions

diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 16a832e27..bfa767f57 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -173,3 +173,25 @@ Lemma odd_S2n : forall n, odd n -> {p : nat | n = S (double p)}.
 Proof.
 intros n H. exists (div2 n). auto with arith.
 Qed.
+
+(** Doubling before dividing by two brings back to the initial number. *)
+
+Lemma div2_double : forall n:nat, div2 (2*n) = n.
+Proof.
+ induction n.
+ simpl; auto.
+ simpl.
+ replace (n+S(n+0)) with (S (2*n)).
+ f_equal; auto.
+ simpl; auto with arith.
+Qed.
+
+Lemma div2_double_plus_one : forall n:nat, div2 (S (2*n)) = n.
+Proof.
+ induction n.
+ simpl; auto.
+ simpl.
+ replace (n+S(n+0)) with (S (2*n)).
+ f_equal; auto.
+ simpl; auto with arith.
+Qed.