proposition: Lemma cos0 : cos 0 = 1.
proof: Proof. apply: lim_near_cst => //; near=> m; rewrite -[m]prednK; last by near: m. rewrite -addn1 series_addn series_cos_coeff0 big_add1 big1 ?addr0//. by move=> i _; rewrite /cos_coeff /= expr0n !(mulr0, mul0r). Unshelve. all: by end_near. 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