proposition: Lemma is_derive_n_tan n x : cos x <> 0%R -> let q n := iteri n (fun i c => PolR.div_mixed_r tt (PolR.add tt c^`() (PolR.lift 2 c^`())) (INR i.+1)) (PolR.lift 1 PolR.one) in is_derive_n tan n x ((q n).[tan x] * INR (fact n)).
proof: Proof. move=> Hx q; move: n x Hx. help_is_derive_n n x. - by move=> x Hx; rewrite /= !Rsimpl. - move=> Hx; auto_derive. + by eapply ex_derive_is_derive; apply: is_derive_tan. + rewrite !Rsimpl; rewrite (is_derive_unique _ _ _ (is_derive_tan _ Hx)). ring. - exact: (open_comp cos (fun y => y <> 0%R) (fun y _ => continuous_cos y) (open_neq 0%R)). - move=> x Hx. move En1 : n.+1 => n1. auto_derive; repeat split. + apply: PolR.ex_derive_horner. + by eapply ex_derive_is_derive; apply: is_derive_tan. + rewrite Rmult_1_l. rewrite (is_derive_unique _ _ _ (is_derive_tan _ Hx)). rewrite PolR.Derive_horner [q n1.+1]iteriS -/(q n1). rewrite PolR.horner_div_mixed_r PolR.horner_add. rewrite !PolR.horner_lift. rewrite fact_simpl mult_INR. set A := (((q n1)^`()).[tan x] + ((q n1)^`()).[tan x] * tan x ^ 2)%R. rewrite /Rdiv. have->: (A * / INR n1.+1 * (INR n1.+1 * INR (fact n1)) = A * INR (fact n1) * (/ INR n1.+1 * INR n1.+1))%R by ring. rewrite Rinv_l; last exact: not_0_INR. rewrite /A; ring. 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