proposition: Theorem Zpower_nat_monotone_le : forall p q : nat, p <= q -> (Zpower_nat n p <= Zpower_nat n q)%Z.
proof: Proof. intros p q H'; case (proj1 (Nat.lt_eq_cases _ _) H'); auto with zarith. intros H1; apply Zlt_le_weak, Zpower_nat_monotone_lt; auto with zarith. intros H1; rewrite H1; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz