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