proposition: Lemma TM_div_mixed_r_correct M (b : I.type) (x0 : R) (X : interval) f (y : R) : b >: y -> i_validTM x0 X M f -> i_validTM x0 X (TM_div_mixed_r M b) (fun x => Xdiv (f x) (Xreal y)).
proof: Proof. have [->|Hy0] := Req_dec y R0. exact: TM_div_mixed_r_aux0. move=> Hy [Hdef Hnai Hzero Hsubs Hmain]. split=>//. move=> x Hx Dx; rewrite /TM_div_mixed_r /=. rewrite I.div_propagate_l //; apply/(Hdef x Hx). case: (f x) Dx => [|fx] //=. by rewrite /Xdiv' is_zero_false. by move=> HX; rewrite I.div_propagate_l // Hnai. have->: (Xreal 0) = (Xdiv (Xreal 0) (Xreal y)). by rewrite /Xdiv' /= is_zero_false // /Rdiv Rmult_0_l. exact: I.div_correct. have [q H1 H2] := Hmain. exists (PolR.map (Rdiv ^~ y) q). - apply: Pol.map_correct =>//. by rewrite /Rdiv Rmult_0_l. by move=> *; apply: J.div_correct. - move=> x Hx /=. move/(_ x Hx) in H2. case Df: (f x) => [|fx]. by rewrite I.div_propagate_l // (Hdef x Hx). clear - H2 Hy Hy0 Df Hdef Hx. rewrite PolR.horner_div_mixed_r /Xdiv' /Xbind2 is_zero_false // /proj_val. rewrite Df in H2. replace (fx / y - q.[x - x0] / y)%R with ((fx - q.[x - x0]) / y)%R by now field. exact: J.div_correct. 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