proposition: Lemma error_fix_contains_0 : forall prec mode emin x, not_empty (convert x) -> contains (convert (error_fix prec mode emin x)) (Xreal 0).
proof: Proof. intros prec mode emin x [v Hv]. unfold error_fix. assert (H := fun emin => proj2 (error_fix_correct_aux prec mode emin _ _ Hv)). destruct mode ; apply H. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval