proposition: Lemma cvg_sin_coeff' x : series (sin_coeff' x) @ \oo --> sin x.
proof: Proof. have /(@cvg_series_cvg_series_group _ _ 2) := @is_cvg_series_sin_coeff x. move=> /(_ isT); apply: cvg_trans. rewrite [X in _ --> series X @ \oo](_ : _ = (fun n => sin_coeff x n.*2.+1)). rewrite [X in series X @ \oo --> _](_ : _ = (fun n => sin_coeff x n.*2.+1)) //. by rewrite funeqE => n; exact: sin_coeff'E. rewrite funeqE=> n; rewrite /= 2!muln2 big_nat_recl //= sin_coeff_even add0r. by rewrite big_nat_recl // big_geq // addr0. 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