proposition: Theorem relative_error_N_FLX_round_ex : forall x, exists eps, (Rabs eps <= u_ro)%R /\ x = (round beta (FLX_exp prec) (Znearest choice) x * (1 + eps))%R.
proof: Proof. intro x; apply relative_error_N_round_ex_derive, relative_error_N_FLX'_ex. Qed.
imports: Coq(ZArith Reals Psatz) Core