proposition: Lemma cvg_cos_coeff' x : series (cos_coeff' x) @ \oo --> cos x.
proof: Proof. have /(@cvg_series_cvg_series_group _ _ 2) := @is_cvg_series_cos_coeff x. move=> /(_ isT); apply: cvg_trans. rewrite [X in _ --> series X @ \oo](_ : _ = (fun n => cos_coeff x n.*2)); last first. rewrite funeqE=> n; rewrite /= 2!muln2 big_nat_recr //= cos_coeff_odd addr0. by rewrite big_nat_recl//= /index_iota subnn big_nil addr0. rewrite [X in series X @ \oo --> _](_ : _ = (fun n => cos_coeff x n.*2)) //. by rewrite funeqE => n; exact: cos_coeff'E. 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