proposition: Theorem Fsqrt_correct : forall x, (0 < F2R x)%R -> let '(m, e, l) := Fsqrt x in (e <= cexp beta fexp (sqrt (F2R x)))%Z /\ inbetween_float beta m e (sqrt (F2R x)) l.
proof: Proof. intros [m1 e1] Hm1. apply gt_0_F2R in Hm1. unfold Fsqrt. set (e := Z.min _ _). assert (2 * e <= e1)%Z as He. { assert (e <= Z.div2 e1)%Z by apply Z.le_min_r. rewrite (Zdiv2_odd_eqn e1). destruct Z.odd ; lia. } generalize (Fsqrt_core_correct m1 e1 e Hm1 He). destruct Fsqrt_core as [m l]. apply conj. apply Z.le_trans with (1 := Z.le_min_l _ _). unfold cexp. rewrite (mag_sqrt_F2R m1 e1 Hm1). apply Z.le_refl. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Digits Generic_fmt Float_prop Bracket