From bd981e0dc87900ad7f180b4c4044fc6858d2b40a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 5 Nov 2003 13:44:21 +0000
Subject: Redondances

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4806 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Arith/Mult.v | 17 ++++++-----------
 1 file changed, 6 insertions(+), 11 deletions(-)

diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 99dc47942b..f56ee2f60e 100755
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -127,6 +127,12 @@ Proof.
 Qed.
 
 Hints Resolve mult_lt : arith.
+V7only [
+Notation lt_mult_left := mult_lt.
+(* Theorem lt_mult_left :
+   (x,y,z:nat) (lt x y) -> (lt (mult (S z) x) (mult (S z) y)).
+*)
+].
 
 Lemma lt_mult_right :
   (m,n,p:nat) (lt m n) -> (lt (0) p) -> (lt (mult m p) (mult n p)).
@@ -137,17 +143,6 @@ Rewrite mult_sym.
 Replace (mult n (S p)) with (mult (S p) n); Auto with arith.
 Qed.
 
-Theorem lt_mult_left :
- (x,y,z:nat) (lt x y) -> (lt (mult (S z) x) (mult (S z) y)).
-Proof.
-Intros x y z H;Elim z; [
-  Simpl; Do 2 Rewrite <- plus_n_O; Assumption
-| Simpl; Intros n H1; Apply lt_trans with m:=(plus y (plus x (mult n x))); [
-    Rewrite (plus_sym x (plus x (mult n x)));
-    Rewrite (plus_sym y (plus x (mult n x))); Apply lt_reg_l; Assumption
-  | Apply lt_reg_l;Assumption ]].
-Qed.
-
 Lemma mult_le_conv_1 : (m,n,p:nat) (le (mult (S m) n) (mult (S m) p)) -> (le n p).
 Proof.
   Intros. Elim (le_or_lt n p). Trivial.
-- 
cgit v1.2.3