proposition: Lemma expR_ge1Dx x : 0 <= x -> 1 + x <= expR x.
proof: Proof. move=> x_gt0; rewrite /expR. pose f (x : R) i := (i == 0%nat)%:R + x *+ (i == 1%nat). have F n : (1 < n)%nat -> \sum_(0 <= i < n) (f x i) = 1 + x. move=> /subnK<-. by rewrite addn2 !big_nat_recl //= /f /= mulr1n !mulr0n big1 ?add0r ?addr0. have -> : 1 + x = limn (series (f x)). by apply/esym/lim_near_cst => //; near=> n; apply: F; near: n. apply: ler_lim; first by apply: is_cvg_near_cst; near=> n; apply: F; near: n. exact: is_cvg_series_exp_coeff. by near=> n; apply: ler_sum => -[|[|i]] _; rewrite /f /exp_coeff /= !(mulr0n, mulr1n, expr0, expr1, divr1, addr0, add0r) // exp_coeff_ge0. 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