proposition: Lemma Rpower_mult_distr : forall x y z, 0 < x -> 0 < y -> Rpower x z * Rpower y z = Rpower (x * y) z.
proof: Proof. intros x y z x0 y0; unfold Rpower. rewrite <- exp_plus, ln_mult, Rmult_plus_distr_l; auto. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra