proposition: Lemma exp_lb x (n : nat) : 0 <= x -> x ^ n / (n`!)%:R <= exp x.
proof: Proof. move=> xpos; by apply Rge_le, Rminus_ge, Rle_ge, exp_dev_ge0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext