proposition: Theorem power_lt_mono : forall p q r : nat, 1 < r -> p < q -> power r p < power r q.
proof: Proof. intros p q r H H0; elim H0; simpl in |- *; intros; auto with arith; pattern (power r p) at 1 in |- *; replace (power r p) with (1 * power r p); auto with arith. repeat rewrite (fun x y z => Nat.mul_comm x (power y z)); auto with arith. apply mult_lt_bis; auto with arith. apply power_lt_O; auto with arith. apply lt_mult_right; auto with arith. Qed.
imports: Coq(Arith ArithRing)