proposition: Lemma is_derive_n_cos n (x : R) : is_derive_n cos n x (if odd n then (-1)^(n./2) * - sin x else ((-1)^(n./2) * cos x)).
proof: Proof. rewrite -{1}(odd_double_half n); case: odd => /=. 2: rewrite -addnn; exact: is_derive_2n_cos. set n' := n./2. eapply is_derive_ext. move => /= {x} x. apply sym_eq, is_derive_n_unique. rewrite -addnn; apply: is_derive_2n_cos. apply is_derive_scal. apply is_derive_Reals, derivable_pt_lim_cos. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp