proposition: Lemma mul_0_contains_0_l y Y X : contains (I.convert Y) y -> contains (I.convert X) (Xreal 0) -> contains (I.convert (I.mul prec X Y)) (Xreal 0).
proof: Proof. move=> Hy H0. have H0y ry : (Xreal 0) = (Xreal 0 * Xreal ry)%XR by rewrite /= Rmult_0_l. case: y Hy => [|ry] Hy; [rewrite (H0y 0%R)|rewrite (H0y 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