proposition: Lemma log_id_cmp x : 0 < x -> log x <= (x - 1) * log (exp 1).
proof: Proof. by move=> x0; rewrite logexp1E; apply leR_wpmul2r; [exact/invR_ge0 | exact/ln_id_cmp]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex