proposition: Lemma TM_inv_correct (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_inv X0 X n) Xinv'.
proof: Proof. move=> Hsubset Hex. rewrite /TM_inv /=. case E0: apart0. apply i_validTM_Ztech with (TR.T_inv tt); last 2 first =>//. exact: I.inv_correct. constructor. - by move=> {n} ? n; rewrite PolR.size_rec1. - { move=> {X0 n Hsubset Hex} x n k Hx Hkn. rewrite (Derive_n_ext_loc _ Rinv); last first. apply: (locally_open (fun t => t <> 0)%R); [exact: open_neq| |exact: apart0_correct E0]. by move=> y Hy; rewrite /Xinv' is_zero_false. rewrite /PolR.nth; elim: k Hkn => [|k IHk] Hkn. by rewrite rec1up_co0 /= Rdiv_1. rewrite nth_rec1up ifF; last by apply: negbTE; rewrite ltnNge Hkn. move/(_ (ltnW Hkn)) in IHk. rewrite nth_rec1up ifF in IHk; last by apply: negbTE; rewrite ltnNge ltnW. rewrite iteriS IHk /TR.inv_rec. have neq0_x : (x <> 0)%R by move/(apart0_correct Hx) in E0. rewrite !(is_derive_n_unique _ _ _ _ (is_derive_n_inv _ _ neq0_x)). rewrite big_ord_recr. set big := \big[Rmult/1%R]_(i < k) _. try simpl (Rmul_monoid _). rewrite /Rdiv !Rmult_assoc; congr Rmult. rewrite fact_simpl mult_INR. rewrite !add1n -[(x ^ k.+2)%R]/(x * x ^ k.+1)%R. set Xk1 := (x ^ k.+1)%R. set k_ := INR (fact k). set k1 := INR k.+1. rewrite Rinv_mult_distr //; last exact: pow_nonzero. rewrite Rinv_mult_distr; try solve [exact: INR_fact_neq_0|exact: not_0_INR]. rewrite !Rmult_assoc -Ropp_inv_permute //. have->: (- k1 * (/ x * (/ Xk1 * (/ k1 * / k_))))%R = ((k1 * / k1) * - (/ x * (/ Xk1 * (/ k_))))%R by ring. rewrite Rinv_r; last exact: not_0_INR. ring. } constructor. - by move=> {n} ? ? n; rewrite PolR.size_rec1 Pol.size_rec1. - { move=> {X0 n Hsubset Hex} X1 x1 n Hx0. apply: Pol.rec1_correct; last exact: J.inv_correct. move=> ai a m Ha; apply: J.div_correct =>//. exact: J.neg_correct. } - { move=> {X0 n Hsubset Hex} Y x Hx Dx n k Hk. apply/Pol.rec1_propagate =>//. - move=> q m Hqm; apply/contains_Xnan; rewrite /inv_rec. by rewrite I.div_propagate_l. - apply/contains_Xnan. rewrite -Dx. exact: (I.inv_correct _ _ (Xreal x)). - by rewrite Pol.size_rec1. } - { move=> {X0 n Hsubset Hex} n x Hx. move/(apart0_correct Hx) in E0. apply: (ex_derive_n_ext_loc Rinv). apply: (locally_open (fun t => t <> 0)%R) =>//. exact: open_neq. by simpl=> y Hy; rewrite /Xinv' is_zero_false. exact: ex_derive_n_is_derive_n (is_derive_n_inv n x E0). } split =>//. by move=> *; rewrite I.nai_correct. by move=> Hx; rewrite /= I.nai_correct. by rewrite I.nai_correct. exact: Hsubset. exists (TR.T_inv tt x0 n). apply: Pol.rec1_correct. by move=> *; repeat first [apply: J.div_correct |apply: J.inv_correct |apply: J.neg_correct ]. exact: J.inv_correct. by 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