Zpower: do not use “omega”

1 files changed, 38 insertions, 9 deletions

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 *)