proposition: Theorem Zpower_nat_monotone_lt : forall p q : nat, p < q -> (Zpower_nat n p < Zpower_nat n q)%Z.
proof: Proof. intros p q H'; elim H'; simpl in |- *; auto. apply Zpower_nat_monotone_S. intros m H H0; apply Z.lt_trans with (1 := H0). apply Zpower_nat_monotone_S. Qed.
imports: Reals ZArith List PeanoNat Psatz