proposition: Lemma error_fix_correct_aux : forall prec mode emin xi x, contains (convert xi) x -> contains (convert (error_fix prec mode emin xi)) (Xerror_fix mode emin x) /\ contains (convert (error_fix prec mode emin xi)) (Xreal 0).
proof: Proof. intros prec mode emin [|xl xu] [|xr]; try easy; [now unfold convert; case (_ && _)|]. intros _. cbn -[error_aux]. refine (_ (error_aux_correct_aux prec mode (FIX.FIX_exp emin) emin xr _ _)). now destruct error_aux. rewrite FIX.ulp_FIX. apply Rle_refl. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval