Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

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

2 files changed, 229 insertions, 359 deletions

diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v
index 480f7594be..e381b1fbeb 100755
--- a/contrib/omega/Omega.v
+++ b/contrib/omega/Omega.v
@@ -19,9 +19,9 @@
 Require Export ZArith_base.
 Require Export OmegaLemmas.
 
-Hints Resolve Zle_n Zplus_sym Zplus_assoc Zmult_sym Zmult_assoc
-  Zero_left Zero_right Zmult_one Zplus_inverse_l Zplus_inverse_r 
-  Zmult_plus_distr_l Zmult_plus_distr_r : zarith.
+Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l
+  Zplus_0_r Zmult_1_l Zplus_opp_l Zplus_opp_r Zmult_plus_distr_l
+  Zmult_plus_distr_r: zarith.
 
 Require Export Zhints.
 
@@ -30,28 +30,28 @@ Require Export Zhints.
 Require Minus.
 *)
 
-Hint eq_nat_Omega : zarith := Extern 10 (eq nat ? ?) Abstract Omega.
-Hint le_Omega : zarith := Extern 10 (le ? ?) Abstract Omega.
-Hint lt_Omega : zarith := Extern 10 (lt ? ?) Abstract Omega.
-Hint ge_Omega : zarith := Extern 10 (ge ? ?) Abstract Omega.
-Hint gt_Omega : zarith := Extern 10 (gt ? ?) Abstract Omega.
-
-Hint not_eq_nat_Omega : zarith := Extern 10 ~(eq nat ? ?) Abstract Omega.
-Hint not_le_Omega : zarith := Extern 10 ~(le ? ?) Abstract Omega.
-Hint not_lt_Omega : zarith := Extern 10 ~(lt ? ?) Abstract Omega.
-Hint not_ge_Omega : zarith := Extern 10 ~(ge ? ?) Abstract Omega.
-Hint not_gt_Omega : zarith := Extern 10 ~(gt ? ?) Abstract Omega.
-
-Hint eq_Z_Omega : zarith := Extern 10 (eq Z ? ?) Abstract Omega.
-Hint Zle_Omega : zarith := Extern 10 (Zle ? ?) Abstract Omega.
-Hint Zlt_Omega : zarith := Extern 10 (Zlt ? ?) Abstract Omega.
-Hint Zge_Omega : zarith := Extern 10 (Zge ? ?) Abstract Omega.
-Hint Zgt_Omega : zarith := Extern 10 (Zgt ? ?) Abstract Omega.
-
-Hint not_eq_nat_Omega : zarith := Extern 10 ~(eq Z ? ?) Abstract Omega.
-Hint not_Zle_Omega : zarith := Extern 10 ~(Zle ? ?) Abstract Omega.
-Hint not_Zlt_Omega : zarith := Extern 10 ~(Zlt ? ?) Abstract Omega.
-Hint not_Zge_Omega : zarith := Extern 10 ~(Zge ? ?) Abstract Omega.
-Hint not_Zgt_Omega : zarith := Extern 10 ~(Zgt ? ?) Abstract Omega.
-
-Hint false_Omega : zarith := Extern 10 False Abstract Omega.
+Hint Extern 10 (_ = _ :>nat) => abstract omega: zarith.
+Hint Extern 10 (_ <= _) => abstract omega: zarith.
+Hint Extern 10 (_ < _) => abstract omega: zarith.
+Hint Extern 10 (_ >= _) => abstract omega: zarith.
+Hint Extern 10 (_ > _) => abstract omega: zarith.
+
+Hint Extern 10 (_ <> _ :>nat) => abstract omega: zarith.
+Hint Extern 10 (~ _ <= _) => abstract omega: zarith.
+Hint Extern 10 (~ _ < _) => abstract omega: zarith.
+Hint Extern 10 (~ _ >= _) => abstract omega: zarith.
+Hint Extern 10 (~ _ > _) => abstract omega: zarith.
+
+Hint Extern 10 (_ = _ :>Z) => abstract omega: zarith.
+Hint Extern 10 (_ <= _)%Z => abstract omega: zarith.
+Hint Extern 10 (_ < _)%Z => abstract omega: zarith.
+Hint Extern 10 (_ >= _)%Z => abstract omega: zarith.
+Hint Extern 10 (_ > _)%Z => abstract omega: zarith.
+
+Hint Extern 10 (_ <> _ :>Z) => abstract omega: zarith.
+Hint Extern 10 (~ (_ <= _)%Z) => abstract omega: zarith.
+Hint Extern 10 (~ (_ < _)%Z) => abstract omega: zarith.
+Hint Extern 10 (~ (_ >= _)%Z) => abstract omega: zarith.
+Hint Extern 10 (~ (_ > _)%Z) => abstract omega: zarith.
+
+Hint Extern 10 False => abstract omega: zarith.
\ No newline at end of file
diff --git a/contrib/omega/OmegaLemmas.v b/contrib/omega/OmegaLemmas.v
index c292240699..61747028e2 100644
--- a/contrib/omega/OmegaLemmas.v
+++ b/contrib/omega/OmegaLemmas.v
@@ -8,392 +8,262 @@
 
 (*i $Id$ i*)
 
-Require ZArith_base.
+Require Import ZArith_base.
 
 (** These are specific variants of theorems dedicated for the Omega tactic *)
 
-Lemma new_var: (x:Z) (EX y:Z |(x=y)).
-Intros x; Exists x; Trivial with arith. 
+Lemma new_var : forall x:Z,  exists y : Z | x = y.
+intros x; exists x; trivial with arith. 
 Qed.
 
-Lemma OMEGA1 : (x,y:Z) (x=y) -> (Zle ZERO x) -> (Zle ZERO y).
-Intros x y H; Rewrite H; Auto with arith.
+Lemma OMEGA1 : forall x y:Z, x = y -> (0 <= x)%Z -> (0 <= y)%Z.
+intros x y H; rewrite H; auto with arith.
 Qed.
 
-Lemma OMEGA2 : (x,y:Z) (Zle ZERO x) -> (Zle ZERO y) -> (Zle ZERO (Zplus x y)).
-Exact Zle_0_plus.
+Lemma OMEGA2 : forall x y:Z, (0 <= x)%Z -> (0 <= y)%Z -> (0 <= x + y)%Z.
+exact Zplus_le_0_compat.
 Qed. 
 
-Lemma OMEGA3 : 
-  (x,y,k:Z)(Zgt k ZERO)-> (x=(Zmult y k)) -> (x=ZERO) -> (y=ZERO).
+Lemma OMEGA3 :
+ forall x y k:Z, (k > 0)%Z -> x = (y * k)%Z -> x = 0%Z -> y = 0%Z.
 
-Intros x y k H1 H2 H3; Apply (Zmult_eq k); [
-  Unfold not ; Intros H4; Absurd (Zgt k ZERO); [
-    Rewrite H4; Unfold Zgt ; Simpl; Discriminate | Assumption]
-  | Rewrite <- H2; Assumption].
+intros x y k H1 H2 H3; apply (Zmult_integral_l k);
+ [ unfold not in |- *; intros H4; absurd (k > 0)%Z;
+    [ rewrite H4; unfold Zgt in |- *; simpl in |- *; discriminate
+    | assumption ]
+ | rewrite <- H2; assumption ].
 Qed.
 
-Lemma OMEGA4 :
-  (x,y,z:Z)(Zgt x ZERO) -> (Zgt y x) -> ~(Zplus (Zmult z y) x) = ZERO.
-
-Unfold not ; Intros x y z H1 H2 H3; Cut (Zgt y ZERO); [
-  Intros H4; Cut (Zle ZERO (Zplus (Zmult z y) x)); [
-    Intros H5; Generalize (Zmult_le_approx y z x H4 H2 H5) ; Intros H6;
-    Absurd (Zgt (Zplus (Zmult z y) x) ZERO); [
-      Rewrite -> H3; Unfold Zgt ; Simpl; Discriminate
-    | Apply Zle_gt_trans with x ; [
-        Pattern 1 x ; Rewrite <- (Zero_left x); Apply Zle_reg_r;
-        Rewrite -> Zmult_sym; Generalize H4 ; Unfold Zgt;
-        Case y; [
-          Simpl; Intros H7; Discriminate H7
-        | Intros p H7; Rewrite <- (Zero_mult_right (POS p));
-          Unfold Zle ; Rewrite -> Zcompare_Zmult_compatible; Exact H6
-        | Simpl; Intros p H7; Discriminate H7]
-      | Assumption]]
-    | Rewrite -> H3; Unfold Zle ; Simpl; Discriminate]
-  | Apply Zgt_trans with x ; [ Assumption | Assumption]].
+Lemma OMEGA4 : forall x y z:Z, (x > 0)%Z -> (y > x)%Z -> (z * y + x)%Z <> 0%Z.
+
+unfold not in |- *; intros x y z H1 H2 H3; cut (y > 0)%Z;
+ [ intros H4; cut (0 <= z * y + x)%Z;
+    [ intros H5; generalize (Zmult_le_approx y z x H4 H2 H5); intros H6;
+       absurd (z * y + x > 0)%Z;
+       [ rewrite H3; unfold Zgt in |- *; simpl in |- *; discriminate
+       | apply Zle_gt_trans with x;
+          [ pattern x at 1 in |- *; rewrite <- (Zplus_0_l x);
+             apply Zplus_le_compat_r; rewrite Zmult_comm; 
+             generalize H4; unfold Zgt in |- *; case y;
+             [ simpl in |- *; intros H7; discriminate H7
+             | intros p H7; rewrite <- (Zmult_0_r (Zpos p));
+                unfold Zle in |- *; rewrite Zcompare_mult_compat; 
+                exact H6
+             | simpl in |- *; intros p H7; discriminate H7 ]
+          | assumption ] ]
+    | rewrite H3; unfold Zle in |- *; simpl in |- *; discriminate ]
+ | apply Zgt_trans with x; [ assumption | assumption ] ].
 Qed.
 
