proposition: Theorem Zpower_NR0 : forall (e : Z) (n : nat), (0 <= e)%Z -> (0 <= Zpower_nat e n)%Z.
proof: Proof. intros e n; elim n; unfold Zpower_nat in |- *; simpl in |- *; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz