proposition: Lemma derive_pt_ln_id_xle1_ge0 x (Hx : 0 < x <= 1) : 0 < if x==1 then 1 else ln_id' Hx.
proof: Proof. case/boolP : (x == 1) => Hcase ; first lra. rewrite -derive_pt_ln_id_xle1; apply/subR_gt0. rewrite -invR1; apply ltR_inv => //; first by case: Hx. case (Rle_lt_or_eq_dec x 1) ; [apply Hx | by [] | ]. move/eqP in Hcase ; move => Habs. rewrite Habs in Hcase ; by contradict Hcase. Defined.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex