proposition: Lemma power_le : forall x n : nat, 0 < n -> x <= power x n.
proof: Proof. intros x n; case n; simpl in |- *; auto. intros H'; inversion H'. intros n'; case x; intros; auto. apply le_mult_right; auto. apply power_lt_O; auto with arith. Qed.
imports: Coq(Arith ArithRing)