Cyclic31: migrate auxiliary lemmas to their legitimate files

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

1 files changed, 14 insertions, 0 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 610afd4d7..1a925cee6 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -222,6 +222,7 @@ Qed.
 
 
 (**********************************************************************)
+
 (** ** Properties of opposite on binary integer numbers *)
 
 Theorem Zopp_neg : forall p:positive, - Zneg p = Zpos p.
@@ -863,6 +864,19 @@ Proof.
 	reflexivity).
 Qed.
 
+(** ** Multiplication and Doubling *)
+
+Lemma Zdouble_mult : forall z, Zdouble z = (Zpos 2) * z.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma Zdouble_plus_one_mult : forall z, 
+  Zdouble_plus_one z = (Zpos 2) * z + (Zpos 1).
+Proof.
+  destruct z; simpl; auto with zarith.
+Qed.
+
 (** ** Multiplication and Opposite *)
 
 Theorem Zopp_mult_distr_l : forall n m:Z, - (n * m) = - n * m.