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