Merge PR #10875: [Stdlib] Remove some uses of the “omega” tactic

Reviewed-by: fajb

18 files changed, 459 insertions, 285 deletions

diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v
index 7e04fe0220..3351c7ef8a 100644
--- a/plugins/micromega/Lia.v
+++ b/plugins/micromega/Lia.v
@@ -44,9 +44,9 @@ Ltac zchecker_ext :=
                                 (@eq_refl bool true <: @eq bool (ZTautoCheckerExt __ff __wit) true)
                                 (@find Z Z0 __varmap)).
 
-Ltac lia := zify; xlia zchecker_ext.
+Ltac lia := PreOmega.zify; xlia zchecker_ext.
                
-Ltac nia := zify; xnlia zchecker.
+Ltac nia := PreOmega.zify; xnlia zchecker.
 
 
 (* Local Variables: *)
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index 4f90d2b415..c160e11467 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -22,6 +22,7 @@ Require  FSetPositive FSetEqProperties.
 Require Import ZCoeff.
 Require Import Refl.
 Require Import ZArith.
+Require PreOmega.
 (*Declare ML Module "micromega_plugin".*)
 Local Open Scope Z_scope.
 
@@ -100,11 +101,16 @@ Require Import EnvRing.
 
 Lemma Zsor : SOR 0 1 Z.add Z.mul Z.sub Z.opp (@eq Z) Z.le Z.lt.
 Proof.
-  constructor ; intros ; subst ; try (intuition (auto  with zarith)).
+  constructor ; intros ; subst; try reflexivity.
   apply Zsth.
   apply Zth.
+  auto using Z.le_antisymm.
+  eauto using Z.le_trans.
+  apply Z.le_neq.
   destruct (Z.lt_trichotomy n m) ; intuition.
+  apply Z.add_le_mono_l; assumption.
   apply Z.mul_pos_pos ; auto.
+  discriminate.
 Qed.
 
 Lemma ZSORaddon :
@@ -195,7 +201,8 @@ Proof.
         (fun x : N => x) (pow_N 1 Z.mul) env Flhs).
   generalize ((eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x)
         (fun x : N => x) (pow_N 1 Z.mul) env Frhs)).
-  destruct Fop ; simpl; intros ; intuition (auto with zarith).
+  destruct Fop ; simpl; intros;
+    intuition auto using Z.le_ge, Z.ge_le, Z.lt_gt, Z.gt_lt.
 Qed.
 
 
@@ -531,7 +538,10 @@ Proof.
     apply Z.mul_le_mono_pos_l in H; auto with zarith.
   - assert (0 < Z.pos r) by easy.
     rewrite Z.add_1_r, Z.le_succ_l.
-    apply Z.mul_lt_mono_pos_l with a; auto with zarith.
+    apply Z.mul_lt_mono_pos_l with a.
+    auto using Z.gt_lt.
+    eapply Z.lt_le_trans. 2: eassumption.
+    now apply Z.lt_add_pos_r.
   - now elim H1.
 Qed.
 
@@ -627,20 +637,15 @@ Qed.
 
 Lemma Zgcd_pol_ge : forall p, fst (Zgcd_pol p) >= 0.
 Proof.
-  induction p.
-  simpl. auto with zarith.
-  simpl. auto.
+  induction p. 1-2: easy.
   simpl.
   case_eq (Zgcd_pol p1).
   case_eq (Zgcd_pol p3).
   intros.
   simpl.
   unfold ZgcdM.
-  generalize (Z.gcd_nonneg z1 z2).
-  generalize (Zmax_spec (Z.gcd z1 z2) 1).
-  generalize (Z.gcd_nonneg (Z.max (Z.gcd z1 z2) 1) z).
-  generalize (Zmax_spec (Z.gcd (Z.max (Z.gcd z1 z2) 1) z) 1).
-  auto with zarith.
+  apply Z.le_ge; transitivity 1. easy.
+  apply Z.le_max_r.
 Qed.
 
 Lemma Zdivide_pol_Zdivide : forall p x y, Zdivide_pol x p -> (y | x) ->  Zdivide_pol y p.
@@ -698,7 +703,7 @@ Proof.
   induction p.
   simpl.
   intros. inversion H.
-  constructor.  replace (c - 0) with c in H1 ; auto with zarith.
+  constructor. rewrite Z.sub_0_r in *. assumption.
   intros.
   constructor.
   simpl in H. inversion H ; subst; clear H.
@@ -735,7 +740,7 @@ Proof.
   destruct HH2.
   rewrite H2.
   apply Zdivide_pol_sub ; auto.
-  auto with zarith.
+  apply Z.lt_le_trans with 1. reflexivity. now apply Z.ge_le.
   destruct HH2. rewrite H2.
   apply Zdivide_pol_one.
   unfold ZgcdM in HH1. unfold ZgcdM.
@@ -1050,7 +1055,7 @@ Fixpoint bdepth (pf : ZArithProof) : nat :=
     | DoneProof  => O
     | RatProof _ p =>  S (bdepth p)
     | CutProof _  p =>   S  (bdepth p)
-    | EnumProof _ _ l => S (List.fold_right (fun pf x => Max.max (bdepth pf) x)   O l)
+    | EnumProof _ _ l => S (List.fold_right (fun pf x => Nat.max (bdepth pf) x)   O l)
   end.
 
 Require Import Wf_nat.
@@ -1069,19 +1074,19 @@ Proof.
   unfold ltof.
   simpl.
   generalize (         (fold_right
-            (fun (pf : ZArithProof) (x : nat) => Max.max (bdepth pf) x) 0%nat l)).
+            (fun (pf : ZArithProof) (x : nat) => Nat.max (bdepth pf) x) 0%nat l)).
   intros.
   generalize (bdepth y) ; intros.
-  generalize (Max.max_l n0 n) (Max.max_r n0 n).
-  auto with zarith.
+  rewrite Nat.lt_succ_r. apply Nat.le_max_l.
   generalize (IHl a0 b  y  H).
   unfold ltof.
   simpl.
-  generalize (      (fold_right (fun (pf : ZArithProof) (x : nat) => Max.max (bdepth pf) x) 0%nat
+  generalize (      (fold_right (fun (pf : ZArithProof) (x : nat) => Nat.max (bdepth pf) x) 0%nat
          l)).
   intros.
-  generalize (Max.max_l (bdepth a) n) (Max.max_r (bdepth a) n).
-  auto with zarith.
+  eapply lt_le_trans. eassumption.
+  rewrite <- Nat.succ_le_mono.
+  apply Nat.le_max_r.
 Qed.
 
 
@@ -1113,10 +1118,14 @@ Proof.
   intros.
   inv H2.
   change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in *.
-  apply Zgcd_pol_correct_lt with (env:=env) in H1.
-  generalize (narrow_interval_lower_bound g (- c0) (eval_pol env (Zdiv_pol (PsubC Z.sub e c0) g)) H0).
-  auto with zarith.
-  auto with zarith.
+  apply Zgcd_pol_correct_lt with (env:=env) in H1. 2: auto using Z.gt_lt.
+  apply Z.le_add_le_sub_l, Z.ge_le; rewrite Z.add_0_r.
+  apply (narrow_interval_lower_bound g (- c0) (eval_pol env (Zdiv_pol (PsubC Z.sub e c0) g)) H0).
+  apply Z.le_ge.
+  rewrite <- Z.sub_0_l.
+  apply Z.le_sub_le_add_r.
+  rewrite <- H1.
+  assumption.
   (* g <= 0 *)
   intros. inv H2. auto with zarith.
 Qed.
@@ -1143,7 +1152,7 @@ Proof.
   case_eq (Z.gtb g 0).
   intros.
   rewrite <- Zgt_is_gt_bool in H.  
-  rewrite Zgcd_pol_correct_lt with (1:= H1)  in H2; auto with zarith.
+  rewrite Zgcd_pol_correct_lt with (1:= H1)  in H2. 2: auto using Z.gt_lt.
   unfold nformula_of_cutting_plane.  
   change (eval_pol env (padd e' (Pc z)) = 0).
   inv H3.
@@ -1159,7 +1168,7 @@ Proof.
   apply Zeq_bool_eq in H0.
   subst. simpl.
   rewrite Z.add_0_r, Z.mul_eq_0 in H2.
-  intuition auto with zarith.
+  intuition subst; easy.
   rewrite negb_false_iff in H0.
   apply Zeq_bool_eq in H0.
   assert (HH := Zgcd_is_gcd g c).
@@ -1168,14 +1177,15 @@ Proof.
   apply Zdivide_opp_r in H4.
   rewrite Zdivide_ceiling ; auto.
   apply Z.sub_move_0_r.
-  apply Z.div_unique_exact ; auto with zarith.
+  apply Z.div_unique_exact. now intros ->.
+  now rewrite Z.add_move_0_r in H2.
   intros.
   unfold nformula_of_cutting_plane.
   inv H3.
   change (eval_pol env (padd e' (Pc 0)) = 0).
   rewrite eval_pol_add.
   simpl.
-  auto with zarith.
+  now rewrite Z.add_0_r.
   (* NonEqual *)
   intros.
   inv H0.
@@ -1184,7 +1194,7 @@ Proof.
   unfold nformula_of_cutting_plane.
   unfold eval_op1 in *.
   rewrite (RingMicromega.eval_pol_add Zsor ZSORaddon).
-  simpl. auto with zarith.
+  simpl. now rewrite Z.add_0_r.
   (* Strict *)
   destruct p as [[e' z] op].
   case_eq (makeCuttingPlane (PsubC Z.sub e 1)).
@@ -1193,7 +1203,7 @@ Proof.
   apply makeCuttingPlane_ns_sound with (env:=env) (2:= H).
   simpl in *.
   rewrite (RingMicromega.PsubC_ok Zsor ZSORaddon).
-  auto with zarith.
+  now apply Z.lt_le_pred.
   (* NonStrict *)
   destruct p as [[e' z] op].
   case_eq (makeCuttingPlane e).
@@ -1220,13 +1230,14 @@ Proof.
   rewrite negb_true_iff in H.
   apply Zeq_bool_neq in H.
   change (eval_pol env p = 0) in H2.
-  rewrite Zgcd_pol_correct_lt with (1:= H0) in H2; auto with zarith.
+  rewrite Zgcd_pol_correct_lt with (1:= H0) in H2. 2: auto using Z.gt_lt.
   set (x:=eval_pol env (Zdiv_pol (PsubC Z.sub p c) g)) in *; clearbody x.
   contradict H5.
-  apply Zis_gcd_gcd; auto with zarith.
+  apply Zis_gcd_gcd. apply Z.lt_le_incl, Z.gt_lt; assumption.
   constructor; auto with zarith.
   exists (-x).
-  rewrite Z.mul_opp_l, Z.mul_comm; auto with zarith.
+  rewrite Z.mul_opp_l, Z.mul_comm.
+  now apply Z.add_move_0_l.
   (**)
   destruct (makeCuttingPlane p);  discriminate.
   discriminate.
@@ -1321,11 +1332,13 @@ Proof.
    change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in HCutR.
    unfold eval_op1 in HCutR.
    destruct op1 ; simpl in Hop1 ; try discriminate;
-     rewrite eval_pol_add in HCutR; simpl in HCutR; auto with zarith.
+     rewrite eval_pol_add in HCutR; simpl in HCutR.
+     rewrite Z.add_move_0_l in HCutR; rewrite HCutR, Z.opp_involutive; reflexivity.
+     now apply Z.le_sub_le_add_r in HCutR.
    (**)
    apply is_pol_Z0_eval_pol with (env := env) in HZ0.
-   rewrite eval_pol_add in HZ0.
-   replace (eval_pol env p1) with (- eval_pol env p2) by omega.
+   rewrite eval_pol_add, Z.add_move_r, Z.sub_0_l in HZ0.
+   rewrite HZ0.
    apply  eval_Psatz_sound with (env:=env) in Hf1 ; auto.
    apply cutting_plane_sound with (1:= Hf1) in HCutL.
    unfold nformula_of_cutting_plane in HCutL.
@@ -1334,7 +1347,10 @@ Proof.
    change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in HCutL.
    unfold eval_op1 in HCutL.
    rewrite eval_pol_add in HCutL. simpl in HCutL.
-   destruct op2 ; simpl in Hop2 ; try discriminate ;  omega.
+   destruct op2 ; simpl in Hop2 ; try discriminate.
+   rewrite Z.add_move_r, Z.sub_0_l in HCutL.
+   now rewrite HCutL, Z.opp_involutive.
+   now rewrite <- Z.le_sub_le_add_l in HCutL.
   revert Hfix.
   match goal with
     | |- context[?F pf (-z1) z2 = true] => set (FF := F)
@@ -1348,26 +1364,24 @@ Proof.
   generalize (-z1). clear z1. intro z1.
   revert z1 z2.
   induction pf;simpl ;intros.
-  generalize (Zgt_cases z1 z2).
-  destruct (Z.gtb z1 z2).
-  intros.
-  apply False_ind ; omega.
-  discriminate.
+  revert Hfix.
+  now case (Z.gtb_spec); [ | easy ]; intros LT; elim (Zlt_not_le _ _ LT); transitivity x.
   flatten_bool.
-  assert (HH:(x = z1 \/ z1 +1 <=x)%Z) by omega.
-  destruct HH.
-  subst.
-  exists a ; auto.
-  assert (z1 + 1 <= x <= z2)%Z by omega.
-  elim IHpf with (2:=H2) (3:= H4).
-  destruct H4.
+  destruct (Z_le_lt_eq_dec _ _ (proj1 H0)) as [ LT | -> ].
+  2: exists a; auto.
+  rewrite <- Z.le_succ_l in LT.
+  assert (LE: (Z.succ z1 <= x <= z2)%Z) by intuition.
+  elim IHpf with (2:=H2) (3:= LE).
   intros.
   exists x0 ; split;tauto.
   intros until 1. 
   apply H ; auto. 
   unfold ltof in *.
   simpl in *.
-  zify. omega.
+  PreOmega.zify.
+  intuition subst. assumption.
+  eapply Z.lt_le_trans. eassumption.
+  apply Z.add_le_mono_r. assumption.
   (*/asser *)
   destruct (HH _ H1) as [pr [Hin Hcheker]].
   assert (make_impl (eval_nformula env) ((PsubC Z.sub p1 (eval_pol env p1),Equal) :: l) False).
diff --git a/plugins/micromega/ZifyBool.v b/plugins/micromega/ZifyBool.v
index 6259c5b47a..03a7774a31 100644
--- a/plugins/micromega/ZifyBool.v
+++ b/plugins/micromega/ZifyBool.v
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 Require Import Bool ZArith.
-Require Import ZifyClasses.
+Require Import Zify ZifyClasses.
 Local Open Scope Z_scope.
 (* Instances of [ZifyClasses] for dealing with boolean operators.
    Various encodings of boolean are possible.  One objective is to
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 7c69350db4..ea4062d9fe 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -1363,7 +1363,8 @@ Lemma elements_aux_cardinal :
 Proof.
  simple induction m; simpl; intuition.
  rewrite <- H; simpl.
- rewrite <- H0; omega.
+ rewrite <- H0, Nat.add_succ_r, (Nat.add_comm (cardinal t)), Nat.add_assoc.
+ reflexivity.
 Qed.
 
 Lemma elements_cardinal : forall (m:t elt), cardinal m = length (elements m).
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index 0ef356b582..fa553d9fce 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -68,7 +68,7 @@ Hint Constructors avl : core.
 Lemma height_non_negative : forall (s : t elt), avl s ->
  height s >= 0.
 Proof.
- induction s; simpl; intros; auto with zarith.
+ induction s; simpl; intros. now apply Z.le_ge.
  inv avl; intuition; omega_max.
 Qed.
 
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index e5133f66b2..342a51b39b 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -476,8 +476,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
    unfold elements.
    intros m; set (p:=1); clearbody p; revert m p.
    induction m; simpl; auto; intros.
-   rewrite (IHm1 (append p 2)), (IHm2 (append p 3)); auto.
-   destruct o; rewrite app_length; simpl; omega.
+   rewrite (IHm1 (append p 2)), (IHm2 (append p 3)).
+   destruct o; rewrite app_length; simpl; auto.
   Qed.
 
   End CompcertSpec.
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index da504259f5..1983c6caa1 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -17,7 +17,7 @@
     [mem x s=true] instead of [In x s],
     [equal s s'=true] instead of [Equal s s'], etc. *)
 
-Require Import FSetProperties Zerob Sumbool Omega DecidableTypeEx.
+Require Import FSetProperties Zerob Sumbool DecidableTypeEx.
 
 Module WEqProperties_fun (Import E:DecidableType)(M:WSfun E).
 Module Import MP := WProperties_fun E M.
@@ -847,11 +847,16 @@ Proof.
 unfold sum.
 intros f g Hf Hg.
 assert (fc : compat_opL (fun x:elt =>plus (f x))).  red; auto with fset.
-assert (ft : transposeL (fun x:elt =>plus (f x))). red; intros; omega.
+assert (ft : transposeL (fun x:elt =>plus (f x))). red; intros x y z.
+  rewrite !PeanoNat.Nat.add_assoc, (PeanoNat.Nat.add_comm (f x) (f y)); reflexivity.
 assert (gc : compat_opL (fun x:elt => plus (g x))). red; auto with fset.
-assert (gt : transposeL (fun x:elt =>plus (g x))). red; intros; omega.
+assert (gt : transposeL (fun x:elt =>plus (g x))). red; intros x y z.
+  rewrite !PeanoNat.Nat.add_assoc, (PeanoNat.Nat.add_comm (g x) (g y)); reflexivity.
 assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))). repeat red; auto.
-assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))). red; intros; omega.
+assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))). red; intros x y z.
+  set (u := (f x + g x)); set (v := (f y + g y)).
+  rewrite !PeanoNat.Nat.add_assoc, (PeanoNat.Nat.add_comm u).
+  reflexivity.
 assert (st : Equivalence (@Logic.eq nat)) by (split; congruence).
 intros s;pattern s; apply set_rec.
 intros.
@@ -859,7 +864,10 @@ rewrite <- (fold_equal _ _ st _ fc ft 0 _ _ H).
 rewrite <- (fold_equal _ _ st _ gc gt 0 _ _ H).
 rewrite <- (fold_equal _ _ st _ fgc fgt 0 _ _ H); auto.
 intros; do 3 (rewrite (fold_add _ _ st);auto).
-rewrite H0;simpl;omega.
+rewrite H0;simpl.
+rewrite <- !(PeanoNat.Nat.add_assoc (f x)); f_equal.
+rewrite !PeanoNat.Nat.add_assoc. f_equal.
+apply PeanoNat.Nat.add_comm.
 do 3 rewrite fold_empty;auto.
 Qed.
 
@@ -872,7 +880,11 @@ assert (cc : compat_opL (fun x => plus (if f x then 1 else 0))).
  repeat red; intros.
  rewrite (Hf _ _ H); auto.
 assert (ct : transposeL (fun x => plus (if f x then 1 else 0))).
- red; intros; omega.
+ red; intros.
+ set (a := if f x then _ else _).
+ rewrite PeanoNat.Nat.add_comm.
+ rewrite <- !PeanoNat.Nat.add_assoc. f_equal.
+ apply PeanoNat.Nat.add_comm.
 intros s;pattern s; apply set_rec.
 intros.
 change elt with E.t.
@@ -921,9 +933,11 @@ Lemma sum_compat :
   forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g ->
   forall s, (forall x, In x s -> f x=g x) -> sum f s=sum g s.
 intros.
-unfold sum; apply (fold_compat _ (@Logic.eq nat)); auto with *.
+unfold sum; apply (fold_compat _ (@Logic.eq nat)); auto with fset.
 intros x x' Hx y y' Hy. rewrite Hx, Hy; auto.
+intros x y z; rewrite !PeanoNat.Nat.add_assoc; f_equal; apply PeanoNat.Nat.add_comm.
 intros x x' Hx y y' Hy. rewrite Hx, Hy; auto.
+intros x y z; rewrite !PeanoNat.Nat.add_assoc; f_equal; apply PeanoNat.Nat.add_comm.
 Qed.
 
 End Sum.
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index b60feb9256..54d35cded2 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -79,7 +79,7 @@ Notation "x <= y <= z" := (x<=y/\y<=z) : Q_scope.
 
 Lemma inject_Z_injective (a b: Z): inject_Z a == inject_Z b <-> a = b.
 Proof.
- unfold Qeq. simpl. omega.
+ unfold Qeq; simpl; rewrite !Z.mul_1_r; reflexivity.
 Qed.
 
 (** Another approach : using Qcompare for defining order relations. *)
@@ -599,9 +599,7 @@ Proof.
 Qed.
 
 Lemma Qle_antisym x y : x<=y -> y<=x -> x==y.
-Proof.
-  unfold Qle, Qeq; auto with zarith.
-Qed.
+Proof. apply Z.le_antisymm. Qed.
 
 Lemma Qle_trans : forall x y z, x<=y -> y<=z -> x<=z.
 Proof.
@@ -618,14 +616,10 @@ Qed.
 Hint Resolve Qle_trans : qarith.
 
 Lemma Qlt_irrefl x : ~x<x.
-Proof.
- unfold Qlt. auto with zarith.
-Qed.
+Proof. apply Z.lt_irrefl. Qed.
 
 Lemma Qlt_not_eq x y : x<y -> ~ x==y.
-Proof.
-  unfold Qlt, Qeq; auto with zarith.
-Qed.
+Proof. apply Z.lt_neq. Qed.
 
 Lemma Zle_Qle (x y: Z): (x <= y)%Z = (inject_Z x <= inject_Z y).
 Proof.
@@ -647,9 +641,7 @@ Proof.
 Qed.
 
 Lemma Qlt_le_weak x y : x<y -> x<=y.
-Proof.
-  unfold Qle, Qlt; auto with zarith.
-Qed.
+Proof. apply Z.lt_le_incl. Qed.
 
 Lemma Qle_lt_trans : forall x y z, x<=y -> y<z -> x<z.
 Proof.
@@ -684,25 +676,17 @@ Qed.
 
 (** [x<y] iff [~(y<=x)] *)
 
-Lemma Qnot_lt_le : forall x y, ~ x<y -> y<=x.
-Proof.
-  unfold Qle, Qlt; auto with zarith.
-Qed.
+Lemma Qnot_lt_le x y : ~ x < y -> y <= x.
+Proof. apply Z.nlt_ge. Qed.
 
-Lemma Qnot_le_lt : forall x y, ~ x<=y -> y<x.
-Proof.
-  unfold Qle, Qlt; auto with zarith.
-Qed.
+Lemma Qnot_le_lt x y : ~ x <= y -> y < x.
+Proof. apply Z.nle_gt. Qed.
 
-Lemma Qlt_not_le : forall x y, x<y -> ~ y<=x.
-Proof.
-  unfold Qle, Qlt; auto with zarith.
-Qed.
+Lemma Qlt_not_le x y : x < y -> ~ y <= x.
+Proof. apply Z.lt_nge. Qed.
 
-Lemma Qle_not_lt : forall x y, x<=y -> ~ y<x.
-Proof.
-  unfold Qle, Qlt; auto with zarith.
-Qed.
+Lemma Qle_not_lt x y : x <= y -> ~ y < x.
+Proof. apply Z.le_ngt. Qed.
 
 Lemma Qle_lt_or_eq : forall x y, x<=y -> x<y \/ x==y.
 Proof.
@@ -746,21 +730,24 @@ Defined.
 Lemma Qopp_le_compat : forall p q, p<=q -> -q <= -p.
 Proof.
   intros (a1,a2) (b1,b2); unfold Qle, Qlt; simpl.
-  rewrite !Z.mul_opp_l. omega.
+  now rewrite !Z.mul_opp_l, <- Z.opp_le_mono.
 Qed.
 
+
 Hint Resolve Qopp_le_compat : qarith.
 
 Lemma Qle_minus_iff : forall p q, p <= q <-> 0 <= q+-p.
 Proof.
   intros (x1,x2) (y1,y2); unfold Qle; simpl.
-  rewrite Z.mul_opp_l. omega.
+  rewrite Z.mul_1_r, Z.mul_opp_l, <- Z.le_sub_le_add_r, Z.opp_involutive.
+  reflexivity.
 Qed.
 
 Lemma Qlt_minus_iff : forall p q, p < q <-> 0 < q+-p.
 Proof.
   intros (x1,x2) (y1,y2); unfold Qlt; simpl.
-  rewrite Z.mul_opp_l. omega.
+  rewrite Z.mul_1_r, Z.mul_opp_l, <- Z.lt_sub_lt_add_r, Z.opp_involutive.
+  reflexivity.
 Qed.
 
 Lemma Qplus_le_compat :
@@ -831,9 +818,11 @@ Lemma Qmult_le_compat_r : forall x y z, x <= y -> 0 <= z -> x*z <= y*z.
 Proof.
   intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl.
   Open Scope Z_scope.
+  rewrite Z.mul_1_r.
   intros; simpl_mult.
   rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1).
-  apply Z.mul_le_mono_nonneg_r; auto with zarith.
+  apply Z.mul_le_mono_nonneg_r; auto.
+  now apply Z.mul_nonneg_nonneg.
   Close Scope Z_scope.
 Qed.
 
@@ -843,9 +832,10 @@ Proof.
   Open Scope Z_scope.
   simpl_mult.
   rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1).
+  rewrite Z.mul_1_r.
   intros LT LE.
   apply Z.mul_le_mono_pos_r in LE; trivial.
-  apply Z.mul_pos_pos; [omega|easy].
+  apply Z.mul_pos_pos; easy.
   Close Scope Z_scope.
 Qed.
 
@@ -866,10 +856,11 @@ Lemma Qmult_lt_compat_r : forall x y z, 0 < z  -> x < y -> x*z < y*z.
 Proof.
   intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl.
   Open Scope Z_scope.
+  rewrite Z.mul_1_r.
   intros; simpl_mult.
   rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1).
   apply Z.mul_lt_mono_pos_r; auto with zarith.
-  apply Z.mul_pos_pos; [omega|reflexivity].
+  apply Z.mul_pos_pos; easy.
   Close Scope Z_scope.
 Qed.
 
@@ -880,8 +871,9 @@ Proof.
  unfold Qle, Qlt; simpl.
  simpl_mult.
  rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1).
+ rewrite Z.mul_1_r.
  intro LT. rewrite <- Z.mul_lt_mono_pos_r. reflexivity.
- apply Z.mul_pos_pos; [omega|reflexivity].
+ now apply Z.mul_pos_pos.
  Close Scope Z_scope.
 Qed.
 
@@ -896,6 +888,7 @@ Proof.
 intros a b Ha Hb.
 unfold Qle in *.
 simpl in *.
+rewrite Z.mul_1_r in *.
 auto with *.
 Qed.
 
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index 78cd549ce6..e314f64028 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.v
@@ -35,7 +35,7 @@ Proof.
   rewrite <- Hg in LE; clear Hg.
   assert (0 <> g) by (intro; subst; discriminate).
   rewrite Z2Pos.id. ring.
-  rewrite <- (Z.mul_pos_cancel_l g); [now rewrite <- Hd | omega].
+  now rewrite <- (Z.mul_pos_cancel_l g); [ rewrite <- Hd | apply Z.le_neq ].
   Close Scope Z_scope.
 Qed.
 
@@ -60,8 +60,8 @@ Proof.
   - congruence.
   - (*rel_prime*)
     constructor.
-    * exists aa; auto with zarith.
-    * exists bb; auto with zarith.
+    * exists aa; auto using Z.mul_1_r.
+    * exists bb; auto using Z.mul_1_r.
     * intros x Ha Hb.
       destruct Hg1 as (Hg11,Hg12,Hg13).
       destruct (Hg13 (g*x)) as (x',Hx).
@@ -73,8 +73,8 @@ Proof.
       apply Z.mul_reg_l with g; auto. rewrite Hx at 1; ring.
   - (* rel_prime *)
     constructor.
-    * exists cc; auto with zarith.
-    * exists dd; auto with zarith.
+    * exists cc; auto using Z.mul_1_r.
+    * exists dd; auto using Z.mul_1_r.
     * intros x Hc Hd.
       inversion Hg'1 as (Hg'11,Hg'12,Hg'13).
       destruct (Hg'13 (g'*x)) as (x',Hx).
@@ -85,9 +85,9 @@ Proof.
       exists x'.
       apply Z.mul_reg_l with g'; auto. rewrite Hx at 1; ring.
   - apply Z.lt_gt.
-    rewrite <- (Z.mul_pos_cancel_l g); [now rewrite <- Hg4 | omega].
+    rewrite <- (Z.mul_pos_cancel_l g); [ now rewrite <- Hg4 |  apply Z.le_neq; intuition ].
   - apply Z.lt_gt.
-    rewrite <- (Z.mul_pos_cancel_l g'); [now rewrite <- Hg'4 | omega].
+    rewrite <- (Z.mul_pos_cancel_l g'); [now rewrite <- Hg'4 | apply Z.le_neq; intuition ].
   - apply Z.mul_reg_l with (g*g').
     * rewrite Z.mul_eq_0. now destruct 1.
     * rewrite Z.mul_shuffle1, <- Hg3, <- Hg'4.
diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v
index af5c471d5d..8d68038582 100644
--- a/theories/QArith/Qround.v
+++ b/theories/QArith/Qround.v
@@ -13,7 +13,8 @@ Require Import QArith.
 Lemma Qopp_lt_compat: forall p q : Q, p < q -> - q < - p.
 Proof.
 intros (a1,a2) (b1,b2); unfold Qle, Qlt; simpl.
-rewrite !Z.mul_opp_l; omega.
+rewrite !Z.mul_opp_l.
+apply Z.opp_lt_mono.
 Qed.
 
 Hint Resolve Qopp_lt_compat : qarith.
@@ -38,7 +39,7 @@ intros z.
 unfold Qceiling.
 simpl.
 rewrite Zdiv_1_r.
-auto with *.
+apply Z.opp_involutive.
 Qed.
 
 Lemma Qfloor_le : forall x, Qfloor x <= x.
@@ -119,7 +120,7 @@ Lemma Qceiling_resp_le : forall x y, x <= y -> (Qceiling x <= Qceiling y)%Z.
 Proof.
 intros x y Hxy.
 unfold Qceiling.
-cut (Qfloor (-y) <= Qfloor (-x))%Z; auto with *.
+rewrite <- Z.opp_le_mono; auto with qarith.
 Qed.
 
 Hint Resolve Qceiling_resp_le : qarith.
diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v
index a760a0af6a..0df1442f46 100644
--- a/theories/Reals/Rtrigo1.v
+++ b/theories/Reals/Rtrigo1.v
@@ -18,6 +18,7 @@ Require Export Cos_rel.
 Require Export Cos_plus.
 Require Import ZArith_base.
 Require Import Zcomplements.
+Import Omega.
 Require Import Lra.
 Require Import Ranalysis1.
 Require Import Rsqrt_def. 
diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v
index a8e6993a63..cc216b21f8 100644
--- a/theories/Structures/OrderedTypeEx.v
+++ b/theories/Structures/OrderedTypeEx.v
@@ -12,7 +12,6 @@ Require Import OrderedType.
 Require Import ZArith.
 Require Import PeanoNat.
 Require Import Ascii String.
-Require Import Omega.
 Require Import NArith Ndec.
 Require Import Compare_dec.
 
@@ -55,7 +54,7 @@ Module Nat_as_OT <: UsualOrderedType.
   Proof. unfold lt; intros; apply lt_trans with y; auto. Qed.
 
   Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
-  Proof. unfold lt, eq; intros; omega. Qed.
+  Proof. unfold lt, eq; intros ? ? LT ->; revert LT; apply Nat.lt_irrefl. Qed.
 
   Definition compare x y : Compare lt eq x y.
   Proof.
@@ -85,10 +84,10 @@ Module Z_as_OT <: UsualOrderedType.
   Definition lt (x y:Z) := (x<y).
 
   Lemma lt_trans : forall x y z, x<y -> y<z -> x<z.
-  Proof. intros; omega. Qed.
+  Proof. exact Z.lt_trans. Qed.
 
   Lemma lt_not_eq : forall x y, x<y -> ~ x=y.
-  Proof. intros; omega. Qed.
+  Proof. intros x y LT ->; revert LT; apply Z.lt_irrefl. Qed.
 
   Definition compare x y : Compare lt eq x y.
   Proof.
diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v
index b0744caa7b..38f9336f1b 100644
--- a/theories/ZArith/ZArith.v
+++ b/theories/ZArith/ZArith.v
@@ -18,6 +18,7 @@ Require Export Zpow_def.
 
 (** Extra modules using [Omega] or [Ring]. *)
 
+Require Export Omega.
 Require Export Zcomplements.
 Require Export Zpower.
 Require Export Zdiv.
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index 73c8ec11c6..0be6f8c8de 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -10,7 +10,6 @@
 
 Require Import ZArithRing.
 Require Import ZArith_base.
-Require Export Omega.
 Require Import Wf_nat.
 Local Open Scope Z_scope.
 
@@ -40,10 +39,19 @@ Proof. reflexivity. Qed.
 
 Lemma floor_ok : forall p:positive, floor p <= Zpos p < 2 * floor p.
 Proof.
- unfold floor. induction p; simpl.
- - rewrite !Pos2Z.inj_xI, (Pos2Z.inj_xO (xO _)), Pos2Z.inj_xO. omega.
- - rewrite (Pos2Z.inj_xO (xO _)), (Pos2Z.inj_xO p), Pos2Z.inj_xO. omega.
- - omega.
+ unfold floor. induction p as [p [IH1p IH2p]|p [IH1p IH2]|]; simpl.
+ - rewrite !Pos2Z.inj_xI, (Pos2Z.inj_xO (xO _)), Pos2Z.inj_xO.
+   split.
+   + apply Z.le_trans with (2 * Z.pos p); auto with zarith.
+     rewrite <- (Z.add_0_r (2 * Z.pos p)) at 1; auto with zarith.
+   + apply Z.lt_le_trans with (2 * (Z.pos p + 1)).
+     * rewrite Z.mul_add_distr_l, Z.mul_1_r.
+       apply Zplus_lt_compat_l; red; auto with zarith.
+     * apply Z.mul_le_mono_nonneg_l; auto with zarith.
+       rewrite Z.add_1_r; apply Zlt_le_succ; auto.
+ - rewrite (Pos2Z.inj_xO (xO _)), (Pos2Z.inj_xO p), Pos2Z.inj_xO.
+   split; auto with zarith.
+ - split; auto with zarith; red; auto.
 Qed.
 
 (**********************************************************************)
@@ -64,9 +72,10 @@ Proof.
   - rewrite Z.abs_eq; auto; intros.
     destruct (H (Z.abs m)); auto with zarith.
     destruct (Zabs_dec m) as [-> | ->]; trivial.
-  - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros.
-    destruct (H (Z.abs m)); auto with zarith.
-    destruct (Zabs_dec m) as [-> | ->]; trivial.
+  - rewrite Z.abs_neq, Z.opp_involutive; intros.
+    + destruct (H (Z.abs m)); auto with zarith.
+      destruct (Zabs_dec m) as [-> | ->]; trivial.
+    + apply Z.opp_le_mono; rewrite Z.opp_involutive; auto.
 Qed.
 
 Theorem Z_lt_abs_induction :
@@ -84,9 +93,10 @@ Proof.
   - rewrite Z.abs_eq; auto; intros.
     elim (H (Z.abs m)); intros; auto with zarith.
     elim (Zabs_dec m); intro eq; rewrite eq; trivial.
-  - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros.
-    destruct (H (Z.abs m)); auto with zarith.
-    destruct (Zabs_dec m) as [-> | ->]; trivial.
+  - rewrite Z.abs_neq, Z.opp_involutive; intros.
+    + destruct (H (Z.abs m)); auto with zarith.
+      destruct (Zabs_dec m) as [-> | ->]; trivial.
+    + apply Z.opp_le_mono; rewrite Z.opp_involutive; auto.
 Qed.
 
 (** To do case analysis over the sign of [z] *)
@@ -129,7 +139,7 @@ Section Zlength_properties.
     clear l. induction l.
     auto with zarith.
     intros. simpl length; simpl Zlength_aux.
-     rewrite IHl, Nat2Z.inj_succ; auto with zarith.
+     rewrite IHl, Nat2Z.inj_succ, Z.add_succ_comm; auto.
     unfold Zlength. now rewrite H.
   Qed.
 
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 78df9941c9..2aaab3e50e 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -14,7 +14,7 @@
 (** Initial Contribution by Claude Marché and Xavier Urbain *)
 
 Require Export ZArith_base.
-Require Import Zbool Omega ZArithRing Zcomplements Setoid Morphisms.
+Require Import Zbool ZArithRing Zcomplements Setoid Morphisms.
 Local Open Scope Z_scope.
 
 (** The definition of the division is now in [BinIntDef], the initial
@@ -67,7 +67,12 @@ Definition Remainder_alt r b :=  Z.abs r < Z.abs b /\ Z.sgn r <> - Z.sgn b.
 
 Lemma Remainder_equiv : forall r b, Remainder r b <-> Remainder_alt r b.
 Proof.
- intros; unfold Remainder, Remainder_alt; omega with *.
+  unfold Remainder, Remainder_alt.
+  intros [ | r | r ] [ | b | b ]; intuition try easy.
+  - now apply Z.opp_lt_mono.
+  - right; split.
+    + now apply Z.opp_lt_mono.
+    + apply Pos2Z.neg_is_nonpos.
 Qed.
 
 Hint Unfold Remainder : core.
@@ -104,7 +109,7 @@ Proof (Z.mod_neg_bound a b).
 
 Lemma Z_div_mod_eq a b : b > 0 -> a = b*(a/b) + (a mod b).
 Proof.
-  intros Hb; apply Z.div_mod; auto with zarith.
+  intros Hb; apply Z.div_mod; now intros ->.
 Qed.
 
 Lemma Zmod_eq_full a b : b<>0 -> a mod b = a - (a/b)*b.
@@ -224,18 +229,25 @@ Proof Z.div_mul.
 (* Division of positive numbers is positive. *)
 
 Lemma Z_div_pos: forall a b, b > 0 -> 0 <= a -> 0 <= a/b.
-Proof. intros. apply Z.div_pos; auto with zarith. Qed.
+Proof. intros. apply Z.div_pos; auto using Z.gt_lt. Qed.
 
 Lemma Z_div_ge0: forall a b, b > 0 -> a >= 0 -> a/b >=0.
 Proof.
-  intros; generalize (Z_div_pos a b H); auto with zarith.
+  intros; apply Z.le_ge, Z_div_pos; auto using Z.ge_le.
 Qed.
 
 (** As soon as the divisor is greater or equal than 2,
     the division is strictly decreasing. *)
 
 Lemma Z_div_lt : forall a b:Z, b >= 2 -> a > 0 -> a/b < a.
-Proof. intros. apply Z.div_lt; auto with zarith. Qed.
+Proof.
+  intros a b b_ge_2 a_gt_0.
+  apply Z.div_lt.
+  - apply Z.gt_lt; exact a_gt_0.
+  - apply (Z.lt_le_trans _ 2).
+    + reflexivity.
+    + apply Z.ge_le; exact b_ge_2.
+Qed.
 
 (** A division of a small number by a bigger one yields zero. *)
 
@@ -250,17 +262,17 @@ Proof Z.mod_small.
 (** [Z.ge] is compatible with a positive division. *)
 
 Lemma Z_div_ge : forall a b c:Z, c > 0 -> a >= b -> a/c >= b/c.
-Proof. intros. apply Z.le_ge. apply Z.div_le_mono; auto with zarith. Qed.
+Proof. intros. apply Z.le_ge. apply Z.div_le_mono; auto using Z.gt_lt, Z.ge_le. Qed.
 
 (** Same, with [Z.le]. *)
 
 Lemma Z_div_le : forall a b c:Z, c > 0 -> a <= b -> a/c <= b/c.
-Proof. intros. apply Z.div_le_mono; auto with zarith. Qed.
+Proof. intros. apply Z.div_le_mono; auto using Z.gt_lt. Qed.
 
 (** With our choice of division, rounding of (a/b) is always done toward bottom: *)
 
 Lemma Z_mult_div_ge : forall a b:Z, b > 0 -> b*(a/b) <= a.
-Proof. intros. apply Z.mul_div_le; auto with zarith. Qed.
+Proof. intros. apply Z.mul_div_le; auto using Z.gt_lt. Qed.
 
 Lemma Z_mult_div_ge_neg : forall a b:Z, b < 0 -> b*(a/b) >= a.
 Proof. intros. apply Z.le_ge. apply Z.mul_div_ge; auto with zarith. Qed.
@@ -296,14 +308,18 @@ Proof. intros a b q; rewrite Z.mul_comm; apply Z.div_le_lower_bound. Qed.
 
 Lemma Zdiv_le_compat_l: forall p q r, 0 <= p -> 0 < q < r ->
     p / r <= p / q.
-Proof. intros; apply Z.div_le_compat_l; auto with zarith. Qed.
+Proof. intros; apply Z.div_le_compat_l; intuition auto using Z.lt_le_incl. Qed.
 
 Theorem Zdiv_sgn: forall a b,
   0 <= Z.sgn (a/b) * Z.sgn a * Z.sgn b.
 Proof.
   destruct a as [ |a|a]; destruct b as [ |b|b]; simpl; auto with zarith;
   generalize (Z.div_pos (Zpos a) (Zpos b)); unfold Z.div, Z.div_eucl;
-  destruct Z.pos_div_eucl as (q,r); destruct r; omega with *.
+  destruct Z.pos_div_eucl as (q,r); destruct r;
+  rewrite ?Z.mul_1_r, <-?Z.opp_eq_mul_m1, ?Z.sgn_opp, ?Z.opp_involutive;
+  match goal with [|- (_ -> _ -> ?P) -> _] =>
+     intros HH; assert (HH1 : P); auto with zarith
+  end; apply Z.sgn_nonneg; auto with zarith.
 Qed.
 
 (** * Relations between usual operations and Z.modulo and Z.div *)
@@ -346,14 +362,14 @@ Proof. intros. zero_or_not b. apply Z.div_opp_l_z; auto. Qed.
 
 Lemma Z_div_nz_opp_full : forall a b:Z, a mod b <> 0 ->
  (-a)/b = -(a/b)-1.
-Proof. intros a b. zero_or_not b. intros; rewrite Z.div_opp_l_nz; auto. Qed.
+Proof. intros a b. zero_or_not b. easy. intros; rewrite Z.div_opp_l_nz; auto. Qed.
 
 Lemma Z_div_zero_opp_r : forall a b:Z, a mod b = 0 -> a/(-b) = -(a/b).
 Proof. intros. zero_or_not b. apply Z.div_opp_r_z; auto. Qed.
 
 Lemma Z_div_nz_opp_r : forall a b:Z, a mod b <> 0 ->
  a/(-b) = -(a/b)-1.
-Proof. intros a b. zero_or_not b. intros; rewrite Z.div_opp_r_nz; auto. Qed.
+Proof. intros a b. zero_or_not b. easy. intros; rewrite Z.div_opp_r_nz; auto. Qed.
 
 (** Cancellations. *)
 
@@ -372,14 +388,16 @@ Lemma Zmult_mod_distr_l: forall a b c,
   (c*a) mod (c*b) = c * (a mod b).
 Proof.
  intros. zero_or_not c. rewrite (Z.mul_comm c b); zero_or_not b.
- rewrite (Z.mul_comm b c). apply Z.mul_mod_distr_l; auto.
+ + now rewrite Z.mul_0_r.
+ + rewrite (Z.mul_comm b c). apply Z.mul_mod_distr_l; auto.
 Qed.
 
 Lemma Zmult_mod_distr_r: forall a b c,
   (a*c) mod (b*c) = (a mod b) * c.
 Proof.
  intros. zero_or_not b. rewrite (Z.mul_comm b c); zero_or_not c.
- rewrite (Z.mul_comm c b). apply Z.mul_mod_distr_r; auto.
+ + now rewrite Z.mul_0_r.
+ + rewrite (Z.mul_comm c b). apply Z.mul_mod_distr_r; auto.
 Qed.
 
 (** Operations modulo. *)
@@ -456,7 +474,7 @@ Proof. unfold eqm; auto. Qed.
 
 Lemma eqm_trans : forall a b c,
   a == b -> b == c -> a == c.
-Proof. unfold eqm; eauto with *. Qed.
+Proof. now unfold eqm; intros a b c ->. Qed.
 
 Instance eqm_setoid : Equivalence eqm.
 Proof.
@@ -501,7 +519,8 @@ End EqualityModulo.
 Lemma Zdiv_Zdiv : forall a b c, 0<=b -> 0<=c -> (a/b)/c = a/(b*c).
 Proof.
  intros. zero_or_not b. rewrite Z.mul_comm. zero_or_not c.
- rewrite Z.mul_comm. apply Z.div_div; auto with zarith.
+ rewrite Z.mul_comm. apply Z.div_div; auto.
+ apply Z.le_neq; auto.
 Qed.
 
 (** Unfortunately, the previous result isn't always true on negative numbers.
@@ -519,7 +538,10 @@ Qed.
 Theorem Zdiv_mult_le:
  forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a/b) <= (c*a)/b.
 Proof.
- intros. zero_or_not b. apply Z.div_mul_le; auto with zarith. Qed.
+ intros. zero_or_not b. now rewrite Z.mul_0_r.
+ apply Z.div_mul_le; auto.
+ apply Z.le_neq; auto.
+Qed.
 
 (** Z.modulo is related to divisibility (see more in Znumtheory) *)
 
@@ -566,17 +588,17 @@ Qed.
 
 Lemma Z_div_same : forall a, a > 0 -> a/a = 1.
 Proof.
-  intros; apply Z_div_same_full; auto with zarith.
+  now intros; apply Z_div_same_full; intros ->.
 Qed.
 
 Lemma Z_div_plus : forall a b c:Z, c > 0 -> (a + b * c) / c = a / c + b.
 Proof.
-  intros; apply Z_div_plus_full; auto with zarith.
+  now intros; apply Z_div_plus_full; intros ->.
 Qed.
 
 Lemma Z_div_mult : forall a b:Z, b > 0 -> (a*b)/b = a.
 Proof.
-  intros; apply Z_div_mult_full; auto with zarith.
+  now intros; apply Z_div_mult_full; intros ->.
 Qed.
 
 Lemma Z_mod_plus : forall a b c:Z, c > 0 -> (a + b * c) mod c = a mod c.
@@ -591,7 +613,7 @@ Qed.
 
 Lemma Z_div_exact_2 : forall a b:Z, b > 0 -> a mod b = 0 -> a = b*(a/b).
 Proof.
-  intros; apply Z_div_exact_full_2; auto with zarith.
+  now intros; apply Z_div_exact_full_2; auto; intros ->.
 Qed.
 
 Lemma Z_mod_zero_opp : forall a b:Z, b > 0 -> a mod b = 0 -> (-a) mod b = 0.
@@ -673,14 +695,15 @@ Theorem Zdiv_eucl_extended :
 Proof.
   intros b Hb a.
   destruct (Z_le_gt_dec 0 b) as [Hb'|Hb'].
-  - assert (Hb'' : b > 0) by omega.
+  - assert (Hb'' : b > 0) by (apply Z.lt_gt, Z.le_neq; auto).
     rewrite Z.abs_eq; [ apply Zdiv_eucl_exist; assumption | assumption ].
-  - assert (Hb'' : - b > 0) by omega.
+  - assert (Hb'' : - b > 0).
+    { now apply Z.lt_gt, Z.opp_lt_mono; rewrite Z.opp_involutive; apply Z.gt_lt. }
     destruct (Zdiv_eucl_exist Hb'' a) as ((q,r),[]).
     exists (- q, r).
     split.
     + rewrite <- Z.mul_opp_comm; assumption.
-    + rewrite Z.abs_neq; [ assumption | omega ].
+    + rewrite Z.abs_neq; [ assumption | apply Z.lt_le_incl, Z.gt_lt; auto ].
 Qed.
 
 Arguments Zdiv_eucl_extended : default implicits.
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 5d1a13ff6c..01365135c5 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -117,17 +117,23 @@ Proof.
    right. now rewrite <- Z.mod_divide.
 Defined.
 
+Lemma Z_lt_neq {x y: Z} : x < y -> y <> x.
+Proof. auto using Z.lt_neq, Z.neq_sym. Qed.
+
 Theorem Zdivide_Zdiv_eq a b : 0 < a -> (a | b) ->  b = a * (b / a).
 Proof.
  intros Ha H.
- rewrite (Z.div_mod b a) at 1; auto with zarith.
- rewrite Zdivide_mod; auto with zarith.
+ rewrite (Z.div_mod b a) at 1.
+ + rewrite Zdivide_mod; auto with zarith.
+ + auto using Z_lt_neq.
 Qed.
 
 Theorem Zdivide_Zdiv_eq_2 a b c :
  0 < a -> (a | b) -> (c * b) / a = c * (b / a).
 Proof.
- intros. apply Z.divide_div_mul_exact; auto with zarith.
+ intros. apply Z.divide_div_mul_exact.
+ + now apply Z_lt_neq.
+ + auto with zarith.
 Qed.
 
 Theorem Zdivide_le: forall a b : Z,
@@ -139,28 +145,30 @@ Qed.
 Theorem Zdivide_Zdiv_lt_pos a b :
  1 < a -> 0 < b -> (a | b) ->  0 < b / a < b .
 Proof.
-  intros H1 H2 H3; split.
-  apply Z.mul_pos_cancel_l with a; auto with zarith.
-  rewrite <- Zdivide_Zdiv_eq; auto with zarith.
-  now apply Z.div_lt.
+  intros H1 H2 H3.
+  assert (0 < a) by (now transitivity 1).
+  split.
+  + apply Z.mul_pos_cancel_l with a; auto.
+    rewrite <- Zdivide_Zdiv_eq; auto.
+  + now apply Z.div_lt.
 Qed.
 
 Lemma Zmod_div_mod n m a:
  0 < n -> 0 < m -> (n | m) -> a mod n = (a mod m) mod n.
-Proof.
+Proof with auto using Z_lt_neq.
   intros H1 H2 (p,Hp).
-  rewrite (Z.div_mod a m) at 1; auto with zarith.
+  rewrite (Z.div_mod a m) at 1...
   rewrite Hp at 1.
-  rewrite Z.mul_shuffle0, Z.add_comm, Z.mod_add; auto with zarith.
+  rewrite Z.mul_shuffle0, Z.add_comm, Z.mod_add...
 Qed.
 
 Lemma Zmod_divide_minus a b c:
  0 < b -> a mod b = c -> (b | a - c).
-Proof.
-  intros H H1. apply Z.mod_divide; auto with zarith.
-  rewrite Zminus_mod; auto with zarith.
+Proof with auto using Z_lt_neq.
+  intros H H1. apply Z.mod_divide...
+  rewrite Zminus_mod.
   rewrite H1. rewrite <- (Z.mod_small c b) at 1.
-  rewrite Z.sub_diag, Z.mod_0_l; auto with zarith.
+  rewrite Z.sub_diag, Z.mod_0_l...
   subst. now apply Z.mod_pos_bound.
 Qed.
 
@@ -169,10 +177,11 @@ Lemma Zdivide_mod_minus a b c:
 Proof.
   intros (H1, H2) H3.
   assert (0 < b) by Z.order.
-  replace a with ((a - c) + c); auto with zarith.
-  rewrite Z.add_mod; auto with zarith.
-  rewrite (Zdivide_mod (a-c) b); try rewrite Z.add_0_l; auto with zarith.
-  rewrite Z.mod_mod; try apply Zmod_small; auto with zarith.
+  assert (b <> 0) by now apply Z_lt_neq.
+  replace a with ((a - c) + c) by ring.
+  rewrite Z.add_mod; auto.
+  rewrite (Zdivide_mod (a-c) b); try rewrite Z.add_0_l; auto.
+  rewrite Z.mod_mod; try apply Zmod_small; auto.
 Qed.
 
 (** * Greatest common divisor (gcd). *)
@@ -300,8 +309,9 @@ Section extended_euclid_algorithm.
     set (q := u3 / x) in *.
     assert (Hq : 0 <= u3 - q * x < x).
     replace (u3 - q * x) with (u3 mod x).
-    apply Z_mod_lt; omega.
-    assert (xpos : x > 0). omega.
+    apply Z_mod_lt.
+    apply Z.lt_gt, Z.le_neq; auto.
+    assert (xpos : x > 0) by (apply Z.lt_gt, Z.le_neq; auto).
     generalize (Z_div_mod_eq u3 x xpos).
     unfold q.
     intro eq; pattern u3 at 2; rewrite eq; ring.
@@ -325,11 +335,13 @@ Section extended_euclid_algorithm.
     intros;
       apply euclid_rec with
 	(u1 := 1) (u2 := 0) (u3 := a) (v1 := 0) (v2 := 1) (v3 := b);
-	auto with zarith; ring.
+      auto; ring.
     intros;
       apply euclid_rec with
 	(u1 := 1) (u2 := 0) (u3 := a) (v1 := 0) (v2 := -1) (v3 := - b);
-	auto with zarith; try ring.
+      auto; try ring.
+    now apply Z.opp_nonneg_nonpos, Z.lt_le_incl, Z.gt_lt.
+    auto with zarith.
   Qed.
 
 End extended_euclid_algorithm.
@@ -433,22 +445,24 @@ Lemma rel_prime_cross_prod :
     rel_prime a b ->
     rel_prime c d -> b > 0 -> d > 0 -> a * d = b * c -> a = c /\ b = d.
 Proof.
-  intros a b c d; intros.
+  intros a b c d; intros H H0 H1 H2 H3.
   elim (Z.divide_antisym b d).
-  split; auto with zarith.
-  rewrite H4 in H3.
-  rewrite Z.mul_comm in H3.
-  apply Z.mul_reg_l with d; auto with zarith.
-  intros; omega.
-  apply Gauss with a.
-  rewrite H3.
-  auto with zarith.
-  red; auto with zarith.
-  apply Gauss with c.
-  rewrite Z.mul_comm.
-  rewrite <- H3.
-  auto with zarith.
-  red; auto with zarith.
+  - split; auto with zarith.
+    rewrite H4 in H3.
+    rewrite Z.mul_comm in H3.
+    apply Z.mul_reg_l with d; auto.
+    contradict H2; rewrite H2; discriminate.
+  - intros H4; contradict H1; rewrite H4.
+    apply Zgt_asym, Z.lt_gt, Z.opp_lt_mono.
+    now rewrite Z.opp_involutive; apply Z.gt_lt.
+  - apply Gauss with a.
+    + rewrite H3; auto with zarith.
+    + now apply Zis_gcd_sym.
+  - apply Gauss with c.
+    + rewrite Z.mul_comm.
+      rewrite <- H3.
+      auto with zarith.
+    + now apply Zis_gcd_sym.
 Qed.
 
 (** After factorization by a gcd, the original numbers are relatively prime. *)
@@ -457,32 +471,35 @@ Lemma Zis_gcd_rel_prime :
   forall a b g:Z,
     b > 0 -> g >= 0 -> Zis_gcd a b g -> rel_prime (a / g) (b / g).
 Proof.
-  intros a b g; intros.
-  assert (g <> 0).
-  intro.
-  elim H1; intros.
-  elim H4; intros.
-  rewrite H2 in H6; subst b; omega.
+  intros a b g; intros H H0 H1.
+  assert (H2 : g <> 0) by
+    (intro;
+    elim H1; intros;
+    elim H4; intros;
+    rewrite H2 in H6; subst b;
+    contradict H; rewrite Z.mul_0_r; discriminate).
+  assert (H3 : g > 0) by
+    (apply Z.lt_gt, Z.le_neq; split; try apply Z.ge_le; auto).
   unfold rel_prime.
-  destruct H1.
-  destruct H1 as (a',H1).
-  destruct H3 as (b',H3).
+  destruct H1 as [Ha  Hb Hab].
+  destruct Ha as [a' Ha'].
+  destruct Hb as [b' Hb'].
   replace (a/g) with a';
-    [|rewrite H1; rewrite Z_div_mult; auto with zarith].
+    [|rewrite Ha'; rewrite Z_div_mult; auto with zarith].
   replace (b/g) with b';
-    [|rewrite H3; rewrite Z_div_mult; auto with zarith].
+      [|rewrite Hb'; rewrite Z_div_mult; auto with zarith].
   constructor.
-  exists a'; auto with zarith.
-  exists b'; auto with zarith.
-  intros x (xa,H5) (xb,H6).
-  destruct (H4 (x*g)) as (x',Hx').
-  exists xa; rewrite Z.mul_assoc; rewrite <- H5; auto.
-  exists xb; rewrite Z.mul_assoc; rewrite <- H6; auto.
-  replace g with (1*g) in Hx'; auto with zarith.
-  do 2 rewrite Z.mul_assoc in Hx'.
-  apply Z.mul_reg_r in Hx'; trivial.
-  rewrite Z.mul_1_r in Hx'.
-  exists x'; auto with zarith.
+  - exists a'; rewrite ?Z.mul_1_r; auto with zarith.
+  - exists b'; rewrite ?Z.mul_1_r; auto with zarith.
+  - intros x (xa,H5) (xb,H6).
+    destruct (Hab (x*g)) as (x',Hx').
+    exists xa; rewrite Z.mul_assoc; rewrite <- H5; auto.
+    exists xb; rewrite Z.mul_assoc; rewrite <- H6; auto.
+    replace g with (1*g) in Hx'; auto with zarith.
+    do 2 rewrite Z.mul_assoc in Hx'.
+    apply Z.mul_reg_r in Hx'; trivial.
+    rewrite Z.mul_1_r in Hx'.
+    exists x'; auto with zarith.
 Qed.
 
 Theorem rel_prime_sym: forall a b, rel_prime a b -> rel_prime b a.
@@ -504,18 +521,18 @@ Qed.
 Theorem rel_prime_1: forall n, rel_prime 1 n.
 Proof.
   intros n; red; apply Zis_gcd_intro; auto.
-  exists 1; auto with zarith.
-  exists n; auto with zarith.
+  exists 1; reflexivity.
+  exists n; rewrite Z.mul_1_r; reflexivity.
 Qed.
 
 Theorem not_rel_prime_0: forall n, 1 < n -> ~ rel_prime 0 n.
 Proof.
   intros n H H1; absurd (n = 1 \/ n = -1).
-  intros [H2 | H2]; subst; contradict H; auto with zarith.
+  intros [H2 | H2]; subst; contradict H; discriminate.
   case (Zis_gcd_unique  0 n n 1); auto.
   apply Zis_gcd_intro; auto.
-  exists 0; auto with zarith.
-  exists 1; auto with zarith.
+  exists 0; reflexivity.
+  exists 1; rewrite Z.mul_1_l; reflexivity.
 Qed.
 
 Theorem rel_prime_mod: forall p q, 0 < q ->
@@ -528,15 +545,16 @@ Proof.
   apply bezout_rel_prime.
   apply Bezout_intro with q1  (r1 + q1 * (p / q)).
   rewrite <- H2.
-  pattern p at 3; rewrite (Z_div_mod_eq p q); try ring; auto with zarith.
+  pattern p at 3; rewrite (Z_div_mod_eq p q); try ring.
+  now apply Z.lt_gt.
 Qed.
 
 Theorem rel_prime_mod_rev: forall p q, 0 < q ->
  rel_prime (p mod q) q -> rel_prime p q.
 Proof.
   intros p q H H0.
-  rewrite (Z_div_mod_eq p q); auto with zarith; red.
-  apply Zis_gcd_sym; apply Zis_gcd_for_euclid2; auto with zarith.
+  rewrite (Z_div_mod_eq p q) by now apply Z.lt_gt. red.
+  apply Zis_gcd_sym; apply Zis_gcd_for_euclid2; auto.
 Qed.
 
 Theorem Zrel_prime_neq_mod_0: forall a b, 1 < b -> rel_prime a b -> a mod b <> 0.
@@ -544,7 +562,8 @@ Proof.
   intros a b H H1 H2.
   case (not_rel_prime_0 _ H).
   rewrite <- H2.
-  apply rel_prime_mod; auto with zarith.
+  apply rel_prime_mod; auto.
+  now transitivity 1.
 Qed.
 
 (** * Primality *)
@@ -563,25 +582,56 @@ Proof.
   assert
     (a = - p \/ - p < a < -1 \/ a = -1 \/ a = 0 \/ a = 1 \/ 1 < a < p \/ a = p).
   { assert (Z.abs a <= Z.abs p) as H2.
-      apply Zdivide_bounds; [ assumption | omega ].
+      apply Zdivide_bounds; [ assumption | now intros -> ].
     revert H2.
     pattern (Z.abs a); apply Zabs_ind; pattern (Z.abs p); apply Zabs_ind;
-    intros; omega. }
+    intros H2 H3 H4.
+    - destruct (Zle_lt_or_eq _ _ H4) as [H5 | H5]; try intuition.
+      destruct (Zle_lt_or_eq _ _ (Z.ge_le _ _ H3)) as [H6 | H6]; try intuition.
+      destruct (Zle_lt_or_eq _ _ (Zlt_le_succ _ _ H6)) as [H7 | H7]; intuition.
+    - contradict H2; apply Zlt_not_le; apply Z.lt_trans with (2 := H); red; auto.
+    - destruct (Zle_lt_or_eq _ _ H4) as [H5 | H5].
+      + destruct (Zle_lt_or_eq _ _  H3) as [H6 | H6]; try intuition.
+        assert (H7 : a <= Z.pred 0) by (apply Z.lt_le_pred; auto).
+        destruct (Zle_lt_or_eq _ _ H7) as [H8 | H8]; intuition.
+        assert (- p < a < -1); try intuition.
+        now apply Z.opp_lt_mono; rewrite Z.opp_involutive.
+      + now left; rewrite <- H5, Z.opp_involutive.
+    - contradict H2.
+      apply Zlt_not_le; apply Z.lt_trans with (2 := H); red; auto.
+    }
   intuition idtac.
   (* -p < a < -1 *)
-  - absurd (rel_prime (- a) p); intuition.
-    inversion H2.
-    assert (- a | - a) by auto with zarith.
-    assert (- a | p) by auto with zarith.
-    apply H7, Z.divide_1_r in H8; intuition.
+  - absurd (rel_prime (- a) p).
+    + intros [H1p H2p H3p].
+      assert (- a | - a) by auto with zarith.
+      assert (- a | p) by auto with zarith.
+      apply H3p, Z.divide_1_r in H5; auto with zarith.
+      destruct H5.
+      * contradict H4; rewrite <- (Z.opp_involutive a), H5 .
+        apply Z.lt_irrefl.
+      * contradict H4; rewrite <- (Z.opp_involutive a), H5 .
+        discriminate.
+    + apply H0; split.
+      * now apply Z.opp_le_mono; rewrite Z.opp_involutive; apply Z.lt_le_incl.
+      * now apply Z.opp_lt_mono; rewrite Z.opp_involutive.
   (* a = 0 *)
-  - inversion H1. subst a; omega.
+  - contradict H.
+    replace p with 0; try discriminate.
+    now apply sym_equal, Z.divide_0_l; rewrite <-H2.
   (* 1 < a < p *)
-  - absurd (rel_prime a p); intuition.
-    inversion H2.
-    assert (a | a) by auto with zarith.
-    assert (a | p) by auto with zarith.
-    apply H7, Z.divide_1_r in H8; intuition.
+  - absurd (rel_prime a p).
+    + intros [H1p H2p H3p].
+      assert (a | a) by auto with zarith.
+      assert (a | p) by auto with zarith.
+      apply H3p, Z.divide_1_r in H5; auto with zarith.
+      destruct H5.
+      * contradict H3; rewrite <- (Z.opp_involutive a), H5 .
+        apply Z.lt_irrefl.
+      * contradict H3; rewrite <- (Z.opp_involutive a), H5 .
+        discriminate.
+    + apply H0; split; auto.
+      now apply Z.lt_le_incl.
 Qed.
 
 (** A prime number is relatively prime with any number it does not divide *)
@@ -605,12 +655,17 @@ Proof.
   intros a p Hp [H1 H2].
   apply rel_prime_sym; apply prime_rel_prime; auto.
   intros [q Hq]; subst a.
-  case (Z.le_gt_cases q 0); intros Hl.
-  absurd (q * p <= 0 * p); auto with zarith.
-  absurd (1 * p <= q * p); auto with zarith.
+  destruct Hp as [H3 H4].
+  contradict H2; apply Zle_not_lt.
+  rewrite <- (Z.mul_1_l p) at 1.
+  apply Zmult_le_compat_r.
+  - apply (Zlt_le_succ 0).
+    apply Zmult_lt_0_reg_r with p.
+    + apply Z.le_succ_l, Z.lt_le_incl; auto.
+    + now apply Z.le_succ_l.
+  - apply Z.lt_le_incl, Z.le_succ_l, Z.lt_le_incl; auto.
 Qed.
 
-
 (** If a prime [p] divides [ab] then it divides either [a] or [b] *)
 
 Lemma prime_mult :
@@ -623,38 +678,44 @@ Qed.
 
 Lemma not_prime_0: ~ prime 0.
 Proof.
-  intros H1; case (prime_divisors _ H1 2); auto with zarith.
+  intros H1; case (prime_divisors _ H1 2); auto with zarith; intuition; discriminate.
 Qed.
 
 Lemma not_prime_1: ~ prime 1.
 Proof.
-  intros H1; absurd (1 < 1); auto with zarith.
+  intros H1; absurd (1 < 1). discriminate.
   inversion H1; auto.
 Qed.
 
 Lemma prime_2: prime 2.
 Proof.
-  apply prime_intro; auto with zarith.
-  intros n (H,H'); Z.le_elim H; auto with zarith.
-  - contradict H'; auto with zarith.
-  - subst n. constructor; auto with zarith.
+  apply prime_intro.
+  - red; auto.
+  - intros n (H,H'); Z.le_elim H; auto with zarith.
+    + contradict H'; auto with zarith.
+      now apply Zle_not_lt, (Zlt_le_succ 1).
+    + subst n. constructor; auto with zarith.
 Qed.
 
 Theorem prime_3: prime 3.
 Proof.
   apply prime_intro; auto with zarith.
-  intros n (H,H'); Z.le_elim H; auto with zarith.
-  - replace n with 2 by omega.
-    constructor; auto with zarith.
-    intros x (q,Hq) (q',Hq').
-    exists (q' - q). ring_simplify. now rewrite <- Hq, <- Hq'.
-  - replace n with 1 by trivial.
-    constructor; auto with zarith.
+  - red; auto.
+  - intros n (H,H'); Z.le_elim H; auto with zarith.
+    + replace n with 2.
+      * constructor; auto with zarith.
+        intros x (q,Hq) (q',Hq').
+        exists (q' - q). ring_simplify. now rewrite <- Hq, <- Hq'.
+      * apply Z.le_antisymm.
+        ++ now apply (Zlt_le_succ 1).
+        ++ now apply (Z.lt_le_pred _ 3).
+     + replace n with 1 by trivial.
+       constructor; auto with zarith.
 Qed.
 
 Theorem prime_ge_2 p : prime p ->  2 <= p.
 Proof.
-  intros (Hp,_); auto with zarith.
+  now intros (Hp,_); apply (Zlt_le_succ 1).
 Qed.
 
 Definition prime' p := 1<p /\ (forall n, 1<n<p -> ~ (n|p)).
@@ -675,17 +736,24 @@ Proof.
     assert (Hx := Z.abs_nonneg x).
     set (y:=Z.abs x) in *; clearbody y; clear x; rename y into x.
     destruct (Z_0_1_more x Hx) as [->|[->|Hx']].
-    + exfalso. apply Z.divide_0_l in Hxn. omega.
+    + exfalso. apply Z.divide_0_l in Hxn.
+      absurd (1 <= n).
+      * rewrite Hxn; red; auto.
+      * intuition.
     + now exists 1.
     + elim (H x); auto.
       split; trivial.
-      apply Z.le_lt_trans with n; auto with zarith.
+      apply Z.le_lt_trans with n; try intuition.
       apply Z.divide_pos_le; auto with zarith.
+      apply Z.lt_le_trans with (2 := H0); red; auto.
   - (* prime' -> prime *)
     constructor; trivial. intros n Hn Hnp.
-    case (Zis_gcd_unique n p n 1); auto with zarith.
-    constructor; auto with zarith.
-    apply H; auto with zarith.
+    case (Zis_gcd_unique n p n 1).
+    + constructor; auto with zarith.
+    + apply H; auto with zarith.
+      now intuition; apply Z.lt_le_incl.
+    + intros H1; intuition; subst n; discriminate.
+    + intros H1; intuition; subst n; discriminate.
 Qed.
 
 Theorem square_not_prime: forall a, ~ prime (a * a).
@@ -698,7 +766,9 @@ Proof.
   assert (H' : 1 < a) by now apply (Z.square_lt_simpl_nonneg 1).
   apply (Ha' a).
   + split; trivial.
-    rewrite <- (Z.mul_1_l a) at 1. apply Z.mul_lt_mono_pos_r; omega.
+    rewrite <- (Z.mul_1_l a) at 1.
+    apply Z.mul_lt_mono_pos_r; auto.
+    apply Z.lt_trans with (2 := H'); red; auto.
   + exists a; auto.
 Qed.
 
@@ -709,10 +779,11 @@ Proof.
   assert (Hp: 0 < p); try apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith.
   assert (Hq: 0 < q); try apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith.
   case prime_divisors with (2 := H2); auto.
-  intros H4; contradict Hp; subst; auto with zarith.
-  intros [H4| [H4 | H4]]; subst; auto.
-  contradict H; auto; apply not_prime_1.
-  contradict Hp; auto with zarith.
+  - intros H4; contradict Hp; subst; discriminate.
+  - intros [H4| [H4 | H4]]; subst; auto.
+    + contradict H; auto; apply not_prime_1.
+    + contradict Hp; apply Zle_not_lt, (Z.opp_le_mono _ 0).
+      now rewrite Z.opp_involutive; apply Z.lt_le_incl.
 Qed.
 
 (** we now prove that [Z.gcd] is indeed a gcd in
@@ -748,6 +819,9 @@ Proof.
   apply Zgcd_is_gcd; auto.
   Z.le_elim H1.
   - generalize (Z.gcd_nonneg a b); auto with zarith.
+    intros H3 H4; contradict H3.
+    rewrite <- (Z.opp_involutive (Z.gcd a b)), <- H4.
+    now apply Zlt_not_le, Z.opp_lt_mono; rewrite Z.opp_involutive.
   - subst. now case (Z.gcd a b).
 Qed.
 
@@ -801,7 +875,8 @@ Proof.
   case (Zis_gcd_unique a b (Z.gcd a b) 1); auto.
   apply Zgcd_is_gcd.
   intros H2; absurd (0 <= Z.gcd a b); auto with zarith.
-  generalize (Z.gcd_nonneg a b); auto with zarith.
+  - rewrite H2; red; auto.
+  - generalize (Z.gcd_nonneg a b); auto with zarith.
 Qed.
 
 Definition rel_prime_dec: forall a b,
@@ -819,18 +894,25 @@ Definition prime_dec_aux:
 Proof.
   intros p m.
   case (Z_lt_dec 1 m); intros H1;
-   [ | left; intros; exfalso; omega ].
+   [ | left; intros; exfalso;
+       contradict H1; apply Z.lt_trans with n; intuition].
   pattern m; apply natlike_rec; auto with zarith.
-  left; intros; exfalso; omega.
-  intros x Hx IH; destruct IH as [F|E].
-  destruct (rel_prime_dec x p) as [Y|N].
-  left; intros n [HH1 HH2].
-  rewrite Z.lt_succ_r in HH2.
-  Z.le_elim HH2; subst; auto with zarith.
-  - case (Z_lt_dec 1 x); intros HH1.
-    * right; exists x; split; auto with zarith.
-    * left; intros n [HHH1 HHH2]; contradict HHH1; auto with zarith.
-  - right; destruct E as (n,((H0,H2),H3)); exists n; auto with zarith.
+  - left; intros; exfalso.
+    absurd (1 < 0); try discriminate.
+    apply Z.lt_trans with  n; intuition.
+  - intros x Hx IH; destruct IH as [F|E].
+    + destruct (rel_prime_dec x p) as [Y|N].
+      * left; intros n [HH1 HH2].
+        rewrite Z.lt_succ_r in HH2.
+        Z.le_elim HH2; subst; auto with zarith.
+      * case (Z_lt_dec 1 x); intros HH1.
+        -- right; exists x; split; auto with zarith.
+        -- left; intros n [HHH1 HHH2]; contradict HHH1; auto with zarith.
+           apply Zle_not_lt; apply Z.le_trans with x.
+           ++ now apply Zlt_succ_le.
+           ++ now apply Znot_gt_le; contradict HH1; apply Z.gt_lt.
+     + right; destruct E as (n,((H0,H2),H3)); exists n; auto with zarith.
+  - apply Z.le_trans with (2 := Z.lt_le_incl _ _ H1); discriminate.
 Defined.
 
 Definition prime_dec: forall p, { prime p }+{ ~ prime p }.
@@ -842,6 +924,7 @@ Proof.
       constructor; auto with zarith.
     * right; intros H3; inversion_clear H3 as [Hp1 Hp2].
       case H2; intros n [Hn1 Hn2]; case Hn2; auto with zarith.
+      now apply Hp2; intuition; apply Z.lt_le_incl.
   + right; intros H3; inversion_clear H3 as [Hp1 Hp2]; case H1; auto.
 Defined.
 
@@ -856,10 +939,15 @@ Proof.
     subst n; constructor; auto with zarith.
   - case H1; intros n (Hn1,Hn2).
     destruct (Z_0_1_more _ (Z.gcd_nonneg n p)) as [H|[H|H]].
-    + exfalso. apply Z.gcd_eq_0_l in H. omega.
+    + exfalso. apply Z.gcd_eq_0_l in H.
+      absurd (1 < n).
+      * rewrite H; discriminate.
+      * now intuition.
     + elim Hn2. red. rewrite <- H. apply Zgcd_is_gcd.
     + exists (Z.gcd n p); split; [ split; auto | apply Z.gcd_divide_r ].
       apply Z.le_lt_trans with n; auto with zarith.
-      apply Z.divide_pos_le; auto with zarith.
-      apply Z.gcd_divide_l.
+      * apply Z.divide_pos_le; auto with zarith.
+        -- apply Z.lt_trans with 1; intuition.
+        -- apply Z.gcd_divide_l.
+      * intuition.
 Qed.
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
index 66e246616f..e65eb7cdc7 100644
--- a/theories/ZArith/Zpow_facts.v
+++ b/theories/ZArith/Zpow_facts.v
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-Require Import ZArith_base ZArithRing Zcomplements Zdiv Znumtheory.
+Require Import ZArith_base ZArithRing Omega Zcomplements Zdiv Znumtheory.
 Require Export Zpower.
 Local Open Scope Z_scope.
 
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index f80d075b67..da8a9402dd 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-Require Import Wf_nat ZArith_base Omega Zcomplements.
+Require Import Wf_nat ZArith_base Zcomplements.
 Require Export Zpow_def.
 Local Open Scope Z_scope.
 
@@ -220,7 +220,8 @@ Section Powers_of_2.
 
   Lemma two_p_pred x : 0 <= x -> two_p (Z.pred x) < two_p x.
   Proof.
-   rewrite !two_p_equiv. intros. apply Z.pow_lt_mono_r; auto with zarith.
+   rewrite !two_p_equiv. intros. apply Z.pow_lt_mono_r; auto using Z.lt_pred_l.
+   reflexivity.
   Qed.
 
 End Powers_of_2.
@@ -265,17 +266,45 @@ Section power_div_with_rest.
     let '(q,r,d) := Pos.iter Zdiv_rest_aux (x, 0, 1) p in
     x = q * d + r /\ 0 <= r < d.
   Proof.
-   apply Pos.iter_invariant; [|omega].
-   intros ((q,r),d) (H,H'). unfold Zdiv_rest_aux.
-   destruct q as [ |[q|q| ]|[q|q| ]]; try omega.
+    apply Pos.iter_invariant; [|rewrite Z.mul_1_r, Z.add_0_r; repeat split; auto; discriminate].
+   intros ((q,r),d) (H,(H1',H2')). unfold Zdiv_rest_aux.
+   assert (H1 : 0 < d) by now apply Z.le_lt_trans with (1 := H1').
+   assert (H2 : 0 <= d + r) by now apply Z.add_nonneg_nonneg; auto; apply Z.lt_le_incl.
+   assert (H3 : d + r < 2 * d)
+     by now rewrite <-Z.add_diag; apply Zplus_lt_compat_l.
+   assert (H4 : r < 2 * d) by now
+     apply Z.lt_le_trans with (1 * d); [
+       rewrite Z.mul_1_l; auto |
+       apply Zmult_le_compat_r; try discriminate;
+       now apply Z.lt_le_incl].
+  destruct q as [ |[q|q| ]|[q|q| ]].
+   - repeat split; auto.
    - rewrite Pos2Z.inj_xI, Z.mul_add_distr_r in H.
-     rewrite Z.mul_shuffle3, Z.mul_assoc. omega.
+     rewrite Z.mul_shuffle3, Z.mul_assoc.
+     rewrite Z.mul_1_l in H; rewrite Z.add_assoc.
+     repeat split; auto with zarith.
    - rewrite Pos2Z.inj_xO in H.
-     rewrite Z.mul_shuffle3, Z.mul_assoc. omega.
+     rewrite Z.mul_shuffle3, Z.mul_assoc.
+     repeat split; auto.
+   - rewrite Z.mul_1_l in H; repeat split; auto.
    - rewrite Pos2Z.neg_xI, Z.mul_sub_distr_r in H.
-     rewrite Z.mul_sub_distr_r, Z.mul_shuffle3, Z.mul_assoc. omega.
+     rewrite Z.mul_sub_distr_r, Z.mul_shuffle3, Z.mul_assoc.
+     repeat split; auto.
+     rewrite !Z.mul_1_l, H, Z.add_assoc.
+     apply f_equal2 with (f := Z.add); auto.
+     rewrite <- Z.sub_sub_distr, <- !Z.add_diag, Z.add_simpl_r.
+     now rewrite Z.mul_1_l.
    - rewrite Pos2Z.neg_xO in H.
-     rewrite Z.mul_shuffle3, Z.mul_assoc. omega.
+     rewrite Z.mul_shuffle3, Z.mul_assoc.
+     repeat split; auto.
+   - repeat split; auto.
+     rewrite H, (Z.mul_opp_l 1), Z.mul_1_l, Z.add_assoc.
+     apply f_equal2 with (f := Z.add); auto.
+     rewrite Z.add_comm, <- Z.add_diag.
+     rewrite Z.mul_add_distr_l.
+     replace (-1 * d) with (-d).
+     + now rewrite Z.add_assoc, Z.add_opp_diag_r .
+     + now rewrite (Z.mul_opp_l 1), <-(Z.mul_opp_l 1).
   Qed.
 
   (** Old-style rich specification by proof of existence *)