-Lemma OMEGA5: (x,y,z:Z)(x=ZERO) -> (y=ZERO) -> (Zplus x (Zmult y z)) = ZERO.
+Lemma OMEGA5 : forall x y z:Z, x = 0%Z -> y = 0%Z -> (x + y * z)%Z = 0%Z.
 
-Intros x y z H1 H2; Rewrite H1; Rewrite H2; Simpl; Trivial with arith.
+intros x y z H1 H2; rewrite H1; rewrite H2; simpl in |- *; trivial with arith.
 Qed.
 
-Lemma OMEGA6:
-  (x,y,z:Z)(Zle ZERO x) -> (y=ZERO) -> (Zle ZERO (Zplus x (Zmult y z))).
+Lemma OMEGA6 : forall x y z:Z, (0 <= x)%Z -> y = 0%Z -> (0 <= x + y * z)%Z.
 
-Intros x y z H1 H2; Rewrite H2; Simpl; Rewrite Zero_right; Assumption.
+intros x y z H1 H2; rewrite H2; simpl in |- *; rewrite Zplus_0_r; assumption.
 Qed.
 
-Lemma OMEGA7:
-  (x,y,z,t:Z)(Zgt z ZERO) -> (Zgt t ZERO) -> (Zle ZERO x) -> (Zle ZERO y) -> 
-    (Zle ZERO (Zplus (Zmult x z) (Zmult y t))).
+Lemma OMEGA7 :
+ forall x y z t:Z,
+   (z > 0)%Z ->
+   (t > 0)%Z -> (0 <= x)%Z -> (0 <= y)%Z -> (0 <= x * z + y * t)%Z.
 
-Intros x y z t H1 H2 H3 H4; Rewrite <- (Zero_left ZERO);
-Apply Zle_plus_plus; Apply Zle_mult; Assumption.
+intros x y z t H1 H2 H3 H4; rewrite <- (Zplus_0_l 0); apply Zplus_le_compat;
+ apply Zmult_gt_0_le_0_compat; assumption.
 Qed.
 
-Lemma OMEGA8: 
-  (x,y:Z) (Zle ZERO x) -> (Zle ZERO y) -> x = (Zopp y) -> x = ZERO.
+Lemma OMEGA8 :
+ forall x y:Z, (0 <= x)%Z -> (0 <= y)%Z -> x = (- y)%Z -> x = 0%Z.
 
-Intros x y H1 H2 H3; Elim (Zle_lt_or_eq ZERO x H1); [
-  Intros H4; Absurd (Zlt ZERO x); [
-    Change (Zge ZERO x); Apply Zle_ge; Apply Zsimpl_le_plus_l with y;
-    Rewrite -> H3; Rewrite Zplus_inverse_r; Rewrite Zero_right; Assumption
-  | Assumption]
-| Intros H4; Rewrite -> H4; Trivial with arith].
+intros x y H1 H2 H3; elim (Zle_lt_or_eq 0 x H1);
+ [ intros H4; absurd (0 < x)%Z;
+    [ change (0 >= x)%Z in |- *; apply Zle_ge; apply Zplus_le_reg_l with y;
+       rewrite H3; rewrite Zplus_opp_r; rewrite Zplus_0_r; 
+       assumption
+    | assumption ]
+ | intros H4; rewrite H4; trivial with arith ].
 Qed.
 
-Lemma OMEGA9:(x,y,z,t:Z) y=ZERO -> x = z -> 
-  (Zplus y (Zmult (Zplus (Zopp x) z) t)) = ZERO.
+Lemma OMEGA9 :
+ forall x y z t:Z, y = 0%Z -> x = z -> (y + (- x + z) * t)%Z = 0%Z.
 
-Intros x y z t H1 H2; Rewrite H2; Rewrite Zplus_inverse_l; 
-Rewrite Zero_mult_left;  Rewrite Zero_right; Assumption.
+intros x y z t H1 H2; rewrite H2; rewrite Zplus_opp_l; rewrite Zmult_0_l;
+ rewrite Zplus_0_r; assumption.
 Qed.
 
-Lemma OMEGA10:(v,c1,c2,l1,l2,k1,k2:Z)
-  (Zplus (Zmult (Zplus (Zmult v c1) l1) k1) (Zmult (Zplus (Zmult v c2) l2) k2))
-  = (Zplus (Zmult v (Zplus (Zmult c1 k1) (Zmult c2 k2)))
-           (Zplus (Zmult l1 k1) (Zmult l2 k2))).
+Lemma OMEGA10 :
+ forall v c1 c2 l1 l2 k1 k2:Z,
+   ((v * c1 + l1) * k1 + (v * c2 + l2) * k2)%Z =
+   (v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2))%Z.
 
-Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r);
-Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; 
-Rewrite (Zplus_permute (Zmult l1 k1) (Zmult (Zmult v c2) k2)); Trivial with arith.
+intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
+ repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
+ rewrite (Zplus_permute (l1 * k1) (v * c2 * k2)); trivial with arith.
 Qed.
 
