diff options
Diffstat (limited to 'theories/Numbers/NatInt/NZMul.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZMul.v | 22 |
1 files changed, 18 insertions, 4 deletions
diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v index a87d6ac62..55ec3f30e 100644 --- a/theories/Numbers/NatInt/NZMul.v +++ b/theories/Numbers/NatInt/NZMul.v @@ -10,9 +10,8 @@ Require Import NZAxioms NZBase NZAdd. -Module Type NZMulPropSig - (Import NZ : NZAxiomsSig')(Import NZBase : NZBasePropSig NZ). -Include NZAddPropSig NZ NZBase. +Module Type NZMulProp (Import NZ : NZAxiomsSig')(Import NZBase : NZBaseProp NZ). +Include NZAddProp NZ NZBase. Theorem mul_0_r : forall n, n * 0 == 0. Proof. @@ -65,4 +64,19 @@ Proof. intro n. now nzsimpl. Qed. -End NZMulPropSig. +Theorem mul_shuffle0 : forall n m p, n*m*p == n*p*m. +Proof. +intros n m p. now rewrite <- 2 mul_assoc, (mul_comm m). +Qed. + +Theorem mul_shuffle1 : forall n m p q, (n * m) * (p * q) == (n * p) * (m * q). +Proof. +intros n m p q. now rewrite 2 mul_assoc, (mul_shuffle0 n). +Qed. + +Theorem mul_shuffle2 : forall n m p q, (n * m) * (p * q) == (n * q) * (m * p). +Proof. +intros n m p q. rewrite (mul_comm p). apply mul_shuffle1. +Qed. + +End NZMulProp. |