proposition: Lemma is_derive_n_sin n (x : R) : is_derive_n sin n x (if odd n then (-1)^n./2 * cos x else ((-1)^n./2 * sin x)).
proof: Proof. rewrite -{1}(odd_double_half n); case: odd => /=. 2: rewrite -addnn; exact: is_derive_2n_sin. set n' := n./2. eapply is_derive_ext. move => /= {x} x. apply sym_eq, is_derive_n_unique. rewrite -addnn; apply: is_derive_2n_sin. apply is_derive_scal. 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