proposition: Theorem div_correct u (Y : I.type) tf tg f g : approximates Y tf f -> approximates Y tg g -> approximates Y (div u Y tf tg) (fun x => Xdiv (f x) (g x)).
proof: Proof. move: tf tg => [cf| |tf] [cg| |tg] Hf Hg; try exact: div_slow_correct. move=> Hne. move: Hf => /(_ Hne) [Hf|[yf Hyf1 /= Hyf2]]. left. now apply I.div_propagate_l. move: Hg => /(_ Hne)[Hg|[yg Hyg1 /= Hyg2]]. left. now apply I.div_propagate_r. right. exists (Xdiv yf yg); first exact: I.div_correct. by move=> x Hx; rewrite /= Hyf2 // Hyg2. intros Hne. move: Hg => /(_ Hne) [Hg|Hg]. apply TM_div_mixed_r_nai with (f := f) (1 := Hg). now apply get_tm_correct. apply: TM_div_mixed_r_correct_strong =>//. apply: TM_var_correct_strong =>//. - exact: J.subset_midpoint. - exact: J.contains_midpoint. - exact: Hf. move=> Hne. move: Hg => /(_ Hne) [Hg|Hg]. apply TM_div_mixed_r_nai with (f := f) (1 := Hg). now apply get_tm_correct. apply: TM_div_mixed_r_correct_strong =>//. now apply get_tm_correct. Qed.
imports: Coq(Reals ZArith Psatz) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq bigop) Interval Xreal Basic Interval_compl Datatypes Taylor_model_sharp Bound Bound_quad Univariate_sig