-Lemma OMEGA11:(v1,c1,l1,l2,k1:Z)
-  (Zplus (Zmult (Zplus (Zmult v1 c1) l1) k1) l2)
-  = (Zplus (Zmult v1 (Zmult c1 k1)) (Zplus (Zmult l1 k1) l2)).
+Lemma OMEGA11 :
+ forall v1 c1 l1 l2 k1:Z,
+   ((v1 * c1 + l1) * k1 + l2)%Z = (v1 * (c1 * k1) + (l1 * k1 + l2))%Z.
 
-Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r);
-Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; Trivial with arith.
+intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
+ repeat rewrite Zmult_assoc; repeat elim Zplus_assoc; 
+ trivial with arith.
 Qed.
 
-Lemma OMEGA12:(v2,c2,l1,l2,k2:Z)
-  (Zplus l1 (Zmult (Zplus (Zmult v2 c2) l2) k2))
-  = (Zplus (Zmult v2 (Zmult c2 k2)) (Zplus l1 (Zmult l2 k2))).
+Lemma OMEGA12 :
+ forall v2 c2 l1 l2 k2:Z,
+   (l1 + (v2 * c2 + l2) * k2)%Z = (v2 * (c2 * k2) + (l1 + l2 * k2))%Z.
 
-Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r);
-Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; Rewrite Zplus_permute;
-Trivial with arith.
+intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
+ repeat rewrite Zmult_assoc; repeat elim Zplus_assoc; 
+ rewrite Zplus_permute; trivial with arith.
 Qed.
 
-Lemma OMEGA13:(v,l1,l2:Z)(x:positive)
-  (Zplus (Zplus (Zmult v (POS x)) l1) (Zplus (Zmult v (NEG x)) l2))
-  = (Zplus l1 l2).
+Lemma OMEGA13 :
+ forall (v l1 l2:Z) (x:positive),
+   (v * Zpos x + l1 + (v * Zneg x + l2))%Z = (l1 + l2)%Z.
 
-Intros; Rewrite  Zplus_assoc; Rewrite (Zplus_sym (Zmult v (POS x)) l1);
-Rewrite (Zplus_assoc_r l1); Rewrite <- Zmult_plus_distr_r;
-Rewrite <- Zopp_NEG; Rewrite (Zplus_sym (Zopp (NEG x)) (NEG x));
-Rewrite Zplus_inverse_r; Rewrite  Zero_mult_right; Rewrite Zero_right; Trivial with arith.
+intros; rewrite Zplus_assoc; rewrite (Zplus_comm (v * Zpos x) l1);
+ rewrite (Zplus_assoc_reverse l1); rewrite <- Zmult_plus_distr_r;
+ rewrite <- Zopp_neg; rewrite (Zplus_comm (- Zneg x) (Zneg x));
+ rewrite Zplus_opp_r; rewrite Zmult_0_r; rewrite Zplus_0_r;
+ trivial with arith.
 Qed.
  
-Lemma OMEGA14:(v,l1,l2:Z)(x:positive)
-  (Zplus (Zplus (Zmult v (NEG x)) l1) (Zplus (Zmult v (POS x)) l2))
-  = (Zplus l1 l2).
-
-Intros; Rewrite  Zplus_assoc; Rewrite (Zplus_sym (Zmult v (NEG x)) l1);
-Rewrite (Zplus_assoc_r l1); Rewrite <- Zmult_plus_distr_r;
-Rewrite <- Zopp_NEG; Rewrite  Zplus_inverse_r; Rewrite  Zero_mult_right;
-Rewrite Zero_right; Trivial with arith.
+Lemma OMEGA14 :
+ forall (v l1 l2:Z) (x:positive),
+   (v * Zneg x + l1 + (v * Zpos x + l2))%Z = (l1 + l2)%Z.
+
+intros; rewrite Zplus_assoc; rewrite (Zplus_comm (v * Zneg x) l1);
+ rewrite (Zplus_assoc_reverse l1); rewrite <- Zmult_plus_distr_r;
+ rewrite <- Zopp_neg; rewrite Zplus_opp_r; rewrite Zmult_0_r;
+ rewrite Zplus_0_r; trivial with arith.
 Qed.
-Lemma OMEGA15:(v,c1,c2,l1,l2,k2:Z)
-  (Zplus (Zplus (Zmult v c1) l1) (Zmult (Zplus (Zmult v c2) l2) k2))
-  = (Zplus (Zmult v (Zplus c1  (Zmult c2 k2)))
-           (Zplus l1 (Zmult l2 k2))).
-
-Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r);
-Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; 
-Rewrite (Zplus_permute l1 (Zmult (Zmult v c2) k2)); Trivial with arith.
+Lemma OMEGA15 :
+ forall v c1 c2 l1 l2 k2:Z,
+   (v * c1 + l1 + (v * c2 + l2) * k2)%Z =
+   (v * (c1 + c2 * k2) + (l1 + l2 * k2))%Z.
+
+intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
+ repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
+ rewrite (Zplus_permute l1 (v * c2 * k2)); trivial with arith.
 Qed.
 
