proposition: Lemma ln_idgt0 x : 0 < x -> ln_id x <= 0.
proof: Proof. case: (ltgtP x 1) => [| |] x1 x0. - by apply/ltRW/ln_idlt0_xlt1; split=> //; apply/RltP. - by apply/ltRW/ln_idlt0_xgt1 => //; exact/RltP. - rewrite x1 /ln_id ln_1 2!subRR. by apply/RleP; rewrite lexx. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex