From 959543f6f899f0384394f9770abbf17649f69b81 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 5 May 2011 15:13:04 +0000
Subject: BinInt: Z.add become the alternative Z.add'

 It relies on Z.pos_sub instead of a Pos.compare followed by Pos.sub.
 Proofs seem to be quite easy to adapt, via some rewrite Z.pos_sub_spec.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14107 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/QArith/Qpower.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories/QArith')

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;
-- 
cgit v1.2.3