proposition: Lemma error_fix_propagate : forall prec mode emin, propagate (I.error_fix prec mode emin).
proof: Proof. intros prec mode emin. apply propagate_extension with (1 := I.error_fix_correct prec mode emin). Qed.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic