proposition: Lemma TM_power_int_correct (p : Z) (x0 : R) (X0 X : I.type) n : subset' (I.convert X0) (I.convert X) -> contains (I.convert X0) (Xreal x0) -> i_validTM x0 (I.convert X) (TM_power_int p X0 X n) (fun x => Xpower_int' x p).
proof: Proof. move=> Hsubs Hnex. rewrite /TM_power_int. case Ep: p => [|p'|p']; last case E0: apart0; try apply: TM_power_int_correct_aux; intuition. constructor =>//. by move=> *; rewrite I.nai_correct. by move=> Hx; rewrite /= I.nai_correct. by rewrite I.nai_correct. exact: Hsubs. exists (TR.T_power_int tt (Z.neg p') x0 n). apply: Pol.dotmuldiv_correct. by rewrite size_falling_seq size_fact_seq. apply: Pol.rec1_correct. rewrite /pow_aux_rec /TR.pow_aux_rec -Ep. move=> ai a m Ha. case: ((p <? 0) || (p >=? Z.of_nat m))%Z. exact: J.power_int_correct. apply I.mask_correct', J.zero_correct. exact: J.power_int_correct. by move=> x Hx; rewrite I.nai_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