proposition: Theorem power_lt_mono_inv2 : forall p q r : nat, 0 < q -> power r p < power r q -> p < q.
proof: Proof. intros p q r H1 H2; apply power_lt_mono_inv1 with (r := r); auto. generalize H1 H2; case r; simpl in |- *; auto with arith. case q; simpl in |- *; auto with arith. case p; simpl in |- *; auto with arith. Qed.
imports: Coq(Arith ArithRing)