Znumtheory: do not use “omega”

2 files changed, 213 insertions, 127 deletions

diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 57b96cad18..01365135c5 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -12,7 +12,6 @@ Require Import ZArith_base.
 Require Import ZArithRing.
 Require Import Zcomplements.
 Require Import Zdiv.
-Require Import Omega.
 Require Import Wf_nat.
 
 (** For compatibility reasons, this Open Scope isn't local as it should *)
@@ -118,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,
@@ -140,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.
 
@@ -170,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). *)
@@ -301,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.
@@ -326,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.
@@ -434,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. *)
@@ -458,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.
@@ -505,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 ->
@@ -529,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.
@@ -545,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 *)
@@ -564,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 *)
@@ -606,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 :
@@ -624,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)).
@@ -676,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).
@@ -699,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.
 
@@ -710,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
@@ -749,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.
 
@@ -802,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,
@@ -820,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 }.
@@ -843,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.
 
@@ -857,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 8ba511940e..e65eb7cdc7 100644
--- a/theories/ZArith/Zpow_facts.v
+++ b/theories/ZArith/Zpow_facts.v
@@ -8,8 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-Require Import ZArith_base ZArithRing Zcomplements Zdiv Znumtheory.
-Import Omega.
+Require Import ZArith_base ZArithRing Omega Zcomplements Zdiv Znumtheory.
 Require Export Zpower.
 Local Open Scope Z_scope.