proposition: Lemma ltRinve1 : exp (-1) < 1.
proof: Proof. rewrite -[X in _ < X]exp_0. apply exp_increasing. lra. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext