proposition: Theorem Zpower_NR1 : forall (e : Z) (n : nat), (1 <= e)%Z -> (1 <= Zpower_nat e n)%Z.
proof: Proof. intros e n; elim n; simpl in |- *. auto with zarith. intros m H1 H2; rewrite <- (Zmult_1_l 1). apply Z.mul_le_mono_nonneg; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz