proposition: Lemma ln_idlt0_xgt1 x : 0 < x -> 1 < x -> ln_id x < 0.
proof: Proof. move=> x0 x1. rewrite /ln_id; apply/subR_lt0/exp_lt_inv. rewrite (exp_ln _ x0) -{1}(addR0 x) -(subRR 1) addRCA. have ? : x - 1 <> 0 by exact/eqP/gtR_eqF/subR_gt0. have ? : 0 < x - 1 by exact/subR_gt0. exact/exp_ineq1. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex