proposition: Lemma expR0 : expR 0 = 1 :> R.
proof: Proof. apply: lim_near_cst => //. near=> m; rewrite -[m]prednK; last by near: m. rewrite -addn1 series_addn series_exp_coeff0 big_add1 big1 ?addr0//. by move=> i _; rewrite /exp_coeff /= expr0n mul0r. Unshelve. all: by end_near. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(boolp classical_sets functions) mathcomp(mathcomp_extra) reals ereal signed topology normedtype landau sequences derive realfun itv convex