proposition: Lemma lnK : {in Num.pos, cancel ln exp}.
proof: Proof. move=> x; rewrite qualifE => x_gt0. rewrite /ln; case: xgetP=> [x1 _ /eqP// |H]. by case: (expR_total x_gt0) => y /eqP Hy; case: (H y). Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(boolp classical_sets functions) mathcomp(mathcomp_extra) reals ereal signed topology normedtype landau sequences derive realfun itv convex