proposition: Lemma is_derive_n_atan n (x : R) : let q n := iteri n (fun i c => PolR.div_mixed_r tt (PolR.sub tt (PolR.add tt c^`() (PolR.lift 2 c^`())) (PolR.mul_mixed tt (INR (i.+1).*2) (PolR.lift 1 c))) (INR i.+2)) PolR.one in is_derive_n atan n x (if n is n.+1 then PolR.horner tt (q n) x / (1 + x²) ^ (n.+1) * INR (fact n.+1) else atan x)%R.
proof: Proof. move=> q; move: n x. help_is_derive_n_whole n x. - rewrite /Rdiv !Rsimpl. have := is_derive_atan x; exact: is_derive_ext. - set Q := (1 + x * x)%R. have HQ : Q <> 0%R by exact: Rsqr_plus1_neq0. have HQ' : (Q ^ n <> 0)%R by exact: pow_nonzero. have HQ'' : (Q * Q ^ n <> 0)%R. rewrite Rmult_comm -(Rmult_0_l (1 + x * x)). by apply:Rmult_neq_compat_r; try apply: pow_nonzero; exact: Rsqr_plus1_neq0. auto_derive; first split. + exact: PolR.ex_derive_horner. + by split. + rewrite Rmult_1_l PolR.Derive_horner [q n.+1]iteriS -/(q n). rewrite PolR.horner_div_mixed_r PolR.horner_sub PolR.horner_add. rewrite PolR.horner_mul_mixed !PolR.horner_lift. rewrite -{1}[in RHS](Rmult_1_r (q n)^`().[x]) -Rmult_plus_distr_l. have->: (x ^ 2 = x²)%R by simpl; rewrite Rmult_1_r. rewrite pow_1 /Rdiv. have H1 : (if n is _.+1 then (INR n + 1)%R else 1%R) = INR n.+1 by []. rewrite H1. rewrite !Rinv_mult_distr // -/pow -/Q. have->: INR (fact n + (n * fact n))%coq_nat = INR (fact n.+1) by []. rewrite [in RHS]fact_simpl mult_INR. set A := (((q n)^`()).[x] * Q - INR (n.+1).*2 * ((q n).[x] * x))%R. have->: (A * / INR n.+2 * (/ Q * (/ Q * / Q ^ n)) * (INR n.+2 * INR (fact n.+1)) = A * (/ INR n.+2 * INR n.+2) * (/ Q * (/ Q * / Q ^ n)) * INR (fact n.+1))%R by ring. rewrite Rinv_l; last exact: not_0_INR. rewrite /A !Rsimpl. rewrite -mul2n [INR (2 * _)%N]mult_INR; simpl (INR 2). field; by split. 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