proposition: Lemma ln_powR a x : ln (a `^ x) = x * ln a.
proof: Proof. have [->|x0] := eqVneq x 0; first by rewrite powRr0 ln1// mul0r. have [->|a0] := eqVneq a 0; first by rewrite powR0// ln0// mulr0. by rewrite /powR (negbTE a0) expRK. 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