proposition: Lemma TM_div_correct (x0 : R) (X0 X : I.type) (TMf TMg : rpa) f g n : contains (I.convert X0) (Xreal x0) -> i_validTM x0 (I.convert X) TMf f -> i_validTM x0 (I.convert X) TMg g -> i_validTM x0 (I.convert X) (TM_div TMf TMg X0 X n) (fun xr => Xdiv (f xr) (g xr)).
proof: Proof. move=> Hne Hf Hg. apply: (TM_fun_eq (f := fun xr => Xmul (f xr) (Xinv (g xr)))). by move=> x; rewrite Xdiv_split. rewrite /TM_div. apply: TM_mul_correct =>//. exact: TM_inv_comp_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