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

Added sqrt_ge_0.

parent d7510700
......@@ -130,6 +130,17 @@ rewrite H.
apply Rle_refl.
Qed.
Theorem sqrt_ge_0 :
forall x : R,
(0 <= sqrt x)%R.
Proof.
intros x.
unfold sqrt.
destruct (Rcase_abs x) as [_|H].
apply Rle_refl.
apply Rsqrt_positivity.
Qed.
End Rmissing.
Section Zmissing.
......
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