proposition: Lemma TM_div_mixed_r_nai M (x0 : R) (X : interval) a f g : I.convert a = Inan -> i_validTM x0 X M f -> i_validTM x0 X (TM_div_mixed_r M a) g.
proof: Proof. intros Ha [Hdef Hnai Hzero Hsubs Hmain]. rewrite /i_validTM /= I.div_propagate_r //. split=> //. destruct Hmain as [Q H1 H2]. exists (PolR.map (fun x => Rdiv x 0) Q) => //. apply: Pol.map_correct =>//. apply Rmult_0_l. intros xi x Hx. apply J.div_correct. exact Hx. now rewrite Ha. 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