proposition: Theorem relative_error_FLX : forall x, (x <> 0)%R -> (Rabs (round beta (FLX_exp prec) rnd x - x) < bpow (-prec + 1) * Rabs x)%R.
proof: Proof. Proof with auto with typeclass_instances. intros x Hx. destruct (mag beta x) as (ex, He). specialize (He Hx). apply relative_error with (ex - 1)%Z... intros k _. apply relative_error_FLX_aux. apply He. Qed.
imports: Coq(ZArith Reals Psatz) Core