proposition: Lemma is_derive_2n_cos n x : is_derive_n cos (n + n) x ((-1)^n * cos x).
proof: Proof. elim: n x => [|n IHn] x. by rewrite /= Rmult_1_l. rewrite -addSnnS 2!addSn /=. apply is_derive_ext with (f := fun x => (-1)^n * -sin x). move => /= {x} x. apply sym_eq, is_derive_unique. eapply is_derive_ext. move => /= {x} x. apply sym_eq, is_derive_n_unique. apply IHn. apply is_derive_scal. apply is_derive_Reals, derivable_pt_lim_cos. replace (-1 * (-1)^n * cos x) with ((-1)^n * -cos x) by ring. apply is_derive_scal. apply: is_derive_opp. apply is_derive_Reals, derivable_pt_lim_sin. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp