proposition: Theorem Rpower_plus : forall x y z:R, Rpower z (x + y) = Rpower z x * Rpower z y.
proof: Proof. intros x y z; unfold Rpower. rewrite Rmult_plus_distr_r; rewrite exp_plus; auto. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra