proposition: Theorem sqrt_error_N_FLX_ex x (Fx : format x) : exists eps, (Rabs eps <= 1 - 1 / sqrt (1 + 2 * u_ro))%R /\ round beta (FLX_exp prec) (Znearest choice) (sqrt x) = (sqrt x * (1 + eps))%R.
proof: Proof. now apply relative_error_le_conversion; [apply valid_rnd_N|apply om1ds1p2u_ro_pos|apply sqrt_error_N_FLX]. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative Sterbenz Mult_error