proposition: Lemma log_id_eq x : 0 < x -> log x = (x - 1) * log (exp 1) -> x = 1.
proof: Proof. move=> Hx'; rewrite logexp1E. rewrite eqR_mul2r; last exact/nesym/eqP/ltR_eqF/invR_gt0. apply ln_id_eq; by [apply Hx' | apply Hx]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex