diff options
| -rw-r--r-- | theories/ZArith/Zpower.v | 47 |
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 *) |