proposition: Theorem pow_pos: forall p n, (0 < p)%nat -> (0 < pow p n)%nat.
proof: Proof. intros p1 n H; elim n; simpl; auto with arith. intros n1 H1; replace 0%nat with (p1 * 0)%nat; auto with arith. repeat rewrite (Nat.mul_comm p1); apply Nat.mul_lt_mono_pos_r; auto with arith. Qed.
imports: Arith