proposition: Theorem powerRZ_Zs : forall (e : R) (n : Z), e <> 0%R -> powerRZ e (Z.succ n) = (e * powerRZ e n)%R.
proof: Proof. intros e n H'0. replace (Z.succ n) with (n + Z.succ 0)%Z. rewrite powerRZ_add; auto. rewrite powerRZ_1. rewrite Rmult_comm; auto. auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz