From 5bb42bbdb310392825d075dab81591463a871a1a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 25 Sep 2003 19:58:49 +0000
Subject: add_x_x de fast_integer vers auxiliary

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4475 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/ZArith/auxiliary.v | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v
index 68a5237839..ec8b42ac71 100644
--- a/theories/ZArith/auxiliary.v
+++ b/theories/ZArith/auxiliary.v
@@ -17,6 +17,7 @@ Require Decidable.
 Require Peano_dec.
 Require Export Compare_dec.
 
+
 Definition neq := [x,y:nat] ~(x=y).
 Definition Zne := [x,y:Z] ~(x=y).
 Theorem add_un_Zs : (x:positive) (POS (add_un x)) = (Zs (POS x)).
@@ -334,11 +335,6 @@ Intros r x y z t; Case r; [
     Rewrite Zcompare_Zplus_compatible; Assumption]].
 Qed.
 
-Lemma add_x_x : (x:positive) (add x x) = (xO x).
-Intros p; Apply convert_intro; Simpl; Rewrite convert_add;
-Unfold 3 convert ; Simpl; Rewrite ZL6; Trivial with arith.
-Qed.
-
 Theorem Zcompare_Zmult_compatible : 
    (x:positive)(y,z:Z)
       (Zcompare (Zmult (POS x) y) (Zmult (POS x) z)) = (Zcompare y z).
-- 
cgit v1.2.3