proposition: Lemma series_sin_coeff0 n : series (sin_coeff 0) n.+1 = 0.
proof: Proof. rewrite /series /= big_nat_recl //= /sin_coeff /= expr0n divr1 !mulr1. by rewrite big1 ?addr0 // => i _; rewrite expr0n !(mul0r, mulr0). 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