proposition: Lemma mul_0_contains_0_r y Y X : contains (I.convert Y) y -> contains (I.convert X) (Xreal 0) -> contains (I.convert (I.mul prec Y X)) (Xreal 0).
proof: Proof. move=> Hy H0. have Hy0 ry : (Xreal 0) = (Xreal ry * Xreal 0)%XR by rewrite /= Rmult_0_r. case: y Hy => [|ry] Hy; [rewrite (Hy0 0%R)|rewrite (Hy0 ry)]; apply: I.mul_correct=>//. by case: (I.convert Y) Hy. Qed.
imports: Coq(ZArith Reals Psatz) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat bigop) Coquelicot(Coquelicot) Stdlib MathComp Xreal Interval Taylor