proposition: Theorem Zpower_nat_anti_monotone_lt : forall p q : nat, (Zpower_nat n p < Zpower_nat n q)%Z -> p < q.
proof: Proof. intros p q H'. case (Nat.le_gt_cases q p); auto; (intros H'1; generalize H'; case H'1). intros H'0; contradict H'0; auto with zarith. intros m H'0 H'2; contradict H'2; auto with zarith. apply Zle_not_lt, Zlt_le_weak, Zpower_nat_monotone_lt; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz