diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-20 17:18:56 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-20 17:18:56 +0000 |
| commit | 580539fce36067d7c6ee89cbcb8707fd29ebc117 (patch) | |
| tree | ac6a0c7d0a42643858e56598b5d0c690e9c88729 /theories/Numbers/Integer | |
| parent | c251e659c18859d0d8522781ff9d95723b253c11 (diff) | |
Some migration of results from BinInt to Numbers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14230 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Integer')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZMul.v | 5 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZMulOrder.v | 4 |
2 files changed, 9 insertions, 0 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v index 618722aa8..36f9c3d52 100644 --- a/theories/Numbers/Integer/Abstract/ZMul.v +++ b/theories/Numbers/Integer/Abstract/ZMul.v @@ -53,6 +53,11 @@ Proof. intros n m; now rewrite mul_opp_l, mul_opp_r, opp_involutive. Qed. +Theorem mul_opp_comm : forall n m, (- n) * m == n * (- m). +Proof. +intros n m. now rewrite mul_opp_l, <- mul_opp_r. +Qed. + Theorem mul_sub_distr_l : forall n m p, n * (m - p) == n * m - n * p. Proof. intros n m p. do 2 rewrite <- add_opp_r. rewrite mul_add_distr_l. diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v index c7795ab90..d0d64faa6 100644 --- a/theories/Numbers/Integer/Abstract/ZMulOrder.v +++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v @@ -208,5 +208,9 @@ apply mul_lt_mono_nonneg. now apply lt_le_incl. assumption. apply le_0_1. assumption. Qed. +(** Alternative name : *) + +Definition mul_eq_1 := eq_mul_1. + End ZMulOrderProp. |