1 files changed, 9 insertions, 1 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 16e2ff3256..9cf3944683 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -9,7 +9,7 @@
 (*i $Id$ i*)
 
 (***********************************************************)
-(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
+(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
 (***********************************************************)
 
 Require Export BinPos.
@@ -703,6 +703,12 @@ Qed.
 (**********************************************************************)
 (** Properties of multiplication on binary integer numbers *)
 
+Theorem Zpos_mult_morphism : 
+ forall p q:positive, Zpos (p*q) = Zpos p * Zpos q.
+Proof.
+auto.
+Qed.
+
 (** One is neutral for multiplication *)
 
 Theorem Zmult_1_l : forall n:Z, Zpos 1 * n = n.
@@ -935,6 +941,8 @@ Proof.
 intros; symmetry  in |- *; apply Zmult_succ_l.
 Qed.
 
+
+
 (** Misc redundant properties *)
 
 Lemma Z_eq_mult : forall n m:Z, m = Z0 -> m * n = Z0.