proposition: Lemma exp_ineq1_le (x : R) : 1 + x <= exp x.
proof: Proof. destruct (Req_dec x 0) as [xeq|?]. - rewrite xeq, exp_0; lra. - left. now apply exp_ineq1. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra