proposition: Lemma TM_inv_comp_correct (x0 : R) (X0 X : I.type) (TMf : rpa) f : contains (I.convert X0) (Xreal x0) -> forall n, i_validTM x0 (I.convert X) TMf f -> i_validTM x0 (I.convert X) (TM_inv_comp TMf X0 X n) (fun xr => Xinv (f xr)).
proof: Proof. move=> Ht n Hf. apply: TM_comp_correct=> //. have {Hf} [Hdef Hnai Hzero Hsubs Hmain] := Hf. move=> Y0 Y k HY HY0. exact: TM_inv_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