proposition: Theorem relative_error_N_FLT_round : forall x, (bpow (emin + prec - 1) <= Rabs x)%R -> (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs (round beta (FLT_exp emin prec) (Znearest choice) x))%R.
proof: Proof. Proof with auto with typeclass_instances. intros x Hx. apply relative_error_N_round with (emin + prec - 1)%Z... apply relative_error_FLT_aux. Qed.
imports: Coq(ZArith Reals Psatz) Core