proposition: Theorem power_lt_mono_inv1 : forall p q r : nat, 0 < r -> power r p < power r q -> p < q.
proof: Proof. intros p q r Hr H; case (Nat.le_gt_cases q p); auto; intros H1. contradict H; auto with arith. apply Nat.le_ngt; apply power_le_mono; auto with arith. Qed.
imports: Coq(Arith ArithRing)