1 files changed, 2 insertions, 2 deletions
diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v
index 188a74fdd..b05ee6495 100644
--- a/theories/QArith/Qpower.v
+++ b/theories/QArith/Qpower.v
@@ -136,9 +136,9 @@ Proof.
 intros a [|n|n] [|m|m] H; simpl; try ring;
 try rewrite Qpower_plus_positive;
 try apply Qinv_mult_distr; try reflexivity;
-case_eq ((n ?= m)%positive); intros H0; simpl;
+rewrite ?Z.pos_sub_spec;
+case Pos.compare_spec; intros H0; simpl; subst;
  try rewrite Qpower_minus_positive;
- try rewrite (Pcompare_Eq_eq _ _ H0);
  try (field; try split; apply Qpower_not_0_positive);
  try assumption;
  apply ZC2;