diff options
Diffstat (limited to 'theories/Numbers/NatInt/NZMul.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZMul.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v index 55ec3f30e..33c50b24e 100644 --- a/theories/Numbers/NatInt/NZMul.v +++ b/theories/Numbers/NatInt/NZMul.v @@ -56,14 +56,16 @@ Qed. Theorem mul_1_l : forall n, 1 * n == n. Proof. -intro n. now nzsimpl. +intro n. now nzsimpl'. Qed. Theorem mul_1_r : forall n, n * 1 == n. Proof. -intro n. now nzsimpl. +intro n. now nzsimpl'. Qed. +Hint Rewrite mul_1_l mul_1_r : nz. + 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). |