proposition: Lemma derive_xlnx_aux1 x (x_pos : 0 < x) : derive_pt xlnx x (derivable_pt_xlnx x_pos) = derive_pt xlnx_total x (derivable_xlnx_total x_pos).
proof: Proof. by rewrite -derive_pt_f_eq_g. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex