proposition: Lemma sin_coeff_even n x : sin_coeff x n.*2 = 0.
proof: Proof. by rewrite /sin_coeff /= odd_double /= !mul0r. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) reals ereal nsatz_realtype signed topology normedtype landau sequences derive realfun exp