proposition: Lemma integral_interval_mul_zero : forall prec a ia f fi g Ig Igi, (0 < a) -> contains (I.convert ia) (Xreal a) -> (forall x, 0 <= x <= a -> contains (I.convert fi) (Xreal (f x))) -> I.bounded fi -> (forall x, 0 <= x <= a -> continuous f x) -> (forall x, 0 < x <= a -> continuous g x) -> constant_sign (fun x => 0 < x <= a) g -> is_RInt_gen g (at_right 0) (at_point a) Ig -> contains (I.convert Igi) (Xreal Ig) -> exists Ifg, is_RInt_gen (fun t => f t * g t) (at_right 0) (at_point a) Ifg /\ contains (I.convert (I.mul prec fi Igi)) (Xreal Ifg).
proof: Proof. move => prec a ia f fi g Ig Igi H0a Hia Hf Hfi Cf Cg Hg HIg HIg'. apply: (integral_interval_mul_sing) => // ; last exact: HIg'; last exact: HIg. exact: Hia. Qed.
imports: Coq(Reals List Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool) Stdlib Coquelicot Xreal Interval Taylor_model Interval_compl