proposition: Lemma exp_ge_taylor (x : R) (n : nat) : 0 <= x -> sum_f_R0 (fun k => x^k / INR (fact k)) n <= exp x.
proof: Proof. move => Hx. rewrite /exp /exist_exp. case: Alembert_C3 => /= y Hy. apply Rnot_lt_le => H. apply Rminus_lt_0 in H. case: (Hy _ H) => N {} Hy. move: (Hy _ (MyNat.le_add_l N n)) => {Hy}. apply Rle_not_lt. apply Rle_trans with (2 := Rle_abs _). apply Rplus_le_compat_r. elim: N => [ | N IH]. rewrite Nat.add_0_r. apply Req_le. elim: (n) => {n H} [ | n /= <-]. apply Rmult_comm. apply f_equal. apply Rmult_comm. apply Rle_trans with (1 := IH). rewrite -plus_n_Sm. move: (n + N)%nat => {H N IH} n. rewrite /sum_f_R0 -/sum_f_R0. apply Rminus_le_0 ; ring_simplify. apply Rmult_le_pos. apply Rlt_le, Rinv_0_lt_compat, INR_fact_lt_0. by apply pow_le. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis