proposition: Lemma TM_mul_mixed_correct_strong (a : I.type) M (x0 : R) (X : interval) f g : is_const f X (I.convert a) -> i_validTM x0 X M g -> i_validTM x0 X (TM_mul_mixed a M) (fun x => Xmul (f x) (g x)).
proof: Proof. move=> [[|y] Hy1 Hy2] Hg. - apply TM_mul_mixed_nai with (2 := Hg). now apply contains_Xnan. - apply: TM_fun_eq; last exact: TM_mul_mixed_correct Hy1 Hg. move=> x Hx /=. by rewrite Hy2. Qed.
imports: Coq(ZArith Psatz Reals) Flocq(Raux) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp Coquelicot Xreal Interval Basic Xreal_derive Interval_compl Datatypes Taylor_poly Basic_rec Bound