ajout des lemmes Zimmerman

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

7 files changed, 376 insertions, 120 deletions

diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 8ef796eef5..72baafe3ac 100755
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -10,6 +10,8 @@
 
 Require Le.
 Require Lt.
+Require Gt.
+Require Decidable.
 
 Theorem zerop : (n:nat){n=O}+{lt O n}.
 Destruct n; Auto with arith.
@@ -52,3 +54,49 @@ Proof.
 Intros; Elim (lt_eq_lt_dec n m); Auto with arith.
 Intros; Absurd (lt m n); Auto with arith.
 Qed.
+
+(* Proofs of decidability *)
+
+Theorem dec_le:(x,y:nat)(decidable (le x y)).
+Intros x y; Unfold decidable ; Elim (le_gt_dec x y); [
+  Auto with arith
+| Intro; Right; Apply gt_not_le; Assumption].
+Save.
+
+Theorem dec_lt:(x,y:nat)(decidable (lt x y)).
+Intros x y; Unfold lt; Apply dec_le.
+Save.
+
+Theorem dec_gt:(x,y:nat)(decidable (gt x y)).
+Intros x y; Unfold gt; Apply dec_lt.
+Save.
+
+Theorem dec_ge:(x,y:nat)(decidable (ge x y)).
+Intros x y; Unfold ge; Apply dec_le.
+Save.
+
+Theorem not_eq : (x,y:nat) ~ x=y -> (lt x y) \/ (lt y x).
+Intros x y H; Elim (lt_eq_lt_dec x y); [
+  Intros H1; Elim H1; [ Auto with arith | Intros H2; Absurd x=y; Assumption]
+| Auto with arith].
+Save.
+
+
+Theorem not_le : (x,y:nat) ~(le x y) -> (gt x y).
+Intros x y H; Elim (le_gt_dec x y);
+  [ Intros H1; Absurd (le x y); Assumption | Trivial with arith ].
+Save.
+
+Theorem not_gt : (x,y:nat) ~(gt x y) -> (le x y).
+Intros x y H; Elim (le_gt_dec x y);
+  [ Trivial with arith | Intros H1; Absurd (gt x y); Assumption].
+Save.
+
+Theorem not_ge : (x,y:nat) ~(ge x y) -> (lt x y).
+Intros x y H; Exact (not_le y x H).
+Save.
+
+Theorem not_lt : (x,y:nat) ~(lt x y) -> (ge x y).
+Intros x y H; Exact (not_gt y x H). 
+Save.
+
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index 29a9780702..afb5a19844 100755
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -94,3 +94,16 @@ Intros n m; Pattern n m; Apply nat_double_ind; Simpl; Auto with arith.
 Intros; Absurd (lt O O); Trivial with arith.
 Qed.
 Hints Immediate lt_O_minus_lt : arith v62.
+
+Theorem pred_of_minus : (x:nat)(pred x)=(minus x (S O)).
+Induction x; Auto with arith.
+Save.
+
+
+Theorem inj_minus_aux: (x,y:nat) ~(le y x) -> (minus x y) = O.
+Intros y x; Pattern y x ; Apply nat_double_ind; [
+  Simpl; Trivial with arith
+| Intros n H; Absurd (le O (S n)); [ Assumption | Apply le_O_n]
+| Simpl; Intros n m H1 H2; Apply H1;
+  Unfold not ; Intros H3; Apply H2; Apply le_n_S; Assumption].
+Save.
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index ff38eef695..e90cec6612 100755
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -10,6 +10,7 @@
 
 Require Export Plus.
 Require Export Minus.
+Require Export Lt.
 
 (**********************************************************)
 (* Multiplication                                         *)
@@ -23,6 +24,12 @@ Elim plus_assoc_l; Elim H; Auto with arith.
 Qed.
 Hints Resolve mult_plus_distr : arith v62.
 
+Lemma mult_plus_distr_r : (n,m,p:nat) (mult n (plus m p))=(plus (mult n m) (mult n p)).
+Proof.
+  Induction n. Trivial.
+  Intros. Simpl. Rewrite (H m p). Apply sym_eq. Apply plus_permute_2_in_4.
+Qed.
+
 Lemma mult_minus_distr : (n,m,p:nat)((mult (minus n m) p)=(minus (mult n p) (mult m p))).
 Proof.
 Intros; Pattern n m; Apply nat_double_ind; Simpl; Intros; Auto with arith.
@@ -65,3 +72,28 @@ Lemma mult_n_1 : (n:nat)(mult n (S O))=n.
 Intro; Elim mult_sym; Auto with arith.
 Save.
 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.
+  Induction m. Intros. Simpl. Apply le_n.
+  Intros. Simpl. Apply le_plus_plus. Assumption.
+  Apply H. Assumption.
+Qed.
+Hints Resolve mult_le : arith.
+
+Lemma mult_lt : (m,n,p:nat) (lt n p) -> (lt (mult (S m) n) (mult (S m) p)).
+Proof.
+  Induction m. Intros. Simpl. Rewrite <- plus_n_O. Rewrite <- plus_n_O. Assumption.
+  Intros. Exact (lt_plus_plus ? ? ? ? H0 (H ? ? H0)).
+Qed.
+
+Hints Resolve mult_lt : arith.
+
+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.
+  Intro H0. Cut (lt (mult (S m) n) (mult (S m) n)). Intro. Elim (lt_n_n ? H1).
+  Apply le_lt_trans with m:=(mult (S m) p). Assumption.
+  Apply mult_lt. Assumption.
+Qed.
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index 913d6dd371..5ee33d1563 100755
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -6,8 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
+Require Decidable.
 (* $Id$ *)
 
+
 Theorem O_or_S : (n:nat)({m:nat|(S m)=n})+{O=n}.
 Proof.
 Induction n.
@@ -22,3 +24,8 @@ Intros q H'; Elim (H q); Auto.
 Qed.
 
 Hints Resolve O_or_S eq_nat_dec : arith.
+
+Theorem dec_eq_nat:(x,y:nat)(decidable (x=y)).
+Intros x y; Unfold decidable; Elim (eq_nat_dec x y); Auto with arith.
+Save.
+
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 2f96112c38..c070e3645e 100755
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -15,7 +15,7 @@
 Require Le.
 Require Lt.
 
-Lemma plus_sym : (n,m:nat)((plus n m)=(plus m n)).
+Lemma plus_sym : (n,m:nat)(plus n m)=(plus m n).
 Proof.
 Intros n m ; Elim n ; Simpl ; Auto with arith.
 Intros y H ; Elim (plus_n_Sm m y) ; Auto with arith.
@@ -118,3 +118,45 @@ Proof.
 Intros; Apply lt_le_trans with m; Auto with arith.
 Qed.
 Hints Immediate lt_plus_trans : arith v62.
+
+Lemma le_lt_plus_plus : (n,m,p,q:nat) (le n m)->(lt p q)->(lt (plus n p) (plus m q)).
+Proof.
+  Unfold lt. Intros. Change (le (plus (S n) p) (plus m q)). Rewrite plus_Snm_nSm.
+  Apply le_plus_plus; Assumption.
+Qed.
+
+Lemma lt_le_plus_plus : (n,m,p,q:nat) (lt n m)->(le p q)->(lt (plus n p) (plus m q)).
+Proof.
+  Unfold lt. Intros. Change (le (plus (S n) p) (plus m q)). Apply le_plus_plus; Assumption.
+Qed.
+
+Lemma lt_plus_plus : (n,m,p,q:nat) (lt n m)->(lt p q)->(lt (plus n p) (plus m q)).
+Proof.
+  Intros. Apply lt_le_plus_plus. Assumption.
+  Apply lt_le_weak. Assumption.
+Qed.
+
+
+Lemma plus_is_O : (m,n:nat) (plus m n)=O -> m=O /\ n=O.
+Proof.
+  Destruct m; Auto.
+  Intros. Discriminate H.
+Qed.
+
+Lemma plus_is_one : (m,n:nat) (plus m n)=(S O) -> {m=O /\ n=(S O)}+{m=(S O) /\ n=O}.
+Proof.
+  Destruct m; Auto.
+  Destruct n; Auto.
+  Intros. 
+  Simpl in H. Discriminate H.
+Qed.
+
+Lemma plus_permute_2_in_4 : (a,b,c,d:nat)
+      (plus (plus a b) (plus c d))=(plus (plus a c) (plus b d)).
+Proof.
+  Intros. 
+  Rewrite <- (plus_assoc_l a b (plus c d)). Rewrite (plus_assoc_l b c d).
+  Rewrite (plus_sym b c). Rewrite <- (plus_assoc_l c b d). Apply plus_assoc_l.
+Qed.
+
+
diff --git a/theories/Zarith/auxiliary.v b/theories/Zarith/auxiliary.v
index be642fa676..9a827f104e 100644
--- a/theories/Zarith/auxiliary.v
+++ b/theories/Zarith/auxiliary.v
@@ -18,6 +18,7 @@
 Require Export Arith.
 Require fast_integer.
 Require zarith_aux.
+Require Decidable.
 Require Peano_dec.
 Require Export Compare_dec.
 
@@ -27,10 +28,6 @@ Theorem add_un_Zs : (x:positive) (POS (add_un x)) = (Zs (POS x)).
 Intro; Rewrite -> ZL12; Unfold Zs; Simpl; Trivial with arith.
 Save.
 
