proposition: Theorem Rpower_mult : forall x y z:R, Rpower (Rpower x y) z = Rpower x (y * z).
proof: Proof. intros x y z; unfold Rpower. rewrite ln_exp. replace (z * (y * ln x)) with (y * z * ln x). - reflexivity. - ring. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra