proposition: Theorem Zpower_nat_monotone_S : forall p : nat, (Zpower_nat n p < Zpower_nat n (S p))%Z.
proof: Proof. intros p; rewrite <- (Zmult_1_l (Zpower_nat n p)); replace (S p) with (1 + p); [ rewrite Zpower_nat_is_exp | auto with zarith ]. rewrite Zpower_nat_1; auto with zarith. apply Zmult_gt_0_lt_compat_r; auto with zarith. apply Z.lt_gt; auto with zarith. apply Zpower_nat_less. Qed.
imports: Reals ZArith List PeanoNat Psatz