proposition: Lemma lnM : {in Num.pos &, {morph ln : x y / x * y >-> x + y}}.
proof: Proof. move=> x y x0 y0; apply: expR_inj; rewrite expRD !lnK//. by move: x0 y0; rewrite !qualifE; exact: mulr_gt0. 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