Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 4d6b7ebc authored by Guillaume Melquiond's avatar Guillaume Melquiond

Move Zpower_lt_Zpower to Fcore_Zaux.

parent 7afc5cc5
......@@ -340,6 +340,46 @@ destruct e1 as [|e1|e1] ; try easy.
apply Zpower_ge_0.
Qed.
Theorem Zpower_lt :
forall e1 e2, (0 <= e2)%Z -> (e1 < e2)%Z ->
(Zpower r e1 < Zpower r e2)%Z.
Proof.
intros e1 e2 He2 He.
destruct (Zle_or_lt 0 e1)%Z as [H1|H1].
replace e2 with (e2 - e1 + e1)%Z by ring.
rewrite <- Zmult_pow with (2 := H1).
rewrite Zmult_comm.
rewrite <- (Zmult_1_r (r ^ e1)) at 1.
apply Zmult_lt_compat2.
split.
now apply Zpower_gt_0.
apply Zle_refl.
split.
easy.
apply Zpower_gt_1.
clear -He ; omega.
apply Zle_minus_le_0.
now apply Zlt_le_weak.
revert H1.
clear -He2.
destruct e1 ; try easy.
intros _.
now apply Zpower_gt_0.
Qed.
Theorem Zpower_lt_Zpower :
forall e1 e2,
(Zpower r (e1 - 1) < Zpower r e2)%Z ->
(e1 <= e2)%Z.
Proof.
intros e1 e2 He.
apply Znot_gt_le.
intros H.
apply Zlt_not_le with (1 := He).
apply Zpower_le.
clear -H ; omega.
Qed.
End Zpower.
Section Div_Mod.
......
......@@ -872,28 +872,6 @@ ring_simplify (Zdigits n - 1 + 1).
apply Zdigits_correct.
Qed.
Theorem Zpower_lt_Zpower :
forall e1 e2,
(Zpower beta (e1 - 1) < Zpower beta e2)%Z ->
(e1 <= e2)%Z.
Proof.
intros e1 e2 He.
apply Znot_gt_le.
intros H.
apply Zlt_not_le with (1 := He).
destruct (Zle_or_lt 0 e2) as [He2|He2].
rewrite <- (Zmult_1_r (beta^ e2)).
replace (e1 - 1)%Z with (e2 + (e1 - 1 - e2))%Z by ring.
assert (0 <= e1 - 1 - e2)%Z by omega.
rewrite <- Zmult_pow by assumption.
apply Zmult_le_compat_l.
apply (Zlt_le_succ 0).
now apply Zpower_gt_0.
apply Zpower_ge_0.
replace (beta ^ e2)%Z with Z0 by now destruct e2.
apply Zpower_ge_0.
Qed.
Theorem Zdigits_slice :
forall n k l, (0 <= l)%Z ->
(Zdigits (Zslice n k l) <= l)%Z.
......@@ -902,7 +880,7 @@ intros n k l Hl.
unfold Zslice.
rewrite Zle_bool_true with (1 := Hl).
destruct (Zdigits_correct (Zscale n (- k) mod beta ^ l)) as (H1,H2).
apply Zpower_lt_Zpower.
apply Zpower_lt_Zpower with beta.
apply Zle_lt_trans with (1 := H1).
rewrite <- (Zabs_eq (beta ^ l)) at 2 by apply Zpower_ge_0.
apply ZOmod_lt.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment