proposition: Lemma exp_strict_lb (n : nat) x : 0 < x -> x ^ n * / (n`!)%:R < exp x.
proof: Proof. move=> xpos; by apply Rgt_lt, Rminus_gt, Rlt_gt, exp_dev_gt0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext