proposition: Theorem Rpower_Ropp : forall x y:R, Rpower x (- y) = / (Rpower x y).
proof: Proof. unfold Rpower. intros x y; rewrite Ropp_mult_distr_l_reverse. apply exp_Ropp. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra