Zdiv: do not use “omega”

2 files changed, 49 insertions, 26 deletions

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 39482dde6c..57b96cad18 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -12,7 +12,7 @@ Require Import ZArith_base.
 Require Import ZArithRing.
 Require Import Zcomplements.
 Require Import Zdiv.
-Import Omega.
+Require Import Omega.
 Require Import Wf_nat.
 
 (** For compatibility reasons, this Open Scope isn't local as it should *)