Nouveaux lemmes

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

1 files changed, 18 insertions, 1 deletions

diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 30095d2fa..761979db3 100755
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -11,6 +11,7 @@
 Require Export Plus.
 Require Export Minus.
 Require Export Lt.
+Require Export Le.
 
 V7only [Import nat_scope.].
 Open Local Scope nat_scope.
@@ -80,7 +81,6 @@ Intro; Elim mult_sym; Auto with arith.
 Qed.
 Hints Resolve mult_n_1 : arith v62.
 
-
 Lemma mult_le : (m,n,p:nat) (le n p) -> (le (mult m n) (mult m p)).
 Proof.
   NewInduction m. Intros. Simpl. Apply le_n.
@@ -95,6 +95,23 @@ Rewrite mult_sym. Rewrite (mult_sym n).
 Auto with arith.
 Qed.
 
+Lemma le_mult_mult :
+  (m,n,p,q:nat)(le m n)->(le p q)->(le (mult m p) (mult n q)).
+Proof.
+Intros m n p q Hmn Hpq; NewInduction Hmn.
+NewInduction Hpq.
+(* m*p<=m*p *)
+Apply le_n.
+(* m*p<=m*m0 -> m*p<=m*(S m0) *)
+Rewrite <- mult_n_Sm; Apply le_trans with (mult m m0).
+Assumption.
+Apply le_plus_l.
+(* m*p<=m0*q -> m*p<=(S m0)*q *)
+Simpl; Apply le_trans with (mult m0 q).
+Assumption.
+Apply le_plus_r.
+Qed.
+
 Lemma mult_lt : (m,n,p:nat) (lt n p) -> (lt (mult (S m) n) (mult (S m) p)).
 Proof.
   NewInduction m. Intros. Simpl. Rewrite <- plus_n_O. Rewrite <- plus_n_O. Assumption.