-Theorem pred_of_minus : (x:nat)(pred x)=(minus x (S O)).
-Induction x; Auto with arith.
-Save.
-
 Theorem inj_S : (y:nat) (inject_nat (S y)) = (Zs (inject_nat y)).
 Induction y; [
   Unfold Zs ; Simpl; Trivial with arith
@@ -75,6 +72,7 @@ Case x; Case y; Intros; [
 | Discriminate H0
 | Simpl in H0; Injection H0; Do 2 Rewrite <- bij1; Intros E; Rewrite E; Auto with arith].
 Save. 
+
 Theorem inj_le:
   (x,y:nat) (le x y) -> (Zle (inject_nat x) (inject_nat y)).
 
@@ -110,6 +108,7 @@ Intros x; Exists (inject_nat x); Split; [
 | Rewrite Zmult_sym; Rewrite Zmult_one; Rewrite Zero_right; 
   Unfold Zle ; Elim x; Intros;Simpl; Discriminate ].
 Save.
+
 Theorem inj_minus1 :
   (x,y:nat) (le y x) -> 
     (inject_nat (minus x y)) = (Zminus (inject_nat x) (inject_nat y)).
@@ -118,36 +117,10 @@ Rewrite Zplus_permute; Rewrite Zplus_inverse_r; Rewrite <- inj_plus;
 Rewrite <- (le_plus_minus y x H);Rewrite Zero_right; Trivial with arith.
 Save.
  
-Theorem inj_minus_aux: (x,y:nat) ~(le y x) -> (minus x y) = O.
-Intros y x; Pattern y x ; Apply nat_double_ind; [
-  Simpl; Trivial with arith
-| Intros n H; Absurd (le O (S n)); [ Assumption | Apply le_O_n]
-| Simpl; Intros n m H1 H2; Apply H1;
-  Unfold not ; Intros H3; Apply H2; Apply le_n_S; Assumption].
-Save.
-
 Theorem inj_minus2: (x,y:nat) (gt y x) -> (inject_nat (minus x y)) = ZERO.
 Intros x y H; Rewrite inj_minus_aux; [ Trivial with arith | Apply gt_not_le; Assumption].
 Save.
 
-Definition decidable := [P:Prop] P \/ ~P.
-
-Theorem dec_not_not : (P:Prop)(decidable P) -> (~P -> False) -> P.
-Unfold decidable; Tauto. Save.
-
-Theorem dec_True: (decidable True).
-Unfold decidable; Auto with arith. Save.
-Theorem dec_False: (decidable False).
-Unfold decidable not; Auto with arith. Save.
-Theorem dec_or: (A,B:Prop)(decidable A) -> (decidable B) -> (decidable (A\/B)).
-Unfold decidable; Tauto. Save.
-Theorem dec_and: (A,B:Prop)(decidable A) -> (decidable B) ->(decidable (A/\B)).
-Unfold decidable; Tauto. Save.
-Theorem dec_not: (A:Prop)(decidable A) -> (decidable ~A).
-Unfold decidable; Tauto. Save.
-Theorem dec_imp: (A,B:Prop)(decidable A) -> (decidable B) ->(decidable (A->B)).
-Unfold decidable; Tauto. Save.
-
 Theorem dec_eq: (x,y:Z) (decidable (x=y)).
 Intros x y; Unfold decidable ; Elim (Zcompare_EGAL x y);
 Intros H1 H2; Elim (Dcompare (Zcompare x y)); [
@@ -192,41 +165,6 @@ Theorem dec_eq_nat:(x,y:nat)(decidable (x=y)).
 Intros x y; Unfold decidable; Elim (eq_nat_dec x y); Auto with arith.
 Save.
 
-Theorem dec_le:(x,y:nat)(decidable (le x y)).
-Intros x y; Unfold decidable ; Elim (le_gt_dec x y); [
-  Auto with arith
-| Intro; Right; Apply gt_not_le; Assumption].
-Save.
-
-Theorem dec_lt:(x,y:nat)(decidable (lt x y)).
-Intros x y; Unfold lt; Apply dec_le.
-Save.
-
-Theorem dec_gt:(x,y:nat)(decidable (gt x y)).
-Intros x y; Unfold gt; Apply dec_lt.
-Save.
-
-Theorem dec_ge:(x,y:nat)(decidable (ge x y)).
-Intros x y; Unfold ge; Apply dec_le.
-Save.
-
-Theorem not_not : (P:Prop)(decidable P) -> (~(~P)) -> P.
-Unfold decidable; Tauto. Save.
-
-Theorem not_or : (A,B:Prop) ~(A\/B) -> ~A /\ ~B.
-Tauto. Save.
-
-Theorem not_and : (A,B:Prop) (decidable A) -> ~(A/\B) -> ~A \/ ~B.
-Unfold decidable; Tauto. Save.
-
-Theorem not_imp : (A,B:Prop) (decidable A) -> ~(A -> B) -> A /\ ~B.
-Unfold decidable;Tauto.
-Save.
-
-Theorem imp_simp : (A,B:Prop) (decidable A) -> (A -> B) -> ~A \/ B.
-Unfold decidable; Tauto.
-Save.
-
 Theorem not_Zge : (x,y:Z) ~(Zge x y) -> (Zlt x y).
 Unfold Zge Zlt ; Intros x y H; Apply dec_not_not;
   [ Exact (dec_Zlt x y) | Assumption].
@@ -253,41 +191,10 @@ Intros x y; Elim (Dcompare (Zcompare x y)); [
     [Auto with arith | Right; Elim (Zcompare_ANTISYM x y); Auto with arith]].
 Save. 
 
-Theorem not_le : (x,y:nat) ~(le x y) -> (gt x y).
-Intros x y H; Elim (le_gt_dec x y);
-  [ Intros H1; Absurd (le x y); Assumption | Trivial with arith ].
-Save.
-
-Theorem not_ge : (x,y:nat) ~(ge x y) -> (lt x y).
-Intros x y H; Exact (not_le y x H).
-Save.
-
-Theorem not_gt : (x,y:nat) ~(gt x y) -> (le x y).
-Intros x y H; Elim (le_gt_dec x y);
-  [ Trivial with arith | Intros H1; Absurd (gt x y); Assumption].
-Save.
-
-Theorem not_lt : (x,y:nat) ~(lt x y) -> (ge x y).
-Intros x y H; Exact (not_gt y x H). 
-Save.
-
-Theorem not_eq : (x,y:nat) ~ x=y -> (lt x y) \/ (lt y x).
-Intros x y H; Elim (lt_eq_lt_dec x y); [
-  Intros H1; Elim H1; [ Auto with arith | Intros H2; Absurd x=y; Assumption]
-| Auto with arith].
-Save.
-
-Theorem eq_ind_r : (A:Set)(x:A)(P:A->Prop)(P x)->(y:A)y=x -> (P y).
-Intros A x P H y H0; Elim (sym_eq A y x H0); Assumption.
-Save.
-
-Theorem eqT_ind_r : (A:Type)(x:A)(P:A->Prop)(P x)->(y:A)y==x -> (P y).
-Intros A x P H y H0; Elim (sym_eqT A y x H0); Assumption.
-Save.
 Lemma new_var: (x:Z) (EX y:Z |(x=y)).
-
 Intros x; Exists x; Trivial with arith. 
 Save.
+
 Theorem Zne_left : (x,y:Z) (Zne x y) -> (Zne (Zplus x (Zopp y)) ZERO).
 Intros x y; Unfold Zne; Unfold not; Intros H1 H2; Apply H1;
 Apply Zsimpl_plus_l with (Zopp y); Rewrite Zplus_inverse_l; Rewrite Zplus_sym;
@@ -295,13 +202,27 @@ Trivial with arith.
 Save.
 
 Theorem Zegal_left : (x,y:Z) (x=y) -> (Zplus x (Zopp y)) = ZERO.
-Intros x y H;Apply (Zsimpl_plus_l y);Rewrite -> Zplus_permute;
+Intros x y H;
+Apply (Zsimpl_plus_l y);Rewrite -> Zplus_permute;
 Rewrite -> Zplus_inverse_r;Do 2 Rewrite -> Zero_right;Assumption.
 Save.
 
 Theorem Zle_left : (x,y:Z) (Zle x y) -> (Zle ZERO (Zplus y (Zopp x))).
-Intros x y H; Apply (Zsimpl_le_plus_l x); Rewrite Zplus_permute;
-Rewrite Zplus_inverse_r; Do 2 Rewrite Zero_right; Assumption.
+Intros x y H; Replace ZERO with (Zplus x (Zopp x)).
+Apply Zle_reg_r; Trivial.
+Apply Zplus_inverse_r.
+Save.
+
+Theorem Zle_left_rev : (x,y:Z) (Zle ZERO (Zplus y (Zopp x))) 
+	-> (Zle x y).
+Intros x y H; Apply (Zsimpl_le_plus_r (Zopp x)).
+Rewrite Zplus_inverse_r; Trivial.
+Save.
+
+Theorem Zlt_left_rev : (x,y:Z) (Zlt ZERO (Zplus y (Zopp x))) 
+	-> (Zlt x y).
+Intros x y H; Apply Zsimpl_lt_plus_r with (Zopp x).
+Rewrite Zplus_inverse_r; Trivial.
 Save.
 
 Theorem Zlt_left :
@@ -311,6 +232,13 @@ Change (Zle (Zs x) (Zs (Zpred y))); Rewrite <- Zs_pred; Apply Zlt_le_S;
 Assumption.
 Save.
 
+Theorem Zlt_left_lt :
+  (x,y:Z) (Zlt x y) -> (Zlt ZERO (Zplus y (Zopp x))).
+Intros x y H; Replace ZERO with (Zplus x (Zopp x)).
+Apply Zlt_reg_r; Trivial.
+Apply Zplus_inverse_r.
+Save.
+
 Theorem Zge_left : (x,y:Z) (Zge x y) -> (Zle ZERO (Zplus x (Zopp y))).
 Intros x y H; Apply Zle_left; Apply Zge_le; Assumption.
 Save.
@@ -319,6 +247,20 @@ Theorem Zgt_left :
   (x,y:Z) (Zgt x y) -> (Zle ZERO (Zplus (Zplus x (NEG xH)) (Zopp y))).
 Intros x y H; Apply Zlt_left; Apply Zgt_lt; Assumption.
 Save.
+
+Theorem Zgt_left_gt :
+  (x,y:Z) (Zgt x y) -> (Zgt (Zplus x (Zopp y)) ZERO).
+Intros x y H; Replace ZERO with (Zplus y (Zopp y)).
+Apply Zgt_reg_r; Trivial.
+Apply Zplus_inverse_r.
+Save.
+
+Theorem Zgt_left_rev : (x,y:Z) (Zgt (Zplus x (Zopp y)) ZERO) 
+	-> (Zgt x y).
+Intros x y H; Apply Zsimpl_gt_plus_r with (Zopp y).
+Rewrite Zplus_inverse_r; Trivial.
+Save.
+
 Theorem Zopp_one : (x:Z)(Zopp x)=(Zmult x (NEG xH)).
 Induction x; Intros; Rewrite Zmult_sym; Auto with arith.
 Save.
@@ -331,6 +273,10 @@ Theorem Zmult_Zopp_left :  (x,y:Z)(Zmult (Zopp x) y) = (Zmult x (Zopp y)).
 Intros; Rewrite Zopp_Zmult; Rewrite Zopp_Zmult_r; Trivial with arith.
 Save.
 
+Theorem Zopp_Zmult_l : (x,y:Z)(Zopp (Zmult x y)) = (Zmult (Zopp x) y).
+Intros x y; Symmetry; Apply Zopp_Zmult.
+Save.
+
 Theorem Zred_factor0 : (x:Z) x = (Zmult x (POS xH)).
 Intro x; Rewrite (Zmult_n_1 x); Trivial with arith.
 Save.
@@ -439,6 +385,7 @@ Theorem Z_eq_mult:
   (x,y:Z)  y = ZERO -> (Zmult y x) = ZERO.
 Intros x y H; Rewrite H; Auto with arith.
 Save.
+
 Theorem Zmult_le:
   (x,y:Z) (Zgt x ZERO) -> (Zle ZERO (Zmult y x)) -> (Zle ZERO y).
 
@@ -450,18 +397,33 @@ Intros x y; Case x; [
 | Intros p; Unfold Zgt ; Simpl; Intros H; Discriminate H].
 Save.
 
+Theorem Zle_ZERO_mult : 
+	 (x,y:Z) (Zle ZERO x) -> (Zle ZERO y) -> (Zle ZERO (Zmult x y)).
+Intros x y; Case x.
+Intros; Rewrite Zero_mult_left; Trivial.
+Intros p H1; Unfold Zle.
+  Pattern 2 ZERO ; Rewrite <- (Zero_mult_right (POS p)).
+  Rewrite  Zcompare_Zmult_compatible; Trivial.
+Intros p H1 H2; Absurd (Zgt ZERO (NEG p)); Trivial.
+Unfold Zgt; Simpl; Auto with zarith.
+Save.
+
+Lemma Zgt_ZERO_mult: (a,b:Z) (Zgt a ZERO)->(Zgt b ZERO)
+	->(Zgt (Zmult a b) ZERO).
+Intros x y; Case x.
+Intros H; Discriminate H.
+Intros p H1; Unfold Zgt; 
+Pattern 2 ZERO ; Rewrite <- (Zero_mult_right (POS p)).
+  Rewrite  Zcompare_Zmult_compatible; Trivial.
+Intros p H; Discriminate H.
+Save.
+
 Theorem Zle_mult:
   (x,y:Z) (Zgt x ZERO) -> (Zle ZERO y) -> (Zle ZERO (Zmult y x)).
-
-Intros x y; Case x; [
-  Simpl; Unfold Zgt ; Simpl; Intros H; Discriminate H
-| Intros p H1; Unfold Zle; Rewrite -> Zmult_sym;
-  Pattern 2 ZERO ; Rewrite <- (Zero_mult_right (POS p));
-  Rewrite  Zcompare_Zmult_compatible; Auto with arith
-| Intros p; Unfold Zgt ; Simpl; Intros H; Discriminate H].
+Intros x y H1 H2; Apply Zle_ZERO_mult; Trivial.
+Apply Zlt_le_weak; Apply Zgt_lt; Trivial.
 Save.
- 
- 
+
 Theorem Zmult_lt:
   (x,y:Z) (Zgt x ZERO) -> (Zlt ZERO (Zmult y x)) -> (Zlt ZERO y).
 
@@ -473,6 +435,17 @@ Intros x y; Case x; [
 | Intros p; Unfold Zgt ; Simpl; Intros H; Discriminate H].
 Save.
 
+Theorem Zmult_gt:
+  (x,y:Z) (Zgt x ZERO) -> (Zgt (Zmult x y) ZERO) -> (Zgt y ZERO).
+
+Intros x y; Case x.
+ Intros H; Discriminate H.
+ Intros p H1; Unfold Zgt.
+ Pattern 1 ZERO ; Rewrite <- (Zero_mult_right (POS p)).
+ Rewrite  Zcompare_Zmult_compatible; Trivial.
+Intros p H; Discriminate H.
+Save.
+
 Theorem Zle_mult_approx:
   (x,y,z:Z) (Zgt x ZERO) -> (Zgt z ZERO) -> (Zle ZERO y) -> 
     (Zle ZERO (Zplus (Zmult y x) z)).
@@ -481,9 +454,91 @@ Intros x y z H1 H2 H3; Apply Zle_trans with m:=(Zmult y x) ; [
   Apply Zle_mult; Assumption
 | Pattern 1 (Zmult y x) ; Rewrite <- Zero_right; Apply Zle_reg_l;
   Apply Zlt_le_weak; Apply Zgt_lt; Assumption].
-
 Save.
 
+Lemma Zle_Zmult_pos_right : 
+	(a,b,c : Z) 
+	(Zle a b) -> (Zle ZERO c) -> (Zle (Zmult a c) (Zmult b c)).
+Intros a b c H1 H2; Apply Zle_left_rev.
+Rewrite Zopp_Zmult_l.
+Rewrite <- Zmult_plus_distr_l.
+Apply Zle_ZERO_mult; Trivial.
+Apply Zle_left; Trivial.
+Save.
+
+Lemma Zle_Zmult_pos_left : 
+	(a,b,c : Z) 
+	(Zle a b) -> (Zle ZERO c) -> (Zle (Zmult c a) (Zmult c b)).
+Intros a b c H1 H2; Rewrite (Zmult_sym c a);Rewrite (Zmult_sym c b).
+Apply  Zle_Zmult_pos_right; Trivial.
+Save.
+
+Lemma Zge_Zmult_pos_right : 
+	(a,b,c : Z) 
+	(Zge a b) -> (Zge c ZERO) -> (Zge (Zmult a c) (Zmult b c)).
+Intros a b c H1 H2; Apply Zle_ge.
+Apply Zle_Zmult_pos_right; Apply Zge_le; Trivial.
+Save.
+
+Lemma Zge_Zmult_pos_left : 
+	(a,b,c : Z) 
+	(Zge a b) -> (Zge c ZERO) -> (Zge (Zmult c a) (Zmult c b)).
+Intros a b c H1 H2; Apply Zle_ge.
+Apply Zle_Zmult_pos_left; Apply Zge_le; Trivial.
+Save.
+
+Lemma Zge_Zmult_pos_compat : 
+	(a,b,c,d : Z) 
+	(Zge a c) -> (Zge b d) -> (Zge c ZERO) -> (Zge d ZERO) 
+	-> (Zge (Zmult a b) (Zmult c d)).
+Intros a b c d H0 H1 H2 H3.
+Apply Zge_trans with (Zmult a d).
+Apply Zge_Zmult_pos_left; Trivial.
+Apply Zge_trans with c; Trivial. 
+Apply Zge_Zmult_pos_right; Trivial.
+Save.
+
+Lemma Zle_mult_simpl 
+ : (a,b,c:Z) (Zgt c ZERO)->(Zle (Zmult a c) (Zmult b c))->(Zle a b).
+Intros a b c H1 H2; Apply Zle_left_rev.
+Apply Zmult_le with c; Trivial.
+Rewrite Zmult_plus_distr_l.
+Rewrite <- Zopp_Zmult_l.
+Apply Zle_left; Trivial.
+Save.
+
+
+Lemma Zge_mult_simpl 
+ : (a,b,c:Z) (Zgt c ZERO)->(Zge (Zmult a c) (Zmult b c))->(Zge a b).
+Intros a b c H1 H2; Apply Zle_ge; Apply Zle_mult_simpl with c; Trivial.
+Apply Zge_le; Trivial.
+Save.
+
+Lemma Zgt_mult_simpl 
+ : (a,b,c:Z) (Zgt c ZERO)->(Zgt (Zmult a c) (Zmult b c))->(Zgt a b).
+Intros a b c H1 H2; Apply Zgt_left_rev.
+Apply Zmult_gt with c; Trivial.
+Rewrite Zmult_sym.
+Rewrite Zmult_plus_distr_l.
+Rewrite <- Zopp_Zmult_l.
+Apply Zgt_left_gt; Trivial.
+Save.
+
+Lemma Zgt_square_simpl: 
+(x, y : Z) (Zge x ZERO) -> (Zge y ZERO) 
+	-> (Zgt (Zmult x x) (Zmult y y)) -> (Zgt x y).
+Intros x y H0 H1 H2.
+Case (dec_Zlt y x).
+Intro; Apply Zlt_gt; Trivial.
+Intros H3; Cut (Zge y x).
+Intros H.
+Elim Zgt_not_le with 1 := H2.
+Apply Zge_le.
+Apply Zge_Zmult_pos_compat; Auto.
+Apply not_Zlt; Trivial.
+Qed.
+
+
 Theorem Zmult_le_approx:
   (x,y,z:Z) (Zgt x ZERO) -> (Zgt x z) -> 
     (Zle ZERO (Zplus (Zmult y x) z)) -> (Zle ZERO y).
diff --git a/theories/Zarith/zarith_aux.v b/theories/Zarith/zarith_aux.v
index a9c0c99760..856082b926 100644
--- a/theories/Zarith/zarith_aux.v
+++ b/theories/Zarith/zarith_aux.v
@@ -144,7 +144,8 @@ Unfold Zle Zgt ;Intros n p H; (ElimCompare 'n 'p); [
 | Intros H1;Absurd (Zcompare n p)=SUPERIEUR;Assumption ].
 Save.
 
-Lemma Zgt_pred       : (n,p:Z)(Zgt p (Zs n))->(Zgt (Zpred p) n).
+Lemma Zgt_pred       
+	: (n,p:Z)(Zgt p (Zs n))->(Zgt (Zpred p) n).
 
 Unfold Zgt Zs Zpred ;Intros n p H; 
 Rewrite <- [x,y:Z](Zcompare_Zplus_compatible x y (POS xH));
@@ -152,17 +153,32 @@ Rewrite (Zplus_sym p); Rewrite Zplus_assoc; Rewrite [x:Z](Zplus_sym x n);
 Simpl; Assumption.
 Save.
 
-Lemma Zsimpl_gt_plus_l : (n,m,p:Z)(Zgt (Zplus p n) (Zplus p m))->(Zgt n m).
+Lemma Zsimpl_gt_plus_l 
+	: (n,m,p:Z)(Zgt (Zplus p n) (Zplus p m))->(Zgt n m).
+
+Unfold Zgt; Intros n m p H; 
+	Rewrite <- (Zcompare_Zplus_compatible n m p); Assumption.
+Save.
+
+Lemma Zsimpl_gt_plus_r
+	: (n,m,p:Z)(Zgt (Zplus n p) (Zplus m p))->(Zgt n m).
+
+Intros n m p H; Apply Zsimpl_gt_plus_l with p.
+Rewrite (Zplus_sym p n); Rewrite (Zplus_sym p m); Trivial.
 
-Unfold Zgt; Intros n m p H; Rewrite <- (Zcompare_Zplus_compatible n m p); 
-Assumption.
 Save.
 
-Lemma Zgt_reg_l      : (n,m,p:Z)(Zgt n m)->(Zgt (Zplus p n) (Zplus p m)).
+Lemma Zgt_reg_l      
+	: (n,m,p:Z)(Zgt n m)->(Zgt (Zplus p n) (Zplus p m)).
 
 Unfold Zgt; Intros n m p H; Rewrite (Zcompare_Zplus_compatible n m p); 
 Assumption.
 Save.
+
+Lemma Zgt_reg_r : (n,m,p:Z)(Zgt n m)->(Zgt (Zplus n p) (Zplus m p)).
+Intros n m p H; Rewrite (Zplus_sym n p); Rewrite (Zplus_sym m p); Apply Zgt_reg_l; Trivial.
+Save.
+
 Theorem Zcompare_et_un: 
   (x,y:Z) (Zcompare x y)=SUPERIEUR <-> 
     ~(Zcompare x (Zplus y (POS xH)))=INFERIEUR.
@@ -243,7 +259,6 @@ Rewrite Zplus_sym; Auto with arith.
 Save.
 
 Theorem Zeq_add_S : (n,m:Z) (Zs n)=(Zs m) -> n=m.
-
 Intros n m H.
 Change (Zplus (Zplus (NEG xH) (POS xH)) n)=
        (Zplus (Zplus (NEG xH) (POS xH)) m);
@@ -379,6 +394,12 @@ Intros m n; Change ~(Zgt m n)-> ~(Zlt n m);
 Unfold not; Intros H1 H2; Apply H1; Apply Zlt_gt; Assumption.
 Save.
 
+Theorem Zge_trans : (n, m, p : Z) (Zge n m) -> (Zge m p) -> (Zge n p).
+Intros n m p H1 H2.
+Apply Zle_ge.
+Apply Zle_trans with m; Apply Zge_le; Trivial.
+Save.
+
 Theorem Zlt_n_Sn : (n:Z)(Zlt n (Zs n)).
 Intro n; Apply Zgt_lt; Apply Zgt_Sn_n.
 Save.
@@ -543,6 +564,12 @@ Intros p n m; Unfold Zle not ;Intros H1 H2;Apply H1;
 Rewrite (Zcompare_Zplus_compatible n m p); Assumption.
 Save.
  
+Lemma Zsimpl_le_plus_r : (p,n,m:Z)(Zle (Zplus n p) (Zplus m p))->(Zle n m).
+
+Intros p n m H; Apply Zsimpl_le_plus_l with p.
+Rewrite (Zplus_sym p n); Rewrite (Zplus_sym p m); Trivial.
+Save.
+
 Lemma Zle_reg_l : (n,m,p:Z)(Zle n m)->(Zle (Zplus p n) (Zplus p m)).
 
 Intros n m p; Unfold Zle not ;Intros H1 H2;Apply H1; 
@@ -567,17 +594,46 @@ Unfold Zs ;Intros n m; Rewrite <- Zplus_assoc; Rewrite (Zplus_sym (POS xH));
 Trivial with arith.
 Save.
 
-Lemma Zsimpl_lt_plus_l : (n,m,p:Z)(Zlt (Zplus p n) (Zplus p m))->(Zlt n m).
+Lemma Zsimpl_lt_plus_l 
+	: (n,m,p:Z)(Zlt (Zplus p n) (Zplus p m))->(Zlt n m).
 
-Unfold Zlt ;Intros n m p; Rewrite Zcompare_Zplus_compatible;Trivial with arith.
+Unfold Zlt ;Intros n m p; 
+	Rewrite Zcompare_Zplus_compatible;Trivial with arith.
 Save.
  
+Lemma Zsimpl_lt_plus_r
+	: (n,m,p:Z)(Zlt (Zplus n p) (Zplus m p))->(Zlt n m).
 
+Intros n m p H; Apply Zsimpl_lt_plus_l with p.
+Rewrite (Zplus_sym p n); Rewrite (Zplus_sym p m); Trivial.
+Save.
+ 
 Lemma Zlt_reg_l : (n,m,p:Z)(Zlt n m)->(Zlt (Zplus p n) (Zplus p m)).
-
 Unfold Zlt ;Intros n m p; Rewrite Zcompare_Zplus_compatible;Trivial with arith.
 Save.
 
+Lemma Zlt_reg_r : (n,m,p:Z)(Zlt n m)->(Zlt (Zplus n p) (Zplus m p)).
+Intros n m p H; Rewrite (Zplus_sym n p); Rewrite (Zplus_sym m p); Apply Zlt_reg_l; Trivial.
+Save.
+
+Lemma Zlt_le_reg :
+ (a,b,c,d:Z) (Zlt a b)->(Zle c d)->(Zlt (Zplus a c) (Zplus b d)).
+Intros a b c d H0 H1.
+Apply Zlt_le_trans with (Zplus b c).
+Apply  Zlt_reg_r; Trivial.
+Apply  Zle_reg_l; Trivial.
+Save.
+
+
+Lemma Zle_lt_reg :
+ (a,b,c,d:Z) (Zle a b)->(Zlt c d)->(Zlt (Zplus a c) (Zplus b d)).
+Intros a b c d H0 H1.
+Apply Zle_lt_trans with (Zplus b c).
+Apply  Zle_reg_r; Trivial.
+Apply  Zlt_reg_l; Trivial.
+Save.
+
+
 Definition Zminus := [m,n:Z](Zplus m (Zopp n)).
 
 Lemma Zminus_plus_simpl : 
@@ -673,6 +729,9 @@ Intros n m; Unfold Zs; Rewrite Zmult_plus_distr_l; Rewrite Zmult_1_n;
 Trivial with arith.
 Save.
 
+
+
+
 (* 
   Just for compatibility with previous versions 
   Use [Zmult_plus_distr_r] and [Zmult_plus_distr_l] rather than