proposition: Lemma ln_id_eq x : 0 < x -> ln x = x - 1 -> x = 1.
proof: Proof. move=> Hx' Hx. case (total_order_T x 1) => [ [] // Hx2 | Hx2]; contradict Hx. - apply/eqP/ltR_eqF; rewrite -subR_lt0. apply ln_idlt0_xlt1; split; [exact Hx' | exact Hx2]. - by apply/eqP/ltR_eqF; rewrite -subR_lt0; exact: ln_idlt0_xgt1. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex