proposition: Lemma ln_id_cmp x : 0 < x -> ln x <= x - 1.
proof: Proof. by move=> Hx; apply Rminus_le; apply ln_idgt0; exact Hx. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex