aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Arith/Mult.v
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-11-14 13:44:25 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-11-14 13:44:25 +0000
commit9977a49c7c39e5431982105a6879c3cb15179847 (patch)
tree7257a4dea07529cbe0149f0a3b955aad324e5c88 /theories/Arith/Mult.v
parent47c543e0ab368a5ee140fab1a2a48f7c3c47d059 (diff)
Nouveaux lemmes 'canoniques'; compatibilite
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4901 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Arith/Mult.v')
-rwxr-xr-xtheories/Arith/Mult.v24
1 files changed, 20 insertions, 4 deletions
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 7c8f43f82..eb36ffa24 100755
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -18,6 +18,18 @@ Open Local Scope nat_scope.
Implicit Variables Type m,n,p:nat.
+(** Zero property *)
+
+Lemma mult_0_r : (n:nat) (mult n O)=O.
+Proof.
+Intro; Symmetry; Apply mult_n_O.
+Qed.
+
+Lemma mult_0_l : (n:nat) (mult O n)=O.
+Proof.
+Reflexivity.
+Qed.
+
(** Distributivity *)
Lemma mult_plus_distr :
@@ -89,13 +101,17 @@ NewInduction m; Simpl; Auto with arith.
Qed.
Hints Resolve mult_O_le : arith v62.
-Lemma mult_le : (m,n,p:nat) (le n p) -> (le (mult m n) (mult m p)).
+Lemma mult_le_compat_l : (n,m,p:nat) (le n m) -> (le (mult p n) (mult p m)).
Proof.
- Intro m; NewInduction m. Intros. Simpl. Apply le_n.
+ NewInduction p as [|p IHp]. Intros. Simpl. Apply le_n.
Intros. Simpl. Apply le_plus_plus. Assumption.
- Apply IHm. Assumption.
+ Apply IHp. Assumption.
Qed.
-Hints Resolve mult_le : arith.
+Hints Resolve mult_le_compat_l : arith.
+V7only [
+Notation mult_le := [m,n,p:nat](mult_le_compat_l p n m).
+].
+
Lemma le_mult_right : (m,n,p:nat)(le m n)->(le (mult m p) (mult n p)).
Intros m n p H.