proposition: Lemma error_fix_correct : forall prec mode emin, extension (Xerror_fix mode emin) (error_fix prec mode emin).
proof: Proof. unfold extension. intros. now apply error_fix_correct_aux. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval