proposition: Lemma error_flt_correct : forall prec mode emin p, extension (Xerror_flt mode emin p) (error_flt prec mode emin p).
proof: Proof. unfold extension. intros. now apply error_flt_correct_aux. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval