proposition: Theorem relative_error_N_FLX_round : forall x, (Rabs (round beta (FLX_exp prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs(round beta (FLX_exp prec) (Znearest choice) x))%R.
proof: Proof. intro x. apply relative_error_le_conversion_round_inv, relative_error_N_FLX_round_ex. Qed.
imports: Coq(ZArith Reals Psatz) Core