-Lemma OMEGA16:
-  (v,c,l,k:Z)
-   (Zmult (Zplus (Zmult v c) l) k) = (Zplus (Zmult v (Zmult c k)) (Zmult l k)).
+Lemma OMEGA16 :
+ forall v c l k:Z, ((v * c + l) * k)%Z = (v * (c * k) + l * k)%Z.
 
-Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r);
-Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; Trivial with arith.
+intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
+ repeat rewrite Zmult_assoc; repeat elim Zplus_assoc; 
+ trivial with arith.
 Qed.
 
-Lemma OMEGA17: 
-  (x,y,z:Z)(Zne x ZERO) -> (y=ZERO) -> (Zne (Zplus x (Zmult y z)) ZERO).
+Lemma OMEGA17 : forall x y z:Z, Zne x 0 -> y = 0%Z -> Zne (x + y * z) 0.
 
-Unfold Zne not; Intros x y z H1 H2 H3; Apply H1; 
-Apply Zsimpl_plus_l with (Zmult y z); Rewrite Zplus_sym; Rewrite H3; 
-Rewrite H2; Auto with arith.
+unfold Zne, not in |- *; intros x y z H1 H2 H3; apply H1;
+ apply Zplus_reg_l with (y * z)%Z; rewrite Zplus_comm; 
+ rewrite H3; rewrite H2; auto with arith.
 Qed.
 
-Lemma OMEGA18:
-  (x,y,k:Z) x=(Zmult y k) -> (Zne x ZERO) -> (Zne y ZERO).
+Lemma OMEGA18 : forall x y k:Z, x = (y * k)%Z -> Zne x 0 -> Zne y 0.
 
-Unfold Zne not; Intros x y k H1 H2 H3; Apply H2; Rewrite H1; Rewrite H3; Auto with arith.
+unfold Zne, not in |- *; intros x y k H1 H2 H3; apply H2; rewrite H1;
+ rewrite H3; auto with arith.
 Qed.
 
-Lemma OMEGA19:
-  (x:Z) (Zne x ZERO) -> 
-    (Zle ZERO (Zplus x (NEG xH))) \/ (Zle ZERO (Zplus (Zmult x (NEG xH)) (NEG xH))).
-
-Unfold Zne ; Intros x H; Elim (Zle_or_lt ZERO x); [
-  Intros H1; Elim Zle_lt_or_eq with 1:=H1; [
-    Intros H2; Left;  Change (Zle ZERO (Zpred x)); Apply Zle_S_n;
-    Rewrite <- Zs_pred; Apply Zlt_le_S; Assumption
-  | Intros H2; Absurd x=ZERO; Auto with arith]
-| Intros H1; Right; Rewrite <- Zopp_one; Rewrite Zplus_sym;
-  Apply Zle_left; Apply Zle_S_n; Simpl; Apply Zlt_le_S; Auto with arith].
+Lemma OMEGA19 :
+ forall x:Z, Zne x 0 -> (0 <= x + -1)%Z \/ (0 <= x * -1 + -1)%Z.
+
+unfold Zne in |- *; intros x H; elim (Zle_or_lt 0 x);
+ [ intros H1; elim Zle_lt_or_eq with (1 := H1);
+    [ intros H2; left; change (0 <= Zpred x)%Z in |- *; apply Zsucc_le_reg;
+       rewrite <- Zsucc_pred; apply Zlt_le_succ; assumption
+    | intros H2; absurd (x = 0%Z); auto with arith ]
+ | intros H1; right; rewrite <- Zopp_eq_mult_neg_1; rewrite Zplus_comm;
+    apply Zle_left; apply Zsucc_le_reg; simpl in |- *; 
+    apply Zlt_le_succ; auto with arith ].
 Qed.
 
-Lemma OMEGA20:
-  (x,y,z:Z)(Zne x  ZERO) -> (y=ZERO) -> (Zne (Zplus x (Zmult y z)) ZERO).
+Lemma OMEGA20 : forall x y z:Z, Zne x 0 -> y = 0%Z -> Zne (x + y * z) 0.
 
-Unfold Zne not; Intros x y z H1 H2 H3; Apply H1; Rewrite H2 in H3;
-Simpl in H3; Rewrite Zero_right in H3; Trivial with arith.
+unfold Zne, not in |- *; intros x y z H1 H2 H3; apply H1; rewrite H2 in H3;
+ simpl in H3; rewrite Zplus_0_r in H3; trivial with arith.
 Qed.
 
