proposition: Theorem sqrt_error_N_FLT_ex : forall x, generic_format beta (FLT_exp emin prec) x -> exists eps, (Rabs eps <= 1 - 1 / sqrt (1 + 2 * u_ro))%R /\ round beta (FLT_exp emin prec) (Znearest choice) (sqrt x) = (sqrt x * (1 + eps))%R.
proof: Proof. intros x Fx. assert (Heps := u_ro_pos). assert (Pb := om1ds1p2u_ro_pos). destruct (Rle_or_lt x 0) as [Nx|Px]. { exists 0%R; split; [now rewrite Rabs_R0|]. now rewrite (sqrt_neg x Nx), round_0, Rmult_0_l; [|apply valid_rnd_N]. } assert (Fx' := generic_format_FLX_FLT _ _ _ _ Fx). destruct (sqrt_error_N_FLX_ex _ Fx') as (d, (Bd, Hd)). exists d; split; [exact Bd|]; rewrite <-Hd; apply round_FLT_FLX. apply (Rle_trans _ (bpow (emin / 2)%Z)). { apply bpow_le, Z.div_le_lower_bound; lia. } apply (Rle_trans _ _ _ (sqrt_bpow_ge _ _)). rewrite Rabs_pos_eq; [|now apply sqrt_pos]; apply sqrt_le_1_alt. revert Fx; apply generic_format_ge_bpow; [|exact Px]. intro e; unfold FLT_exp; apply Z.le_max_r. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative Sterbenz Mult_error