proposition: Theorem sqrt_correct : forall x : float beta, round beta fexp rnd (R_sqrt.sqrt (F2R x)) = F2R (sqrt x).
proof: Proof. intros x. unfold sqrt. case Zlt_bool_spec ; intros Hm. generalize (Fsqrt_correct fexp x (F2R_gt_0 _ _ Hm)). destruct Fsqrt as [[m' e'] l]. intros [Hs1 Hs2]. rewrite (round_trunc_sign_any_correct' beta fexp rnd choice rnd_choice _ m' e' l). destruct truncate as [[m'' e''] l']. now rewrite Rlt_bool_false by apply sqrt_ge_0. now rewrite Rabs_pos_eq by apply sqrt_ge_0. now left. destruct (Req_dec (F2R x) 0) as [Hz|Hz]. rewrite Hz, sqrt_0, F2R_0. now apply round_0. unfold R_sqrt.sqrt. destruct Rcase_abs as [H|H]. rewrite F2R_0. now apply round_0. destruct H as [H|H]. elim Rgt_not_le with (1 := H). now apply F2R_le_0. now elim Hz. Qed.
imports: Coq(ZArith Reals) Flocq(Core Bracket Round Operations Div Sqrt)