proposition: Theorem Rpower_1 : forall x:R, 0 < x -> Rpower x 1 = x.
proof: Proof. intros x H; unfold Rpower. rewrite Rmult_1_l; apply exp_ln; apply H. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra