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

1 files changed, 6 insertions, 4 deletions

diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 1eee8d852..c0cd78649 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -557,6 +557,7 @@ Proof.
 (* POS/POS *)
   rewrite Pplus_plus; auto with real.
 (* POS/NEG *)
+  rewrite Z.pos_sub_spec.
   case Pcompare_spec; intros; simpl.
   subst; auto with real.
   rewrite Pminus_minus by trivial.
@@ -568,16 +569,17 @@ Proof.
   rewrite plus_comm, le_plus_minus_r by (now apply lt_le_weak, Plt_lt).
   reflexivity.
 (* NEG/POS *)
+  rewrite Z.pos_sub_spec.
   case Pcompare_spec; intros; simpl.
   subst; auto with real.
   rewrite Pminus_minus by trivial.
-  rewrite (pow_RN_plus x _ (nat_of_P n1)) by auto with real.
-  rewrite plus_comm, le_plus_minus_r by (now apply lt_le_weak, Plt_lt).
-  auto with real.
-  rewrite Pminus_minus by trivial.
   rewrite (pow_RN_plus x _ (nat_of_P m1)) by auto with real.
   rewrite plus_comm, le_plus_minus_r by (now apply lt_le_weak, Plt_lt).
   rewrite Rinv_mult_distr, Rinv_involutive; auto with real.
+  rewrite Pminus_minus by trivial.
+  rewrite (pow_RN_plus x _ (nat_of_P n1)) by auto with real.
+  rewrite plus_comm, le_plus_minus_r by (now apply lt_le_weak, Plt_lt).
+  auto with real.
 (* NEG/NEG *)
   rewrite Pplus_plus; auto with real.
   intros H'; rewrite pow_add; auto with real.