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 acdbe8ff authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix proofs.

parent 084ef5ec
......@@ -260,7 +260,8 @@ unfold F2R; now simpl.
apply Zlt_le_trans with (4^1)%Z.
simpl; unfold Z.pow_pos; simpl; omega.
rewrite Hb.
apply Interval_missing.Zpower_le_exp_compat; omega.
apply (Zpower_le (Build_radix 4 eq_refl)).
now apply Zlt_le_weak.
apply Rle_lt_trans with (2:=Hx).
replace (sqrt (Z2R beta)) with 2%R.
now right.
......@@ -1000,7 +1001,8 @@ simpl; split.
unfold F2R; simpl; ring.
rewrite H; apply Zlt_le_trans with (4^1)%Z.
simpl; unfold Z.pow_pos; simpl; omega.
apply Interval_missing.Zpower_le_exp_compat; omega.
apply (Zpower_le (Build_radix 4 eq_refl)).
now apply Zlt_le_weak.
(* ... *)
apply Rle_trans with (x-Z2R 0 * ulp_flx x).
right; simpl; ring.
......
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