proposition: Lemma pderivable_ln_id_xle1 : pderivable ln_id (fun x => 0 < x <= 1).
proof: Proof. rewrite /pderivable => x Hx. rewrite /ln_id. apply derivable_pt_plus. - apply derivable_pt_ln, Hx. - apply derivable_pt_opp, derivable_pt_minus; [apply derivable_pt_id | apply derivable_pt_cst]. Defined.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex