proposition: Lemma TM_div_mixed_r_aux0 M (b : I.type) (x0 : R) (X : interval) f : b >: 0%R -> i_validTM x0 X M f -> i_validTM x0 X (TM_div_mixed_r M b) (fun x => Xdiv (f x) (Xreal 0)).
proof: Proof. move=> Hb0 [Hdef Hnai Hzero Hsubs /= Hmain]. have Lem : contains (I.convert (error (TM_div_mixed_r M b))) Xnan. rewrite /TM_div_mixed_r. simpl. rewrite -(Xdiv_0_r (Xreal R0)). exact: I.div_correct. split=>//. by move=> x Hx Dx; apply/contains_Xnan. by rewrite (proj1 (contains_Xnan _) Lem). by rewrite (proj1 (contains_Xnan _) Lem). have [Q Happrox Herr] := Hmain. exists (PolR.map (Rdiv^~ 0)%R Q) =>/=. apply: Pol.map_correct =>//; first by rewrite /Rdiv Rmult_0_l. move=> *; exact: J.div_correct. by move=> x Hx; move/contains_Xnan: Lem ->. 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