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