proposition: Lemma ln_Rpower : forall x y:R, ln (Rpower x y) = y * ln x.
proof: Proof. intros x y. unfold Rpower. rewrite (ln_exp (y * ln x)). reflexivity. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra