proposition: Lemma Log_expR (a b : R) (n : nat) : 0 < a -> Log b (a ^ n) = n%:R * Log b a.
proof: Proof. by move=> a0; rewrite /Log ln_expR // mulRA. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext