proposition: Lemma derive_xlnx_aux2 x (x_pos : 0 < x) : derive_pt xlnx x (derivable_pt_xlnx x_pos) = ln x + 1.
proof: Proof. rewrite derive_xlnx_aux1 /f derive_pt_mult derive_pt_ln. rewrite mulRV ?gtR_eqF //. rewrite (_ : derive_pt ssrfun.id x (derivable_id x) = 1) ; first by rewrite mul1R. by rewrite -(derive_pt_id x); apply proof_derive_irrelevance. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex