proposition: Lemma lnXn n x : 0 < x -> ln (x ^+ n) = ln x *+ n.
proof: Proof. move=> x_gt0; elim: n => [|n ih] /=; first by rewrite expr0 ln1 mulr0n. by rewrite !exprS lnM ?qualifE//= ?exprn_gt0// mulrS ih. 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