Nouveaux lemmes 'canoniques'; compatibilite

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4901 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 42 insertions, 8 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.
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index d44914499..ffa94fcd0 100755
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -18,6 +18,18 @@ Open Local Scope nat_scope.
 
 Implicit Variables Type m,n,p,q:nat.
 
+(** Zero is neutral *)
+
+Lemma plus_0_l : (n:nat) (O+n)=n.
+Proof.
+Reflexivity.
+Qed.
+
+Lemma plus_0_r : (n:nat) (n+O)=n.
+Proof.
+Intro; Symmetry; Apply plus_n_O.
+Qed.
+
 (** Commutativity *)
 
 Lemma plus_sym : (n,m:nat)(n+m)=(m+n).
@@ -56,15 +68,21 @@ Hints Resolve plus_assoc_r : arith v62.
 
 (** Simplification *)
 
-Lemma simpl_plus_l : (n,m,p:nat)((n+m)=(n+p))->(m=p).
+Lemma plus_reg_l : (n,m,p:nat)((p+n)=(p+m))->(n=m).
 Proof.
-NewInduction n ; Simpl ; Auto with arith.
+Intros m p n; NewInduction n ; Simpl ; Auto with arith.
 Qed.
+V7only [
+Notation simpl_plus_l := [n,m,p:nat](plus_reg_l m p n).
+].
 
-Lemma simpl_le_plus_l : (p,n,m:nat) (p+n)<=(p+m) -> n<=m.
+Lemma plus_le_reg_l : (n,m,p:nat) (p+n)<=(p+m) -> n<=m.
 Proof.
-Intro p; NewInduction p; Simpl; Auto with arith.
+NewInduction p; Simpl; Auto with arith.
 Qed.
+V7only [
+Notation simpl_le_plus_l := [p,n,m:nat](plus_le_reg_l n m p).
+].
 
 Lemma simpl_lt_plus_l : (n,m,p:nat) (p+n)<(p+m) -> n<m.
 Proof.