proposition: Theorem power_le_mono : forall p q r : nat, 0 < r -> p <= q -> power r p <= power r q.
proof: Proof. intros p q r H; inversion H; auto with arith. repeat rewrite SO_power; auto with arith. intros H2; case ((proj1 (Nat.lt_eq_cases _ _)) H2); auto; intros H3. apply Nat.lt_le_incl; apply power_lt_mono; auto with arith. rewrite H3; auto. Qed.
imports: Coq(Arith ArithRing)