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