-Definition fast_Zplus_sym := 
-[x,y:Z][P:Z -> Prop][H: (P (Zplus y x))]
-  (eq_ind_r Z (Zplus y x) P H (Zplus x y) (Zplus_sym x y)).
-
-Definition fast_Zplus_assoc_r :=
-[n,m,p:Z][P:Z -> Prop][H : (P (Zplus n (Zplus m p)))]
- (eq_ind_r Z (Zplus n (Zplus m p)) P H (Zplus (Zplus n m) p) (Zplus_assoc_r n m p)).
-
-Definition fast_Zplus_assoc_l :=
-[n,m,p:Z][P:Z -> Prop][H : (P (Zplus (Zplus n m) p))]
- (eq_ind_r Z (Zplus (Zplus n m) p) P H (Zplus n (Zplus m p)) 
-           (Zplus_assoc_l n m p)).
-
-Definition fast_Zplus_permute :=
-[n,m,p:Z][P:Z -> Prop][H : (P (Zplus m (Zplus n p)))]
- (eq_ind_r Z (Zplus m (Zplus n p)) P H (Zplus n (Zplus m p))
-           (Zplus_permute n m p)).
-
-Definition fast_OMEGA10 := 
-[v,c1,c2,l1,l2,k1,k2:Z][P:Z -> Prop]
-[H : (P (Zplus (Zmult v (Zplus (Zmult c1 k1) (Zmult c2 k2)))
-               (Zplus (Zmult l1 k1) (Zmult l2 k2))))]
- (eq_ind_r Z 
-           (Zplus (Zmult v (Zplus (Zmult c1 k1) (Zmult c2 k2)))
-            (Zplus (Zmult l1 k1) (Zmult l2 k2)))
-           P H 
-          (Zplus (Zmult (Zplus (Zmult v c1) l1) k1)
-                 (Zmult (Zplus (Zmult v c2) l2) k2))
-        (OMEGA10 v c1 c2 l1 l2 k1 k2)).
-
-Definition fast_OMEGA11 := 
-[v1,c1,l1,l2,k1:Z][P:Z -> Prop]
-[H : (P (Zplus (Zmult v1 (Zmult c1 k1)) (Zplus (Zmult l1 k1) l2)))]
- (eq_ind_r Z 
-   (Zplus (Zmult v1 (Zmult c1 k1)) (Zplus (Zmult l1 k1) l2))
-   P H 
-   (Zplus (Zmult (Zplus (Zmult v1 c1) l1) k1) l2)
-   (OMEGA11 v1 c1 l1 l2 k1)).
-Definition fast_OMEGA12 := 
-[v2,c2,l1,l2,k2:Z][P:Z -> Prop]
-[H : (P (Zplus (Zmult v2 (Zmult c2 k2)) (Zplus l1 (Zmult l2 k2))))]
- (eq_ind_r Z 
-   (Zplus (Zmult v2 (Zmult c2 k2)) (Zplus l1 (Zmult l2 k2)))
-   P H 
-   (Zplus l1 (Zmult (Zplus (Zmult v2 c2) l2) k2))
-   (OMEGA12 v2 c2 l1 l2 k2)).
-
-Definition fast_OMEGA15 :=
-[v,c1,c2,l1,l2,k2 :Z][P:Z -> Prop]
-[H : (P (Zplus (Zmult v (Zplus c1 (Zmult c2 k2))) (Zplus l1 (Zmult l2 k2))))]
- (eq_ind_r Z 
-   (Zplus (Zmult v (Zplus c1 (Zmult c2 k2))) (Zplus l1 (Zmult l2 k2)))
-   P H 
-   (Zplus (Zplus (Zmult v c1) l1) (Zmult (Zplus (Zmult v c2) l2) k2))
-   (OMEGA15 v c1 c2 l1 l2 k2)).
-Definition fast_OMEGA16 :=
-[v,c,l,k :Z][P:Z -> Prop]
-[H : (P (Zplus (Zmult v (Zmult c k)) (Zmult l k)))]
- (eq_ind_r Z 
-   (Zplus (Zmult v (Zmult c k)) (Zmult l k))
-   P H 
-   (Zmult (Zplus (Zmult v c) l) k)
-   (OMEGA16 v c l k)).
-
-Definition fast_OMEGA13 :=
-[v,l1,l2 :Z][x:positive][P:Z -> Prop]
-[H : (P (Zplus l1 l2))]
- (eq_ind_r Z 
-   (Zplus l1 l2)
-   P H 
-   (Zplus (Zplus (Zmult v (POS x)) l1) (Zplus (Zmult v (NEG x)) l2))
-   (OMEGA13 v l1 l2 x )).
-
-Definition fast_OMEGA14 :=
-[v,l1,l2 :Z][x:positive][P:Z -> Prop]
-[H : (P (Zplus l1 l2))]
- (eq_ind_r Z 
-   (Zplus l1 l2)
-   P H 
-   (Zplus (Zplus (Zmult v (NEG x)) l1) (Zplus (Zmult v (POS x)) l2))
-   (OMEGA14 v l1 l2 x )).
-Definition fast_Zred_factor0:=
-[x:Z][P:Z -> Prop]
-[H : (P (Zmult x (POS xH)) )]
- (eq_ind_r Z 
-   (Zmult x (POS xH))
-   P H 
-   x
-   (Zred_factor0 x)).
-
-Definition fast_Zopp_one :=
-[x:Z][P:Z -> Prop]
-[H : (P (Zmult x (NEG xH)))]
- (eq_ind_r Z 
-   (Zmult x (NEG xH))
-   P H 
-   (Zopp x)
-   (Zopp_one x)).
-
-Definition fast_Zmult_sym :=
-[x,y :Z][P:Z -> Prop]
-[H : (P (Zmult y x))]
- (eq_ind_r Z 
-(Zmult y x)
-   P H 
-(Zmult x y)
-   (Zmult_sym x y )).
-
-Definition fast_Zopp_Zplus :=
-[x,y :Z][P:Z -> Prop]
-[H : (P (Zplus (Zopp x) (Zopp y)) )]
- (eq_ind_r Z 
-   (Zplus (Zopp x) (Zopp y))
-   P H 
-   (Zopp (Zplus x y))
-   (Zopp_Zplus x y )).
-
-Definition fast_Zopp_Zopp :=
-[x:Z][P:Z -> Prop]
-[H : (P x )] (eq_ind_r Z x P H (Zopp (Zopp x)) (Zopp_Zopp x)).
-
-Definition fast_Zopp_Zmult_r :=
-[x,y:Z][P:Z -> Prop]
-[H : (P (Zmult x (Zopp y)))]
- (eq_ind_r Z 
-   (Zmult x (Zopp y))
-   P H 
-   (Zopp (Zmult x y))
-   (Zopp_Zmult_r x y )).
-
-Definition fast_Zmult_plus_distr :=
-[n,m,p:Z][P:Z -> Prop]
-[H : (P (Zplus (Zmult n p) (Zmult m p)))]
- (eq_ind_r Z 
-   (Zplus (Zmult n p) (Zmult m p))
-   P H 
-   (Zmult (Zplus n m) p)
-   (Zmult_plus_distr_l n m p)).
-Definition fast_Zmult_Zopp_left:=
-[x,y:Z][P:Z -> Prop]
-[H : (P (Zmult x (Zopp y)))]
- (eq_ind_r Z 
-   (Zmult x (Zopp y))
-   P H 
-   (Zmult (Zopp x) y)
-   (Zmult_Zopp_left x y)).
-
-Definition fast_Zmult_assoc_r :=
-[n,m,p :Z][P:Z -> Prop]
-[H : (P (Zmult n (Zmult m p)))]
- (eq_ind_r Z 
-   (Zmult n (Zmult m p))
-   P H 
-   (Zmult (Zmult n m) p)
-   (Zmult_assoc_r n m p)).
-
-Definition fast_Zred_factor1 :=
-[x:Z][P:Z -> Prop]
-[H : (P (Zmult x (POS (xO xH))) )]
- (eq_ind_r Z 
-   (Zmult x (POS (xO xH)))
-   P H 
-   (Zplus x x)
-   (Zred_factor1 x)).
-
-Definition fast_Zred_factor2 :=
-[x,y:Z][P:Z -> Prop]
-[H : (P (Zmult x (Zplus (POS xH) y)))]
- (eq_ind_r Z 
-   (Zmult x (Zplus (POS xH) y))
-   P H 
-   (Zplus x (Zmult x y))
-   (Zred_factor2 x y)).
-Definition fast_Zred_factor3 :=
-[x,y:Z][P:Z -> Prop]
-[H : (P (Zmult x (Zplus (POS xH) y)))]
- (eq_ind_r Z 
-   (Zmult x (Zplus (POS xH) y))
-   P H 
-   (Zplus (Zmult x y) x)
-   (Zred_factor3 x y)).
-
-Definition fast_Zred_factor4 :=
-[x,y,z:Z][P:Z -> Prop]
-[H : (P (Zmult x (Zplus y z)))]
- (eq_ind_r Z 
-   (Zmult x (Zplus y z))
-   P H 
-   (Zplus (Zmult x y) (Zmult x z))
-   (Zred_factor4 x y z)).
-
-Definition fast_Zred_factor5 :=
-[x,y:Z][P:Z -> Prop]
-[H : (P y)]
- (eq_ind_r Z 
-   y
-   P H 
-   (Zplus (Zmult x ZERO) y)
-   (Zred_factor5 x y)).
-
-Definition fast_Zred_factor6 :=
-[x :Z][P:Z -> Prop]
-[H : (P(Zplus x ZERO) )]
- (eq_ind_r Z 
-   (Zplus x ZERO)
-   P H 
-   x
-   (Zred_factor6 x )).
+Definition fast_Zplus_sym (x y:Z) (P:Z -> Prop) (H:P (y + x)%Z) :=
+  eq_ind_r P H (Zplus_comm x y).
+
+Definition fast_Zplus_assoc_r (n m p:Z) (P:Z -> Prop)
+  (H:P (n + (m + p))%Z) := eq_ind_r P H (Zplus_assoc_reverse n m p).
+
+Definition fast_Zplus_assoc_l (n m p:Z) (P:Z -> Prop) 
+  (H:P (n + m + p)%Z) := eq_ind_r P H (Zplus_assoc n m p).
+
+Definition fast_Zplus_permute (n m p:Z) (P:Z -> Prop)
+  (H:P (m + (n + p))%Z) := eq_ind_r P H (Zplus_permute n m p).
+
+Definition fast_OMEGA10 (v c1 c2 l1 l2 k1 k2:Z) (P:Z -> Prop)
+  (H:P (v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2))%Z) :=
+  eq_ind_r P H (OMEGA10 v c1 c2 l1 l2 k1 k2).
+
+Definition fast_OMEGA11 (v1 c1 l1 l2 k1:Z) (P:Z -> Prop)
+  (H:P (v1 * (c1 * k1) + (l1 * k1 + l2))%Z) :=
+  eq_ind_r P H (OMEGA11 v1 c1 l1 l2 k1).
+Definition fast_OMEGA12 (v2 c2 l1 l2 k2:Z) (P:Z -> Prop)
+  (H:P (v2 * (c2 * k2) + (l1 + l2 * k2))%Z) :=
+  eq_ind_r P H (OMEGA12 v2 c2 l1 l2 k2).
+
+Definition fast_OMEGA15 (v c1 c2 l1 l2 k2:Z) (P:Z -> Prop)
+  (H:P (v * (c1 + c2 * k2) + (l1 + l2 * k2))%Z) :=
+  eq_ind_r P H (OMEGA15 v c1 c2 l1 l2 k2).
+Definition fast_OMEGA16 (v c l k:Z) (P:Z -> Prop)
+  (H:P (v * (c * k) + l * k)%Z) := eq_ind_r P H (OMEGA16 v c l k).
+
+Definition fast_OMEGA13 (v l1 l2:Z) (x:positive) (P:Z -> Prop)
+  (H:P (l1 + l2)%Z) := eq_ind_r P H (OMEGA13 v l1 l2 x).
+
+Definition fast_OMEGA14 (v l1 l2:Z) (x:positive) (P:Z -> Prop)
+  (H:P (l1 + l2)%Z) := eq_ind_r P H (OMEGA14 v l1 l2 x).
+Definition fast_Zred_factor0 (x:Z) (P:Z -> Prop) (H:P (x * 1)%Z) :=
+  eq_ind_r P H (Zred_factor0 x).
+
+Definition fast_Zopp_one (x:Z) (P:Z -> Prop) (H:P (x * -1)%Z) :=
+  eq_ind_r P H (Zopp_eq_mult_neg_1 x).
+
+Definition fast_Zmult_sym (x y:Z) (P:Z -> Prop) (H:P (y * x)%Z) :=
+  eq_ind_r P H (Zmult_comm x y).
+
+Definition fast_Zopp_Zplus (x y:Z) (P:Z -> Prop) (H:P (- x + - y)%Z) :=
+  eq_ind_r P H (Zopp_plus_distr x y).
+
+Definition fast_Zopp_Zopp (x:Z) (P:Z -> Prop) (H:P x) :=
+  eq_ind_r P H (Zopp_involutive x).
+
+Definition fast_Zopp_Zmult_r (x y:Z) (P:Z -> Prop) 
+  (H:P (x * - y)%Z) := eq_ind_r P H (Zopp_mult_distr_r x y).
+
+Definition fast_Zmult_plus_distr (n m p:Z) (P:Z -> Prop)
+  (H:P (n * p + m * p)%Z) := eq_ind_r P H (Zmult_plus_distr_l n m p).
+Definition fast_Zmult_Zopp_left (x y:Z) (P:Z -> Prop) 
+  (H:P (x * - y)%Z) := eq_ind_r P H (Zmult_opp_comm x y).
+
+Definition fast_Zmult_assoc_r (n m p:Z) (P:Z -> Prop)
+  (H:P (n * (m * p))%Z) := eq_ind_r P H (Zmult_assoc_reverse n m p).
+
+Definition fast_Zred_factor1 (x:Z) (P:Z -> Prop) (H:P (x * 2)%Z) :=
+  eq_ind_r P H (Zred_factor1 x).
+
+Definition fast_Zred_factor2 (x y:Z) (P:Z -> Prop) 
+  (H:P (x * (1 + y))%Z) := eq_ind_r P H (Zred_factor2 x y).
+Definition fast_Zred_factor3 (x y:Z) (P:Z -> Prop) 
+  (H:P (x * (1 + y))%Z) := eq_ind_r P H (Zred_factor3 x y).
+
+Definition fast_Zred_factor4 (x y z:Z) (P:Z -> Prop) 
+  (H:P (x * (y + z))%Z) := eq_ind_r P H (Zred_factor4 x y z).
+
+Definition fast_Zred_factor5 (x y:Z) (P:Z -> Prop) 
+  (H:P y) := eq_ind_r P H (Zred_factor5 x y).
+
+Definition fast_Zred_factor6 (x:Z) (P:Z -> Prop) (H:P (x + 0)%Z) :=
+  eq_ind_r P H (Zred_factor6 x).
\ No newline at end of file