1 files changed, 0 insertions, 48 deletions
diff --git a/theories/Ints/BigZ.v b/theories/Ints/BigZ.v
deleted file mode 100644
index 8c7c1f809c..0000000000
--- a/theories/Ints/BigZ.v
+++ /dev/null
@@ -1,48 +0,0 @@
-Require Export BigN.
-Require Import ZMake.
-
-
-Module BigZ := Make BigN.
-
-
-Definition bigZ := BigZ.t.
-
-Delimit Scope bigZ_scope with bigZ.
-Bind Scope bigZ_scope with bigZ.
-Bind Scope bigZ_scope with BigZ.t.
-Bind Scope bigZ_scope with BigZ.t_.
-
-Notation " i + j " := (BigZ.add i j) : bigZ_scope.
-Notation " i - j " := (BigZ.sub i j) : bigZ_scope.
-Notation " i * j " := (BigZ.mul i j) : bigZ_scope.
-Notation " i / j " := (BigZ.div i j) : bigZ_scope.
-Notation " i ?= j " := (BigZ.compare i j) : bigZ_scope.
-
-
- Theorem spec_to_Z: 
-  forall n, BigN.to_Z (BigZ.to_N n) = 
-            (Zsgn (BigZ.to_Z n) * BigZ.to_Z n)%Z.
- intros n; case n; simpl; intros p; 
-     generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
- intros p1 H1; case H1; auto.
- intros p1 H1; case H1; auto.
- Qed.
-
- Theorem spec_to_N n: 
-  (BigZ.to_Z n = 
-    Zsgn (BigZ.to_Z n) * (BigN.to_Z (BigZ.to_N n)))%Z.
- intros n; case n; simpl; intros p; 
-     generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
- intros p1 H1; case H1; auto.
- intros p1 H1; case H1; auto.
- Qed.
-
- Theorem spec_to_Z_pos: 
-  forall n, (0 <= BigZ.to_Z n ->
-              BigN.to_Z (BigZ.to_N n) = BigZ.to_Z n)%Z.
- intros n; case n; simpl; intros p; 
-     generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
- intros p1 _  H1; case H1; auto.
- intros p1 H1; case H1; auto.
- Qed.
-