proposition: Theorem power_le_mono_inv : forall p q r : nat, 1 < r -> power r p <= power r q -> p <= q.
proof: Proof. intros p q r H H0; case (Nat.le_gt_cases p q); auto; intros H1. contradict H0; auto with arith. apply Nat.lt_nge; apply power_lt_mono; auto with arith. Qed.
imports: Coq(Arith ArithRing)