proposition: Theorem relative_error_N_FLX'_ex : forall x, exists eps, (Rabs eps <= u_ro / (1 + u_ro))%R /\ round beta (FLX_exp prec) (Znearest choice) x = (x * (1 + eps))%R.
proof: Proof. Proof with auto with typeclass_instances. intros x. apply relative_error_le_conversion... { apply u_rod1pu_ro_pos. } now apply relative_error_N_FLX'. Qed.
imports: Coq(ZArith Reals Psatz) Core