proposition: Lemma ln_expR (a : R) (n : nat) : 0 < a -> ln (a ^ n) = n%:R * ln a.
proof: Proof. move=> a0; elim: n => [|n IH]; first by rewrite expR0 ln_1 mul0R. rewrite expRS ln_mult //; last exact: expR_gt0. by rewrite IH S_INR mulRDl mul1R addRC. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext