Added Z and Q implementations with int31.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9846 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 469 insertions, 394 deletions

diff --git a/Makefile b/Makefile
index 06e562f203..2de542be20 100644
--- a/Makefile
+++ b/Makefile
@@ -918,7 +918,8 @@ INTSVO=\
  theories/Ints/num/GenDiv.vo theories/Ints/num/GenSqrt.vo \
  theories/Ints/num/GenLift.vo theories/Ints/num/Zn2Z.vo\
  theories/Ints/num/Nbasic.vo theories/Ints/num/NMake.vo \
- theories/Ints/BigN.vo
+ theories/Ints/BigN.vo theories/Ints/num/ZMake.vo \
+ theories/Ints/BigZ.vo theories/Ints/num/QMake.vo
 # theories/Ints/List/ListAux.vo
 # theories/Ints/List/LPermutation.vo theories/Ints/List/Iterator.vo \
 # theories/Ints/List/ZProgression.vo
diff --git a/parsing/g_intsyntax.ml b/parsing/g_intsyntax.ml
index 0c2c870eb1..2c3189087c 100644
--- a/parsing/g_intsyntax.ml
+++ b/parsing/g_intsyntax.ml
@@ -8,7 +8,7 @@
 
 (*i $ $ i*)
 
-(* digit-based syntax for int31 and bigint *)
+(* digit-based syntax for int31, bigN and bigZ *)
 
 open Bigint
 open Libnames
@@ -31,7 +31,7 @@ let make_kn dir id = Libnames.encode_kn (make_dir dir) (Names.id_of_string id)
 let int31_module = ["Coq"; "Ints"; "Int31"]
 let int31_path = make_path int31_module "int31"
 let int31_id = make_kn int31_module
-
+let int31_scope = "int31_scope"
 
 let int31_construct = ConstructRef ((int31_id "int31",0),1)
 
@@ -39,7 +39,7 @@ let int31_0 = ConstructRef ((int31_id "digits",0),1)
 let int31_1 = ConstructRef ((int31_id "digits",0),2)
 
 
-(* bigint stuff*)
+(* bigN stuff*)
 let zn2z_module = ["Coq"; "Ints"; "Basic_type"]
 let zn2z_path = make_path zn2z_module "zn2z"
 let zn2z_id = make_kn zn2z_module
@@ -53,6 +53,7 @@ let bigN_path = make_path bigN_module "bigN"
 let bigN_id id = (Obj.magic ((Names.MPdot ((Names.MPfile (make_dir bigN_module)), 
                              Names.mk_label "BigN")),
               [], Names.id_of_string id) : Names.kernel_name)
+let bigN_scope = "bigN_scope"
 
 (* number of inlined level of bigN (actually the level 0 to n_inlined-1 are inlined) *)
 let n_inlined = of_string "13"
@@ -76,6 +77,21 @@ let bigN_constructor =
 		  (to_int n_inlined)+1
 	       )
 
+(*bigZ stuff*)
+let bigZ_module = ["Coq"; "Ints"; "BigZ"]
+let bigZ_path = make_path bigZ_module "bigZ"
+(* big ugly hack bis *)
+let bigZ_id id = (Obj.magic ((Names.MPdot ((Names.MPfile (make_dir bigZ_module)), 
+                             Names.mk_label "BigZ")),
+              [], Names.id_of_string id) : Names.kernel_name)
+let bigZ_scope = "bigZ_scope"
+
+let bigZ_pos = ConstructRef ((bigZ_id "t_",0),1)
+let bigZ_neg = ConstructRef ((bigZ_id "t_",0),2)
+
+
+
+
 (*** Definition of the Non_closed exception, used in the pretty printing ***)
 exception Non_closed
 
@@ -126,7 +142,7 @@ let uninterp_int31 i =
     None
 
 (* Actually declares the interpreter for int31 *)
-let _ = Notation.declare_numeral_interpreter "int31_scope"
+let _ = Notation.declare_numeral_interpreter int31_scope
   (int31_path, int31_module)
   interp_int31
   ([RRef (Util.dummy_loc, int31_construct)],
@@ -134,8 +150,8 @@ let _ = Notation.declare_numeral_interpreter "int31_scope"
    true)
 
 
-(*** Parsing for BigN in digital notation ***)
-(* the base for BigN (in Coq) that is 2^31 in our case *)
+(*** Parsing for bigN in digital notation ***)
+(* the base for bigN (in Coq) that is 2^31 in our case *)
 let base = pow two (of_string "31")
 
 (* base of the bigN of height N : *)
@@ -224,7 +240,7 @@ let bigint_of_word =
     let hght = get_height rc in
     transform hght rc
     
-let bigint_of_bigN rc=
+let bigint_of_bigN rc =
   match rc with
   | RApp (_,_,[one_arg]) -> bigint_of_word one_arg
   | RApp (_,_,[_;second_arg]) -> bigint_of_word second_arg
@@ -250,9 +266,46 @@ let bigN_list_of_constructors =
   build zero
 
 (* Actually declares the interpreter for bigN *)
-let _ = Notation.declare_numeral_interpreter "bigN_scope"
+let _ = Notation.declare_numeral_interpreter bigN_scope
   (bigN_path, bigN_module)
   interp_bigN
   (bigN_list_of_constructors,
    uninterp_bigN,
    true)
+
+
+(*** Parsing for bigZ in digital notation ***)
+let interp_bigZ dloc n = 
+  let ref_pos = RRef (dloc, bigZ_pos) in
+  let ref_neg = RRef (dloc, bigZ_neg) in
+  if is_pos_or_zero n then
+    RApp (dloc, ref_pos, [bigN_of_pos_bigint dloc n])
+  else
+    RApp (dloc, ref_neg, [bigN_of_pos_bigint dloc n])
+
+(* pretty printing functions for bigZ *)
+let bigint_of_bigZ = function
+  | RApp (_, RRef(_,c), [one_arg]) when c = bigZ_pos -> bigint_of_bigN one_arg
+  | RApp (_, RRef(_,c), [one_arg]) when c = bigZ_neg -> 
+      let opp_val = bigint_of_bigN one_arg in 
+      if equal opp_val zero then
+	raise Non_closed
+      else
+	neg opp_val
+  | _ -> raise Non_closed
+
+
+let uninterp_bigZ rc = 
+  try 
+    Some (bigint_of_bigZ rc)
+  with Non_closed ->
+    None
+
+(* Actually declares the interpreter for bigN *)
+let _ = Notation.declare_numeral_interpreter bigZ_scope
+  (bigZ_path, bigZ_module)
+  interp_bigZ
+  ([RRef (Util.dummy_loc, bigZ_pos);
+    RRef (Util.dummy_loc, bigZ_neg)],
+   uninterp_bigZ,
+   true)
diff --git a/theories/Ints/BigN.v b/theories/Ints/BigN.v
index 98e24c63fd..1d2b177dfb 100644
--- a/theories/Ints/BigN.v
+++ b/theories/Ints/BigN.v
@@ -66,8 +66,8 @@ Definition int31_op : znz_op int31.
  exact gcd31. (*gcd*)
  
  (* shift operations *)
- exact addmuldiv31. (*add_mul_div with positive ? *)
-(*modulo 2^p (p positive) *)
+ exact addmuldiv31. (*add_mul_div  *)
+(*modulo 2^p  *)
  exact (fun p i => 
      match compare31 p 32 with
      | Lt => addmuldiv31 p 0 (addmuldiv31 (31-p) i 0)
diff --git a/theories/Ints/BigZ.v b/theories/Ints/BigZ.v
new file mode 100644
index 0000000000..78fe2bced1
--- /dev/null
+++ b/theories/Ints/BigZ.v
@@ -0,0 +1,19 @@
+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.
diff --git a/theories/Ints/num/QMake.v b/theories/Ints/num/QMake.v
index 28f4bd991b..0fd20a1eb1 100644
--- a/theories/Ints/num/QMake.v
+++ b/theories/Ints/num/QMake.v
@@ -1,10 +1,12 @@
 Require Import Bool.
 Require Import ZArith.
 Require Import Arith.
+Require Export BigN.
+Require Export BigZ.
 
 Inductive q_type : Set := 
- | Qz : Z.t -> q_type
- | Qq : Z.t -> N.t -> q_type.
+ | Qz : BigZ.t -> q_type
+ | Qq : BigZ.t -> BigN.t -> q_type.
 
 Definition print_type x := 
  match x with
@@ -14,76 +16,76 @@ Definition print_type x :=
 
 Definition print x :=
  match x return print_type x with
- | Qz zx => Z.to_Z zx
- | Qq nx dx => (Z.to_Z nx, N.to_Z dx)
+ | Qz zx => BigZ.to_Z zx
+ | Qq nx dx => (BigZ.to_Z nx, BigN.to_Z dx)
  end.
 
 Module Qp.
 
  Definition t := q_type.
 
- Definition zero := Qz Z.zero.
- Definition one  := Qz Z.one.
- Definition minus_one := Qz Z.minus_one.
+ Definition zero := Qz BigZ.zero.
+ Definition one  := Qz BigZ.one.
+ Definition minus_one := Qz BigZ.minus_one.
 
- Definition of_Z x := Qz (Z.of_Z x).
+ Definition of_Z x := Qz (BigZ.of_Z x).
 
- Definition d_to_Z d := Z.Pos (N.succ d).
+ Definition d_to_Z d := BigZ.Pos (BigN.succ d).
 
  Definition compare x y :=
   match x, y with
-  | Qz zx, Qz zy => Z.compare zx zy
-  | Qz zx, Qq ny dy => Z.compare (Z.mul zx (d_to_Z dy)) ny
-  | Qq nx dy, Qz zy => Z.compare nx (Z.mul zy (d_to_Z dy))
+  | Qz zx, Qz zy => BigZ.compare zx zy
+  | Qz zx, Qq ny dy => BigZ.compare (BigZ.mul zx (d_to_Z dy)) ny
+  | Qq nx dy, Qz zy => BigZ.compare nx (BigZ.mul zy (d_to_Z dy))
   | Qq nx dx, Qq ny dy =>
-    Z.compare (Z.mul nx (d_to_Z dy)) (Z.mul ny (d_to_Z dx))
+    BigZ.compare (BigZ.mul nx (d_to_Z dy)) (BigZ.mul ny (d_to_Z dx))
   end.
 
  Definition opp x :=
   match x with
-  | Qz zx => Qz (Z.opp zx)
-  | Qq nx dx => Qq (Z.opp nx) dx
+  | Qz zx => Qz (BigZ.opp zx)
+  | Qq nx dx => Qq (BigZ.opp nx) dx
   end.
 
 (* Inv d > 0, Pour la forme normal unique on veut d > 1 *)
  Definition norm n d :=
-  if Z.eq_bool n Z.zero then zero
+  if BigZ.eq_bool n BigZ.zero then zero
   else
-    let gcd := N.gcd (Z.to_N n) d in
-    if N.eq_bool gcd N.one then Qq n (N.pred d)
+    let gcd := BigN.gcd (BigZ.to_N n) d in
+    if BigN.eq_bool gcd BigN.one then Qq n (BigN.pred d)
     else	
-      let n := Z.div n (Z.Pos gcd) in
-      let d := N.div d gcd in
-      if N.eq_bool d N.one then Qz n
-      else Qq n (N.pred d).
+      let n := BigZ.div n (BigZ.Pos gcd) in
+      let d := BigN.div d gcd in
+      if BigN.eq_bool d BigN.one then Qz n
+      else Qq n (BigN.pred d).
    
  Definition add x y :=
   match x, y with
-  | Qz zx, Qz zy => Qz (Z.add zx zy)
-  | Qz zx, Qq ny dy => Qq (Z.add (Z.mul zx (d_to_Z dy)) ny) dy
-  | Qq nx dx, Qz zy => Qq (Z.add nx (Z.mul zy (d_to_Z dx))) dx
+  | Qz zx, Qz zy => Qz (BigZ.add zx zy)
+  | Qz zx, Qq ny dy => Qq (BigZ.add (BigZ.mul zx (d_to_Z dy)) ny) dy
+  | Qq nx dx, Qz zy => Qq (BigZ.add nx (BigZ.mul zy (d_to_Z dx))) dx
   | Qq nx dx, Qq ny dy => 
-    let dx' := N.succ dx in
-    let dy' := N.succ dy in
-    let n := Z.add (Z.mul nx (Z.Pos dy')) (Z.mul ny (Z.Pos dx')) in
-    let d := N.pred (N.mul dx' dy') in
+    let dx' := BigN.succ dx in
+    let dy' := BigN.succ dy in
+    let n := BigZ.add (BigZ.mul nx (BigZ.Pos dy')) (BigZ.mul ny (BigZ.Pos dx')) in
+    let d := BigN.pred (BigN.mul dx' dy') in
     Qq n d
   end.
 
  Definition add_norm x y := 
   match x, y with
-  | Qz zx, Qz zy => Qz (Z.add zx zy)
+  | Qz zx, Qz zy => Qz (BigZ.add zx zy)
   | Qz zx, Qq ny dy => 
-    let d := N.succ dy in
-    norm (Z.add (Z.mul zx (Z.Pos d)) ny) d 
+    let d := BigN.succ dy in
+    norm (BigZ.add (BigZ.mul zx (BigZ.Pos d)) ny) d 
   | Qq nx dx, Qz zy =>
-    let d := N.succ dx in
-    norm (Z.add (Z.mul zy (Z.Pos d)) nx) d
+    let d := BigN.succ dx in
+    norm (BigZ.add (BigZ.mul zy (BigZ.Pos d)) nx) d
   | Qq nx dx, Qq ny dy =>
-    let dx' := N.succ dx in
-    let dy' := N.succ dy in
-    let n := Z.add (Z.mul nx (Z.Pos dy')) (Z.mul ny (Z.Pos dx')) in
-    let d := N.mul dx' dy' in
+    let dx' := BigN.succ dx in
+    let dy' := BigN.succ dy in
+    let n := BigZ.add (BigZ.mul nx (BigZ.Pos dy')) (BigZ.mul ny (BigZ.Pos dx')) in
+    let d := BigN.mul dx' dy' in
     norm n d 
   end.
  
@@ -93,81 +95,81 @@ Module Qp.
 
  Definition mul x y :=
   match x, y with
-  | Qz zx, Qz zy => Qz (Z.mul zx zy)
-  | Qz zx, Qq ny dy => Qq (Z.mul zx ny) dy
-  | Qq nx dx, Qz zy => Qq (Z.mul nx zy) dx
+  | Qz zx, Qz zy => Qz (BigZ.mul zx zy)
+  | Qz zx, Qq ny dy => Qq (BigZ.mul zx ny) dy
+  | Qq nx dx, Qz zy => Qq (BigZ.mul nx zy) dx
   | Qq nx dx, Qq ny dy => 
-    Qq (Z.mul nx ny) (N.pred (N.mul (N.succ dx) (N.succ dy)))
+    Qq (BigZ.mul nx ny) (BigN.pred (BigN.mul (BigN.succ dx) (BigN.succ dy)))
   end.
 
  Definition mul_norm x y := 
   match x, y with
-  | Qz zx, Qz zy => Qz (Z.mul zx zy)
+  | Qz zx, Qz zy => Qz (BigZ.mul zx zy)
   | Qz zx, Qq ny dy =>
-    if Z.eq_bool zx Z.zero then zero
+    if BigZ.eq_bool zx BigZ.zero then zero
     else	
-      let d := N.succ dy in
-      let gcd := N.gcd (Z.to_N zx) d in
-      if N.eq_bool gcd N.one then Qq (Z.mul zx ny) dy
+      let d := BigN.succ dy in
+      let gcd := BigN.gcd (BigZ.to_N zx) d in
+      if BigN.eq_bool gcd BigN.one then Qq (BigZ.mul zx ny) dy
       else 
-        let zx := Z.div zx (Z.Pos gcd) in
-        let d := N.div d gcd in
-        if N.eq_bool d N.one then Qz (Z.mul zx ny)
-        else Qq (Z.mul zx ny) (N.pred d)
+        let zx := BigZ.div zx (BigZ.Pos gcd) in
+        let d := BigN.div d gcd in
+        if BigN.eq_bool d BigN.one then Qz (BigZ.mul zx ny)
+        else Qq (BigZ.mul zx ny) (BigN.pred d)
   | Qq nx dx, Qz zy =>   
-    if Z.eq_bool zy Z.zero then zero
+    if BigZ.eq_bool zy BigZ.zero then zero
     else	
-      let d := N.succ dx in
-      let gcd := N.gcd (Z.to_N zy) d in
-      if N.eq_bool gcd N.one then Qq (Z.mul zy nx) dx
+      let d := BigN.succ dx in
+      let gcd := BigN.gcd (BigZ.to_N zy) d in
+      if BigN.eq_bool gcd BigN.one then Qq (BigZ.mul zy nx) dx
       else 
-        let zy := Z.div zy (Z.Pos gcd) in
-        let d := N.div d gcd in
-        if N.eq_bool d N.one then Qz (Z.mul zy nx)
-        else Qq (Z.mul zy nx) (N.pred d)
+        let zy := BigZ.div zy (BigZ.Pos gcd) in
+        let d := BigN.div d gcd in
+        if BigN.eq_bool d BigN.one then Qz (BigZ.mul zy nx)
+        else Qq (BigZ.mul zy nx) (BigN.pred d)
   | Qq nx dx, Qq ny dy => 
-    norm (Z.mul nx ny) (N.mul (N.succ dx) (N.succ dy))
+    norm (BigZ.mul nx ny) (BigN.mul (BigN.succ dx) (BigN.succ dy))
   end.
 
  Definition inv x := 
   match x with
-  | Qz (Z.Pos n) => 
-    if N.eq_bool n N.zero then zero else Qq Z.one (N.pred n)
-  | Qz (Z.Neg n) => 
-    if N.eq_bool n N.zero then zero else Qq Z.minus_one (N.pred n)
-  | Qq (Z.Pos n) d => 
-    if N.eq_bool n N.zero then zero else Qq (Z.Pos (N.succ d)) (N.pred n)
-  | Qq (Z.Neg n) d => 
-    if N.eq_bool n N.zero then zero else Qq (Z.Neg (N.succ d)) (N.pred n)
+  | Qz (BigZ.Pos n) => 
+    if BigN.eq_bool n BigN.zero then zero else Qq BigZ.one (BigN.pred n)
+  | Qz (BigZ.Neg n) => 
+    if BigN.eq_bool n BigN.zero then zero else Qq BigZ.minus_one (BigN.pred n)
+  | Qq (BigZ.Pos n) d => 
+    if BigN.eq_bool n BigN.zero then zero else Qq (BigZ.Pos (BigN.succ d)) (BigN.pred n)
+  | Qq (BigZ.Neg n) d => 
+    if BigN.eq_bool n BigN.zero then zero else Qq (BigZ.Neg (BigN.succ d)) (BigN.pred n)
   end.
 
 Definition inv_norm x := 
  match x with
- | Qz (Z.Pos n) => 
-      if N.eq_bool n N.zero then zero else
-      if N.eq_bool n N.one then x else Qq Z.one (N.pred n)
- | Qz (Z.Neg n) => 
-      if N.eq_bool n N.zero then zero  else
-      if N.eq_bool n N.one then x else Qq Z.minus_one n
- | Qq (Z.Pos n) d => let d := N.succ d in 
-                  if N.eq_bool n N.one then Qz (Z.Pos d) 
-                     else Qq (Z.Pos d) (N.pred n)
- | Qq (Z.Neg n) d => let d := N.succ d in 
-                  if N.eq_bool n N.one then Qz (Z.Neg d) 
-                     else Qq (Z.Pos d) (N.pred n)
+ | Qz (BigZ.Pos n) => 
+      if BigN.eq_bool n BigN.zero then zero else
+      if BigN.eq_bool n BigN.one then x else Qq BigZ.one (BigN.pred n)
+ | Qz (BigZ.Neg n) => 
+      if BigN.eq_bool n BigN.zero then zero  else
+      if BigN.eq_bool n BigN.one then x else Qq BigZ.minus_one n
+ | Qq (BigZ.Pos n) d => let d := BigN.succ d in 
+                  if BigN.eq_bool n BigN.one then Qz (BigZ.Pos d) 
+                     else Qq (BigZ.Pos d) (BigN.pred n)
+ | Qq (BigZ.Neg n) d => let d := BigN.succ d in 
+                  if BigN.eq_bool n BigN.one then Qz (BigZ.Neg d) 
+                     else Qq (BigZ.Pos d) (BigN.pred n)
  end.
 
 
  Definition square x :=
   match x with
-  | Qz zx => Qz (Z.square zx)
-  | Qq nx dx => Qq (Z.square nx) (N.pred (N.square (N.succ dx)))
+  | Qz zx => Qz (BigZ.square zx)
+  | Qq nx dx => Qq (BigZ.square nx) (BigN.pred (BigN.square (BigN.succ dx)))
   end.
 
  Definition power_pos x p :=
   match x with
-  | Qz zx => Qz (Z.power_pos zx p)
-  | Qq nx dx => Qq (Z.power_pos nx p) (N.pred (N.power_pos (N.succ dx) p))
+  | Qz zx => Qz (BigZ.power_pos zx p)
+  | Qq nx dx => Qq (BigZ.power_pos nx p) (BigN.pred (BigN.power_pos (BigN.succ dx) p))
   end.
 
 End Qp.
@@ -180,16 +182,16 @@ Module Qv.
 
  Definition t := q_type.
 
- Definition zero := Qz Z.zero.
- Definition one  := Qz Z.one.
- Definition minus_one := Qz Z.minus_one.
+ Definition zero := Qz BigZ.zero.
+ Definition one  := Qz BigZ.one.
+ Definition minus_one := Qz BigZ.minus_one.
 
- Definition of_Z x := Qz (Z.of_Z x).
+ Definition of_Z x := Qz (BigZ.of_Z x).
 
  Definition is_valid x := 
   match x with
   | Qz _ => True
-  | Qq n d => if N.eq_bool d N.zero then False else True
+  | Qq n d => if BigN.eq_bool d BigN.zero then False else True
   end.
  (* Les fonctions doivent assurer que si leur arguments sont valides alors
     le resultat est correct et valide (si c'est un Q) 
@@ -197,50 +199,50 @@ Module Qv.
 
  Definition compare x y :=
   match x, y with
-  | Qz zx, Qz zy => Z.compare zx zy
-  | Qz zx, Qq ny dy => Z.compare (Z.mul zx (Z.Pos dy)) ny
-  | Qq nx dx, Qz zy => Z.compare Z.zero zy 
-  | Qq nx dx, Qq ny dy => Z.compare (Z.mul nx (Z.Pos dy)) (Z.mul ny (Z.Pos dx))
+  | Qz zx, Qz zy => BigZ.compare zx zy
+  | Qz zx, Qq ny dy => BigZ.compare (BigZ.mul zx (BigZ.Pos dy)) ny
+  | Qq nx dx, Qz zy => BigZ.compare BigZ.zero zy 
+  | Qq nx dx, Qq ny dy => BigZ.compare (BigZ.mul nx (BigZ.Pos dy)) (BigZ.mul ny (BigZ.Pos dx))
   end.
 
  Definition opp x :=
   match x with
-  | Qz zx => Qz (Z.opp zx)
-  | Qq nx dx => Qq (Z.opp nx) dx
+  | Qz zx => Qz (BigZ.opp zx)
+  | Qq nx dx => Qq (BigZ.opp nx) dx
   end.
 
  Definition norm n d :=
-  if Z.eq_bool n Z.zero then zero
+  if BigZ.eq_bool n BigZ.zero then zero
   else
-    let gcd := N.gcd (Z.to_N n) d in
-    if N.eq_bool gcd N.one then Qq n d
+    let gcd := BigN.gcd (BigZ.to_N n) d in
+    if BigN.eq_bool gcd BigN.one then Qq n d
     else	
-      let n := Z.div n (Z.Pos gcd) in
-      let d := N.div d gcd in
-      if N.eq_bool d N.one then Qz n
+      let n := BigZ.div n (BigZ.Pos gcd) in
+      let d := BigN.div d gcd in
+      if BigN.eq_bool d BigN.one then Qz n
       else Qq n d.
    
  Definition add x y :=
   match x, y with
-  | Qz zx, Qz zy => Qz (Z.add zx zy)
-  | Qz zx, Qq ny dy => Qq (Z.add (Z.mul zx (Z.Pos dy)) ny) dy
-  | Qq nx dx, Qz zy => Qq (Z.add nx (Z.mul zy (Z.Pos dx))) dx
+  | Qz zx, Qz zy => Qz (BigZ.add zx zy)
+  | Qz zx, Qq ny dy => Qq (BigZ.add (BigZ.mul zx (BigZ.Pos dy)) ny) dy
+  | Qq nx dx, Qz zy => Qq (BigZ.add nx (BigZ.mul zy (BigZ.Pos dx))) dx
   | Qq nx dx, Qq ny dy => 
-    let n := Z.add (Z.mul nx (Z.Pos dy)) (Z.mul ny (Z.Pos dx)) in
-    let d := N.mul dx dy in
+    let n := BigZ.add (BigZ.mul nx (BigZ.Pos dy)) (BigZ.mul ny (BigZ.Pos dx)) in
+    let d := BigN.mul dx dy in
     Qq n d
   end.
 
  Definition add_norm x y := 
   match x, y with
-  | Qz zx, Qz zy => Qz (Z.add zx zy)
+  | Qz zx, Qz zy => Qz (BigZ.add zx zy)
   | Qz zx, Qq ny dy => 
-    norm (Z.add (Z.mul zx (Z.Pos dy)) ny) dy 
+    norm (BigZ.add (BigZ.mul zx (BigZ.Pos dy)) ny) dy 
   | Qq nx dx, Qz zy =>
-    norm (Z.add (Z.mul zy (Z.Pos dx)) nx) dx
+    norm (BigZ.add (BigZ.mul zy (BigZ.Pos dx)) nx) dx
   | Qq nx dx, Qq ny dy =>
-    let n := Z.add (Z.mul nx (Z.Pos dy)) (Z.mul ny (Z.Pos dx)) in
-    let d := N.mul dx dy in
+    let n := BigZ.add (BigZ.mul nx (BigZ.Pos dy)) (BigZ.mul ny (BigZ.Pos dx)) in
+    let d := BigN.mul dx dy in
     norm n d 
   end.
  
@@ -250,61 +252,61 @@ Module Qv.
 
  Definition mul x y :=
   match x, y with
-  | Qz zx, Qz zy => Qz (Z.mul zx zy)
-  | Qz zx, Qq ny dy => Qq (Z.mul zx ny) dy
-  | Qq nx dx, Qz zy => Qq (Z.mul nx zy) dx
+  | Qz zx, Qz zy => Qz (BigZ.mul zx zy)
+  | Qz zx, Qq ny dy => Qq (BigZ.mul zx ny) dy
+  | Qq nx dx, Qz zy => Qq (BigZ.mul nx zy) dx
   | Qq nx dx, Qq ny dy => 
-    Qq (Z.mul nx ny) (N.mul dx dy)
+    Qq (BigZ.mul nx ny) (BigN.mul dx dy)
   end.
 
  Definition mul_norm x y := 
   match x, y with
-  | Qz zx, Qz zy => Qz (Z.mul zx zy)
+  | Qz zx, Qz zy => Qz (BigZ.mul zx zy)
   | Qz zx, Qq ny dy =>
-    if Z.eq_bool zx Z.zero then zero
+    if BigZ.eq_bool zx BigZ.zero then zero
     else	
-      let gcd := N.gcd (Z.to_N zx) dy in
-      if N.eq_bool gcd N.one then Qq (Z.mul zx ny) dy
+      let gcd := BigN.gcd (BigZ.to_N zx) dy in
+      if BigN.eq_bool gcd BigN.one then Qq (BigZ.mul zx ny) dy
       else 
-        let zx := Z.div zx (Z.Pos gcd) in
-        let d := N.div dy gcd in
-        if N.eq_bool d N.one then Qz (Z.mul zx ny)
-        else Qq (Z.mul zx ny) d
+        let zx := BigZ.div zx (BigZ.Pos gcd) in
+        let d := BigN.div dy gcd in
+        if BigN.eq_bool d BigN.one then Qz (BigZ.mul zx ny)
+        else Qq (BigZ.mul zx ny) d
   | Qq nx dx, Qz zy =>   
-    if Z.eq_bool zy Z.zero then zero
+    if BigZ.eq_bool zy BigZ.zero then zero
     else	
-      let gcd := N.gcd (Z.to_N zy) dx in
-      if N.eq_bool gcd N.one then Qq (Z.mul zy nx) dx
+      let gcd := BigN.gcd (BigZ.to_N zy) dx in
+      if BigN.eq_bool gcd BigN.one then Qq (BigZ.mul zy nx) dx
       else 
-        let zy := Z.div zy (Z.Pos gcd) in
-        let d := N.div dx gcd in
-        if N.eq_bool d N.one then Qz (Z.mul zy nx)
-        else Qq (Z.mul zy nx) d
-  | Qq nx dx, Qq ny dy => norm (Z.mul nx ny) (N.mul dx dy)
+        let zy := BigZ.div zy (BigZ.Pos gcd) in
+        let d := BigN.div dx gcd in
+        if BigN.eq_bool d BigN.one then Qz (BigZ.mul zy nx)
+        else Qq (BigZ.mul zy nx) d
+  | Qq nx dx, Qq ny dy => norm (BigZ.mul nx ny) (BigN.mul dx dy)
   end.
 
  Definition inv x := 
   match x with
-  | Qz (Z.Pos n) => 
-    if N.eq_bool n N.zero then zero else Qq Z.one n
-  | Qz (Z.Neg n) => 
-    if N.eq_bool n N.zero then zero else Qq Z.minus_one n
-  | Qq (Z.Pos n) d => 
-    if N.eq_bool n N.zero then zero else Qq (Z.Pos d) n
-  | Qq (Z.Neg n) d => 
-    if N.eq_bool n N.zero then zero else Qq (Z.Neg d) n
+  | Qz (BigZ.Pos n) => 
+    if BigN.eq_bool n BigN.zero then zero else Qq BigZ.one n
+  | Qz (BigZ.Neg n) => 
+    if BigN.eq_bool n BigN.zero then zero else Qq BigZ.minus_one n
+  | Qq (BigZ.Pos n) d => 
+    if BigN.eq_bool n BigN.zero then zero else Qq (BigZ.Pos d) n
+  | Qq (BigZ.Neg n) d => 
+    if BigN.eq_bool n BigN.zero then zero else Qq (BigZ.Neg d) n
   end.
 
  Definition square x :=
   match x with
-  | Qz zx => Qz (Z.square zx)
-  | Qq nx dx => Qq (Z.square nx) (N.square dx)
+  | Qz zx => Qz (BigZ.square zx)
+  | Qq nx dx => Qq (BigZ.square nx) (BigN.square dx)
   end.
 
  Definition power_pos x p :=
   match x with
-  | Qz zx => Qz (Z.power_pos zx p)
-  | Qq nx dx => Qq (Z.power_pos nx p) (N.power_pos dx p)
+  | Qz zx => Qz (BigZ.power_pos zx p)
+  | Qq nx dx => Qq (BigZ.power_pos nx p) (BigN.power_pos dx p)
   end.
 
 End Qv.
@@ -319,44 +321,44 @@ Module Q.
 
  Definition t := q_type.
 
- Definition zero := Qz Z.zero.
- Definition one  := Qz Z.one.
- Definition minus_one := Qz Z.minus_one.
+ Definition zero := Qz BigZ.zero.
+ Definition one  := Qz BigZ.one.
+ Definition minus_one := Qz BigZ.minus_one.
 
- Definition of_Z x := Qz (Z.of_Z x).
+ Definition of_Z x := Qz (BigZ.of_Z x).
 
  Definition compare x y :=
   match x, y with
-  | Qz zx, Qz zy => Z.compare zx zy
+  | Qz zx, Qz zy => BigZ.compare zx zy
   | Qz zx, Qq ny dy => 
-    if N.eq_bool dy N.zero then Z.compare zx Z.zero
-    else Z.compare (Z.mul zx (Z.Pos dy)) ny
+    if BigN.eq_bool dy BigN.zero then BigZ.compare zx BigZ.zero
+    else BigZ.compare (BigZ.mul zx (BigZ.Pos dy)) ny
   | Qq nx dx, Qz zy => 
-    if N.eq_bool dx N.zero then Z.compare Z.zero zy 
-    else Z.compare nx (Z.mul zy (Z.Pos dx))
+    if BigN.eq_bool dx BigN.zero then BigZ.compare BigZ.zero zy 
+    else BigZ.compare nx (BigZ.mul zy (BigZ.Pos dx))
   | Qq nx dx, Qq ny dy =>
-    match N.eq_bool dx N.zero, N.eq_bool dy N.zero with
+    match BigN.eq_bool dx BigN.zero, BigN.eq_bool dy BigN.zero with
     | true, true => Eq
-    | true, false => Z.compare Z.zero ny
-    | false, true => Z.compare nx Z.zero
-    | false, false => Z.compare (Z.mul nx (Z.Pos dy)) (Z.mul ny (Z.Pos dx))
+    | true, false => BigZ.compare BigZ.zero ny
+    | false, true => BigZ.compare nx BigZ.zero
+    | false, false => BigZ.compare (BigZ.mul nx (BigZ.Pos dy)) (BigZ.mul ny (BigZ.Pos dx))
     end
   end.
 
  Definition opp x :=
   match x with
-  | Qz zx => Qz (Z.opp zx)
-  | Qq nx dx => Qq (Z.opp nx) dx
+  | Qz zx => Qz (BigZ.opp zx)
+  | Qq nx dx => Qq (BigZ.opp nx) dx
   end.
 
 (* Je pense que cette fonction normalise bien ... *)
  Definition norm n d :=
-  let gcd := N.gcd (Z.to_N n) d in 
-  match N.compare N.one gcd with
+  let gcd := BigN.gcd (BigZ.to_N n) d in 
+  match BigN.compare BigN.one gcd with
   | Lt => 
-    let n := Z.div n (Z.Pos gcd) in
-    let d := N.div d gcd in
-    match N.compare d N.one with
+    let n := BigZ.div n (BigZ.Pos gcd) in
+    let d := BigN.div d gcd in
+    match BigN.compare d BigN.one with
     | Gt => Qq n d
     | Eq => Qz n
     | Lt => zero
@@ -369,20 +371,20 @@ Module Q.
   match x with
   | Qz zx =>
     match y with
-    | Qz zy => Qz (Z.add zx zy)
+    | Qz zy => Qz (BigZ.add zx zy)
     | Qq ny dy => 
-      if N.eq_bool dy N.zero then x 
-      else Qq (Z.add (Z.mul zx (Z.Pos dy)) ny) dy
+      if BigN.eq_bool dy BigN.zero then x 
+      else Qq (BigZ.add (BigZ.mul zx (BigZ.Pos dy)) ny) dy
     end
   | Qq nx dx =>
-    if N.eq_bool dx N.zero then y 
+    if BigN.eq_bool dx BigN.zero then y 
     else match y with
-    | Qz zy => Qq (Z.add nx (Z.mul zy (Z.Pos dx))) dx
+    | Qz zy => Qq (BigZ.add nx (BigZ.mul zy (BigZ.Pos dx))) dx
     | Qq ny dy =>
-      if N.eq_bool dy N.zero then x
+      if BigN.eq_bool dy BigN.zero then x
       else
-       let n := Z.add (Z.mul nx (Z.Pos dy)) (Z.mul ny (Z.Pos dx)) in
-       let d := N.mul dx dy in
+       let n := BigZ.add (BigZ.mul nx (BigZ.Pos dy)) (BigZ.mul ny (BigZ.Pos dx)) in
+       let d := BigN.mul dx dy in
        Qq n d
     end
   end.
@@ -391,20 +393,20 @@ Module Q.
   match x with
   | Qz zx =>
     match y with
-    | Qz zy => Qz (Z.add zx zy)
+    | Qz zy => Qz (BigZ.add zx zy)
     | Qq ny dy =>  
-      if N.eq_bool dy N.zero then x 
-      else norm (Z.add (Z.mul zx (Z.Pos dy)) ny) dy
+      if BigN.eq_bool dy BigN.zero then x 
+      else norm (BigZ.add (BigZ.mul zx (BigZ.Pos dy)) ny) dy
     end
   | Qq nx dx =>
-    if N.eq_bool dx N.zero then y 
+    if BigN.eq_bool dx BigN.zero then y 
     else match y with
-    | Qz zy => norm (Z.add nx (Z.mul zy (Z.Pos dx))) dx
+    | Qz zy => norm (BigZ.add nx (BigZ.mul zy (BigZ.Pos dx))) dx
     | Qq ny dy =>
-      if N.eq_bool dy N.zero then x
+      if BigN.eq_bool dy BigN.zero then x
       else
-       let n := Z.add (Z.mul nx (Z.Pos dy)) (Z.mul ny (Z.Pos dx)) in
-       let d := N.mul dx dy in
+       let n := BigZ.add (BigZ.mul nx (BigZ.Pos dy)) (BigZ.mul ny (BigZ.Pos dx)) in
+       let d := BigN.mul dx dy in
        norm n d
     end
   end.
@@ -415,85 +417,85 @@ Module Q.
 
  Definition mul x y :=
   match x, y with
-  | Qz zx, Qz zy => Qz (Z.mul zx zy)
-  | Qz zx, Qq ny dy => Qq (Z.mul zx ny) dy
-  | Qq nx dx, Qz zy => Qq (Z.mul nx zy) dx
-  | Qq nx dx, Qq ny dy => Qq (Z.mul nx ny) (N.mul dx dy)
+  | Qz zx, Qz zy => Qz (BigZ.mul zx zy)
+  | Qz zx, Qq ny dy => Qq (BigZ.mul zx ny) dy
+  | Qq nx dx, Qz zy => Qq (BigZ.mul nx zy) dx
+  | Qq nx dx, Qq ny dy => Qq (BigZ.mul nx ny) (BigN.mul dx dy)
   end.
 
 Definition mul_norm x y := 
  match x, y with
- | Qz zx, Qz zy => Qz (Z.mul zx zy)
+ | Qz zx, Qz zy => Qz (BigZ.mul zx zy)
  | Qz zx, Qq ny dy =>
-   if Z.eq_bool zx Z.zero then zero
+   if BigZ.eq_bool zx BigZ.zero then zero
    else	
-     let d := N.succ dy in
-     let gcd := N.gcd (Z.to_N zx) d in
-     if N.eq_bool gcd N.one then Qq (Z.mul zx ny) dy
+     let d := BigN.succ dy in
+     let gcd := BigN.gcd (BigZ.to_N zx) d in
+     if BigN.eq_bool gcd BigN.one then Qq (BigZ.mul zx ny) dy
      else 
-       let zx := Z.div zx (Z.Pos gcd) in
-       let d := N.div d gcd in
-       if N.eq_bool d N.one then Qz (Z.mul zx ny)
-       else Qq (Z.mul zx ny) (N.pred d)
+       let zx := BigZ.div zx (BigZ.Pos gcd) in
+       let d := BigN.div d gcd in
+       if BigN.eq_bool d BigN.one then Qz (BigZ.mul zx ny)
+       else Qq (BigZ.mul zx ny) (BigN.pred d)
  | Qq nx dx, Qz zy =>   
-   if Z.eq_bool zy Z.zero then zero
+   if BigZ.eq_bool zy BigZ.zero then zero
    else	
-     let d := N.succ dx in
-     let gcd := N.gcd (Z.to_N zy) d in
-     if N.eq_bool gcd N.one then Qq (Z.mul zy nx) dx
+     let d := BigN.succ dx in
+     let gcd := BigN.gcd (BigZ.to_N zy) d in
+     if BigN.eq_bool gcd BigN.one then Qq (BigZ.mul zy nx) dx
      else 
-       let zy := Z.div zy (Z.Pos gcd) in
-       let d := N.div d gcd in
-       if N.eq_bool d N.one then Qz (Z.mul zy nx)
-       else Qq (Z.mul zy nx) (N.pred d)
+       let zy := BigZ.div zy (BigZ.Pos gcd) in
+       let d := BigN.div d gcd in
+       if BigN.eq_bool d BigN.one then Qz (BigZ.mul zy nx)
+       else Qq (BigZ.mul zy nx) (BigN.pred d)
  | Qq nx dx, Qq ny dy => 
-     let dx := N.succ dx in
-     let dy := N.succ dy in
+     let dx := BigN.succ dx in
+     let dy := BigN.succ dy in
      let (nx, dy) := 
-       let gcd := N.gcd (Z.to_N nx) dy in
-       if N.eq_bool gcd N.one then (nx, dy)
-       else (Z.div nx (Z.Pos gcd), N.div dy gcd) in
+       let gcd := BigN.gcd (BigZ.to_N nx) dy in
+       if BigN.eq_bool gcd BigN.one then (nx, dy)
+       else (BigZ.div nx (BigZ.Pos gcd), BigN.div dy gcd) in
      let (ny, dx) := 
-       let gcd := N.gcd (Z.to_N ny) dx in
-       if N.eq_bool gcd N.one then (ny, dx)
-       else (Z.div ny (Z.Pos gcd), N.div dx gcd) in
-     let d := (N.mul dx dy) in
-     if N.eq_bool d N.one then Qz (Z.mul ny nx) 
-     else Qq (Z.mul ny nx) (N.pred d)
+       let gcd := BigN.gcd (BigZ.to_N ny) dx in
+       if BigN.eq_bool gcd BigN.one then (ny, dx)
+       else (BigZ.div ny (BigZ.Pos gcd), BigN.div dx gcd) in
+     let d := (BigN.mul dx dy) in
+     if BigN.eq_bool d BigN.one then Qz (BigZ.mul ny nx) 
+     else Qq (BigZ.mul ny nx) (BigN.pred d)
  end.
 
 
 Definition inv x := 
  match x with
- | Qz (Z.Pos n) => Qq Z.one (N.pred n)
- | Qz (Z.Neg n) => Qq Z.minus_one (N.pred n)
- | Qq (Z.Pos n) d => Qq (Z.Pos (N.succ d)) (N.pred n)
- | Qq (Z.Neg n) d => Qq (Z.Neg (N.succ d)) (N.pred n)
+ | Qz (BigZ.Pos n) => Qq BigZ.one (BigN.pred n)
+ | Qz (BigZ.Neg n) => Qq BigZ.minus_one (BigN.pred n)
+ | Qq (BigZ.Pos n) d => Qq (BigZ.Pos (BigN.succ d)) (BigN.pred n)
+ | Qq (BigZ.Neg n) d => Qq (BigZ.Neg (BigN.succ d)) (BigN.pred n)
  end.
 
 
 Definition inv_norm x := 
  match x with
- | Qz (Z.Pos n) => if N.eq_bool n N.one then x else Qq Z.one (N.pred n)
- | Qz (Z.Neg n) => if N.eq_bool n N.one then x else Qq Z.minus_one n
- | Qq (Z.Pos n) d => let d := N.succ d in 
-                  if N.eq_bool n N.one then Qz (Z.Pos d) 
-                     else Qq (Z.Pos d) (N.pred n)
- | Qq (Z.Neg n) d => let d := N.succ d in 
-                  if N.eq_bool n N.one then Qz (Z.Neg d) 
-                     else Qq (Z.Pos d) (N.pred n)
+ | Qz (BigZ.Pos n) => if BigN.eq_bool n BigN.one then x else Qq BigZ.one (BigN.pred n)
+ | Qz (BigZ.Neg n) => if BigN.eq_bool n BigN.one then x else Qq BigZ.minus_one n
+ | Qq (BigZ.Pos n) d => let d := BigN.succ d in 
+                  if BigN.eq_bool n BigN.one then Qz (BigZ.Pos d) 
+                     else Qq (BigZ.Pos d) (BigN.pred n)
+ | Qq (BigZ.Neg n) d => let d := BigN.succ d in 
+                  if BigN.eq_bool n BigN.one then Qz (BigZ.Neg d) 
+                     else Qq (BigZ.Pos d) (BigN.pred n)
  end.
 
  Definition square x :=
   match x with
-  | Qz zx => Qz (Z.square zx)
-  | Qq nx dx => Qq (Z.square nx) (N.square dx)
+  | Qz zx => Qz (BigZ.square zx)
+  | Qq nx dx => Qq (BigZ.square nx) (BigN.square dx)
   end.
 
  Definition power_pos x p :=
   match x with
-  | Qz zx => Qz (Z.power_pos zx p)
-  | Qq nx dx => Qq (Z.power_pos nx p) (N.power_pos dx p)
+  | Qz zx => Qz (BigZ.power_pos zx p)
+  | Qq nx dx => Qq (BigZ.power_pos nx p) (BigN.power_pos dx p)
   end.
 
 End Q.
@@ -511,71 +513,71 @@ Module Qif.
 
  Definition t := q_type.
 
- Definition zero := Qz Z.zero.
- Definition one  := Qz Z.one.
- Definition minus_one := Qz Z.minus_one.
+ Definition zero := Qz BigZ.zero.
+ Definition one  := Qz BigZ.one.
+ Definition minus_one := Qz BigZ.minus_one.
 
- Definition of_Z x := Qz (Z.of_Z x).
+ Definition of_Z x := Qz (BigZ.of_Z x).
 
  Definition compare x y :=
   match x, y with
-  | Qz zx, Qz zy => Z.compare zx zy
+  | Qz zx, Qz zy => BigZ.compare zx zy
   | Qz zx, Qq ny dy => 
-    if N.eq_bool dy N.zero then Z.compare zx Z.zero
-    else Z.compare (Z.mul zx (Z.Pos dy)) ny
+    if BigN.eq_bool dy BigN.zero then BigZ.compare zx BigZ.zero
+    else BigZ.compare (BigZ.mul zx (BigZ.Pos dy)) ny
   | Qq nx dx, Qz zy => 
-    if N.eq_bool dx N.zero then Z.compare Z.zero zy 
-    else Z.compare nx (Z.mul zy (Z.Pos dx))
+    if BigN.eq_bool dx BigN.zero then BigZ.compare BigZ.zero zy 
+    else BigZ.compare nx (BigZ.mul zy (BigZ.Pos dx))
   | Qq nx dx, Qq ny dy =>
-    match N.eq_bool dx N.zero, N.eq_bool dy N.zero with
+    match BigN.eq_bool dx BigN.zero, BigN.eq_bool dy BigN.zero with
     | true, true => Eq
-    | true, false => Z.compare Z.zero ny
-    | false, true => Z.compare nx Z.zero
-    | false, false => Z.compare (Z.mul nx (Z.Pos dy)) (Z.mul ny (Z.Pos dx))
+    | true, false => BigZ.compare BigZ.zero ny
+    | false, true => BigZ.compare nx BigZ.zero
+    | false, false => BigZ.compare (BigZ.mul nx (BigZ.Pos dy)) (BigZ.mul ny (BigZ.Pos dx))
     end
   end.
 
  Definition opp x :=
   match x with
-  | Qz zx => Qz (Z.opp zx)
-  | Qq nx dx => Qq (Z.opp nx) dx
+  | Qz zx => Qz (BigZ.opp zx)
+  | Qq nx dx => Qq (BigZ.opp nx) dx
   end.
 
 
  Definition do_norm_n n := 
   match n with
-  | N.N0 _ => false
-  | N.N1 _ => false
-  | N.N2 _ => false
-  | N.N3 _ => false
-  | N.N4 _ => false
-  | N.N5 _ => false
-  | N.N6 _ => false
-  | N.N7 _ => false
-  | N.N8 _ => false
-  | N.N9 _ => true 
-  | N.N10 _ => true
-  | N.N11 _ => true
-  | N.N12 _ => true
-  | N.Nn n _ => true
+  | BigN.N0 _ => false
+  | BigN.N1 _ => false
+  | BigN.N2 _ => false
+  | BigN.N3 _ => false
+  | BigN.N4 _ => false
+  | BigN.N5 _ => false
+  | BigN.N6 _ => false
+  | BigN.N7 _ => false
+  | BigN.N8 _ => false
+  | BigN.N9 _ => true 
+  | BigN.N10 _ => true
+  | BigN.N11 _ => true
+  | BigN.N12 _ => true
+  | BigN.Nn n _ => true
   end.
 
  Definition do_norm_z z :=
   match z with
-  | Z.Pos n => do_norm_n n
-  | Z.Neg n => do_norm_n n
+  | BigZ.Pos n => do_norm_n n
+  | BigZ.Neg n => do_norm_n n
   end.
 
 Require Import Bool.
 (* Je pense que cette fonction normalise bien ... *)
  Definition norm n d :=
   if andb (do_norm_z n) (do_norm_n d) then
-  let gcd := N.gcd (Z.to_N n) d in 
-  match N.compare N.one gcd with
+  let gcd := BigN.gcd (BigZ.to_N n) d in 
+  match BigN.compare BigN.one gcd with
   | Lt => 
-    let n := Z.div n (Z.Pos gcd) in
-    let d := N.div d gcd in
-    match N.compare d N.one with
+    let n := BigZ.div n (BigZ.Pos gcd) in
+    let d := BigN.div d gcd in
+    match BigN.compare d BigN.one with
     | Gt => Qq n d
     | Eq => Qz n
     | Lt => zero
@@ -591,20 +593,20 @@ Require Import Bool.
   match x with
   | Qz zx =>
     match y with
-    | Qz zy => Qz (Z.add zx zy)
+    | Qz zy => Qz (BigZ.add zx zy)
     | Qq ny dy => 
-      if N.eq_bool dy N.zero then x 
-      else Qq (Z.add (Z.mul zx (Z.Pos dy)) ny) dy
+      if BigN.eq_bool dy BigN.zero then x 
+      else Qq (BigZ.add (BigZ.mul zx (BigZ.Pos dy)) ny) dy
     end
   | Qq nx dx =>
-    if N.eq_bool dx N.zero then y 
+    if BigN.eq_bool dx BigN.zero then y 
     else match y with
-    | Qz zy => Qq (Z.add nx (Z.mul zy (Z.Pos dx))) dx
+    | Qz zy => Qq (BigZ.add nx (BigZ.mul zy (BigZ.Pos dx))) dx
     | Qq ny dy =>
-      if N.eq_bool dy N.zero then x
+      if BigN.eq_bool dy BigN.zero then x
       else
-       let n := Z.add (Z.mul nx (Z.Pos dy)) (Z.mul ny (Z.Pos dx)) in
-       let d := N.mul dx dy in
+       let n := BigZ.add (BigZ.mul nx (BigZ.Pos dy)) (BigZ.mul ny (BigZ.Pos dx)) in
+       let d := BigN.mul dx dy in
        Qq n d
     end
   end.
@@ -613,20 +615,20 @@ Require Import Bool.
   match x with
   | Qz zx =>
     match y with
-    | Qz zy => Qz (Z.add zx zy)
+    | Qz zy => Qz (BigZ.add zx zy)
     | Qq ny dy =>  
-      if N.eq_bool dy N.zero then x 
-      else norm (Z.add (Z.mul zx (Z.Pos dy)) ny) dy
+      if BigN.eq_bool dy BigN.zero then x 
+      else norm (BigZ.add (BigZ.mul zx (BigZ.Pos dy)) ny) dy
     end
   | Qq nx dx =>
-    if N.eq_bool dx N.zero then y 
+    if BigN.eq_bool dx BigN.zero then y 
     else match y with
-    | Qz zy => norm (Z.add nx (Z.mul zy (Z.Pos dx))) dx
+    | Qz zy => norm (BigZ.add nx (BigZ.mul zy (BigZ.Pos dx))) dx
     | Qq ny dy =>
-      if N.eq_bool dy N.zero then x
+      if BigN.eq_bool dy BigN.zero then x
       else
-       let n := Z.add (Z.mul nx (Z.Pos dy)) (Z.mul ny (Z.Pos dx)) in
-       let d := N.mul dx dy in
+       let n := BigZ.add (BigZ.mul nx (BigZ.Pos dy)) (BigZ.mul ny (BigZ.Pos dx)) in
+       let d := BigN.mul dx dy in
        norm n d
     end
   end.
@@ -637,50 +639,50 @@ Require Import Bool.
 
  Definition mul x y :=
   match x, y with
-  | Qz zx, Qz zy => Qz (Z.mul zx zy)
-  | Qz zx, Qq ny dy => Qq (Z.mul zx ny) dy
-  | Qq nx dx, Qz zy => Qq (Z.mul nx zy) dx
-  | Qq nx dx, Qq ny dy => Qq (Z.mul nx ny) (N.mul dx dy)
+  | Qz zx, Qz zy => Qz (BigZ.mul zx zy)
+  | Qz zx, Qq ny dy => Qq (BigZ.mul zx ny) dy
+  | Qq nx dx, Qz zy => Qq (BigZ.mul nx zy) dx
+  | Qq nx dx, Qq ny dy => Qq (BigZ.mul nx ny) (BigN.mul dx dy)
   end.
 
  Definition mul_norm x y := 
   match x, y with
-  | Qz zx, Qz zy => Qz (Z.mul zx zy)
-  | Qz zx, Qq ny dy => norm (Z.mul zx ny) dy
-  | Qq nx dx, Qz zy => norm (Z.mul nx zy) dx
-  | Qq nx dx, Qq ny dy => norm (Z.mul nx ny) (N.mul dx dy)
+  | Qz zx, Qz zy => Qz (BigZ.mul zx zy)
+  | Qz zx, Qq ny dy => norm (BigZ.mul zx ny) dy
+  | Qq nx dx, Qz zy => norm (BigZ.mul nx zy) dx
+  | Qq nx dx, Qq ny dy => norm (BigZ.mul nx ny) (BigN.mul dx dy)
   end.
 
  Definition inv x := 
   match x with
-  | Qz (Z.Pos n) => Qq Z.one n
-  | Qz (Z.Neg n) => Qq Z.minus_one n
-  | Qq (Z.Pos n) d => Qq (Z.Pos d) n
-  | Qq (Z.Neg n) d => Qq (Z.Neg d) n
+  | Qz (BigZ.Pos n) => Qq BigZ.one n
+  | Qz (BigZ.Neg n) => Qq BigZ.minus_one n
+  | Qq (BigZ.Pos n) d => Qq (BigZ.Pos d) n
+  | Qq (BigZ.Neg n) d => Qq (BigZ.Neg d) n
   end.
 
  Definition inv_norm x := 
   match x with
-  | Qz (Z.Pos n) => 
-    if N.eq_bool n N.zero then zero else Qq Z.one n
-  | Qz (Z.Neg n) => 
-    if N.eq_bool n N.zero then zero else Qq Z.minus_one n
-  | Qq (Z.Pos n) d => 
-    if N.eq_bool n N.zero then zero else Qq (Z.Pos d) n
-  | Qq (Z.Neg n) d => 
-    if N.eq_bool n N.zero then zero else Qq (Z.Neg d) n
+  | Qz (BigZ.Pos n) => 
+    if BigN.eq_bool n BigN.zero then zero else Qq BigZ.one n
+  | Qz (BigZ.Neg n) => 
+    if BigN.eq_bool n BigN.zero then zero else Qq BigZ.minus_one n
+  | Qq (BigZ.Pos n) d => 
+    if BigN.eq_bool n BigN.zero then zero else Qq (BigZ.Pos d) n
+  | Qq (BigZ.Neg n) d => 
+    if BigN.eq_bool n BigN.zero then zero else Qq (BigZ.Neg d) n
   end.
 
  Definition square x :=
   match x with
-  | Qz zx => Qz (Z.square zx)
-  | Qq nx dx => Qq (Z.square nx) (N.square dx)
+  | Qz zx => Qz (BigZ.square zx)
+  | Qq nx dx => Qq (BigZ.square nx) (BigN.square dx)
   end.
 
  Definition power_pos x p :=
   match x with
-  | Qz zx => Qz (Z.power_pos zx p)
-  | Qq nx dx => Qq (Z.power_pos nx p) (N.power_pos dx p)
+  | Qz zx => Qz (BigZ.power_pos zx p)
+  | Qq nx dx => Qq (BigZ.power_pos nx p) (BigN.power_pos dx p)
   end.
 
 End Qif.
@@ -698,85 +700,85 @@ Module Qbi.
 
  Definition t := q_type.
 
- Definition zero := Qz Z.zero.
- Definition one  := Qz Z.one.
- Definition minus_one := Qz Z.minus_one.
+ Definition zero := Qz BigZ.zero.
+ Definition one  := Qz BigZ.one.
+ Definition minus_one := Qz BigZ.minus_one.
 
- Definition of_Z x := Qz (Z.of_Z x).
+ Definition of_Z x := Qz (BigZ.of_Z x).
 
  Definition compare x y :=
   match x, y with
-  | Qz zx, Qz zy => Z.compare zx zy
+  | Qz zx, Qz zy => BigZ.compare zx zy
   | Qz zx, Qq ny dy => 
-    if N.eq_bool dy N.zero then Z.compare zx Z.zero
+    if BigN.eq_bool dy BigN.zero then BigZ.compare zx BigZ.zero
     else
-      match Z.cmp_sign zx ny with
+      match BigZ.cmp_sign zx ny with
       | Lt => Lt 
       | Gt => Gt
-      | Eq => Z.compare (Z.mul zx (Z.Pos dy)) ny
+      | Eq => BigZ.compare (BigZ.mul zx (BigZ.Pos dy)) ny
       end
   | Qq nx dx, Qz zy =>
-    if N.eq_bool dx N.zero then Z.compare Z.zero zy     
+    if BigN.eq_bool dx BigN.zero then BigZ.compare BigZ.zero zy     
     else
-      match Z.cmp_sign nx zy with
+      match BigZ.cmp_sign nx zy with
       | Lt => Lt
       | Gt => Gt
-      | Eq => Z.compare nx (Z.mul zy (Z.Pos dx))
+      | Eq => BigZ.compare nx (BigZ.mul zy (BigZ.Pos dx))
       end
   | Qq nx dx, Qq ny dy =>
-    match N.eq_bool dx N.zero, N.eq_bool dy N.zero with
+    match BigN.eq_bool dx BigN.zero, BigN.eq_bool dy BigN.zero with
     | true, true => Eq
-    | true, false => Z.compare Z.zero ny
-    | false, true => Z.compare nx Z.zero
+    | true, false => BigZ.compare BigZ.zero ny
+    | false, true => BigZ.compare nx BigZ.zero
     | false, false =>
-      match Z.cmp_sign nx ny with
+      match BigZ.cmp_sign nx ny with
       | Lt => Lt
       | Gt => Gt
-      | Eq => Z.compare (Z.mul nx (Z.Pos dy)) (Z.mul ny (Z.Pos dx))
+      | Eq => BigZ.compare (BigZ.mul nx (BigZ.Pos dy)) (BigZ.mul ny (BigZ.Pos dx))
       end
     end
   end.
 
  Definition opp x :=
   match x with
-  | Qz zx => Qz (Z.opp zx)
-  | Qq nx dx => Qq (Z.opp nx) dx
+  | Qz zx => Qz (BigZ.opp zx)
+  | Qq nx dx => Qq (BigZ.opp nx) dx
   end.
 
 
  Definition do_norm_n n := 
   match n with
-  | N.N0 _ => false
-  | N.N1 _ => false
-  | N.N2 _ => false
-  | N.N3 _ => false
-  | N.N4 _ => false
-  | N.N5 _ => false
-  | N.N6 _ => false
-  | N.N7 _ => false
-  | N.N8 _ => false
-  | N.N9 _ => true 
-  | N.N10 _ => true
-  | N.N11 _ => true
-  | N.N12 _ => true
-  | N.Nn n _ => true
+  | BigN.N0 _ => false
+  | BigN.N1 _ => false
+  | BigN.N2 _ => false
+  | BigN.N3 _ => false
+  | BigN.N4 _ => false
+  | BigN.N5 _ => false
+  | BigN.N6 _ => false
+  | BigN.N7 _ => false
+  | BigN.N8 _ => false
+  | BigN.N9 _ => true 
+  | BigN.N10 _ => true
+  | BigN.N11 _ => true
+  | BigN.N12 _ => true
+  | BigN.Nn n _ => true
   end.
  
  Definition do_norm_z z :=
   match z with
-  | Z.Pos n => do_norm_n n
-  | Z.Neg n => do_norm_n n
+  | BigZ.Pos n => do_norm_n n
+  | BigZ.Neg n => do_norm_n n
   end.
 
 (* Je pense que cette fonction normalise bien ... *)
  Definition norm n d :=
   if andb (do_norm_z n) (do_norm_n d) then
-  let gcd := N.gcd (Z.to_N n) d in 
-  match N.compare N.one gcd with
+  let gcd := BigN.gcd (BigZ.to_N n) d in 
+  match BigN.compare BigN.one gcd with
   | Lt => 
-    let n := Z.div n (Z.Pos gcd) in
-    let d := N.div d gcd in
-    match N.compare d N.one with
+    let n := BigZ.div n (BigZ.Pos gcd) in
+    let d := BigN.div d gcd in
+    match BigN.compare d BigN.one with
     | Gt => Qq n d
     | Eq => Qz n
     | Lt => zero
@@ -791,24 +793,24 @@ Module Qbi.
   match x with
   | Qz zx =>
     match y with
-    | Qz zy => Qz (Z.add zx zy)
+    | Qz zy => Qz (BigZ.add zx zy)
     | Qq ny dy => 
-      if N.eq_bool dy N.zero then x 
-      else Qq (Z.add (Z.mul zx (Z.Pos dy)) ny) dy
+      if BigN.eq_bool dy BigN.zero then x 
+      else Qq (BigZ.add (BigZ.mul zx (BigZ.Pos dy)) ny) dy
     end
   | Qq nx dx =>
-    if N.eq_bool dx N.zero then y 
+    if BigN.eq_bool dx BigN.zero then y 
     else match y with
-    | Qz zy => Qq (Z.add nx (Z.mul zy (Z.Pos dx))) dx
+    | Qz zy => Qq (BigZ.add nx (BigZ.mul zy (BigZ.Pos dx))) dx
     | Qq ny dy =>
-      if N.eq_bool dy N.zero then x
+      if BigN.eq_bool dy BigN.zero then x
       else
-       if N.eq_bool dx dy then
-         let n := Z.add nx ny in
+       if BigN.eq_bool dx dy then
+         let n := BigZ.add nx ny in
          Qq n dx
        else
-         let n := Z.add (Z.mul nx (Z.Pos dy)) (Z.mul ny (Z.Pos dx)) in
-         let d := N.mul dx dy in
+         let n := BigZ.add (BigZ.mul nx (BigZ.Pos dy)) (BigZ.mul ny (BigZ.Pos dx)) in
+         let d := BigN.mul dx dy in
          Qq n d
     end
   end.
@@ -817,25 +819,25 @@ Module Qbi.
   match x with
   | Qz zx =>
     match y with
-    | Qz zy => Qz (Z.add zx zy)
+    | Qz zy => Qz (BigZ.add zx zy)
     | Qq ny dy =>  
-      if N.eq_bool dy N.zero then x 
+      if BigN.eq_bool dy BigN.zero then x 
       else 
-        norm (Z.add (Z.mul zx (Z.Pos dy)) ny) dy
+        norm (BigZ.add (BigZ.mul zx (BigZ.Pos dy)) ny) dy
     end
   | Qq nx dx =>
-    if N.eq_bool dx N.zero then y 
+    if BigN.eq_bool dx BigN.zero then y 
     else match y with
-    | Qz zy => norm (Z.add nx (Z.mul zy (Z.Pos dx))) dx
+    | Qz zy => norm (BigZ.add nx (BigZ.mul zy (BigZ.Pos dx))) dx
     | Qq ny dy =>
-      if N.eq_bool dy N.zero then x
+      if BigN.eq_bool dy BigN.zero then x
       else
-       if N.eq_bool dx dy then
-         let n := Z.add nx ny in
+       if BigN.eq_bool dx dy then
+         let n := BigZ.add nx ny in
          norm n dx
        else
-         let n := Z.add (Z.mul nx (Z.Pos dy)) (Z.mul ny (Z.Pos dx)) in
-         let d := N.mul dx dy in
+         let n := BigZ.add (BigZ.mul nx (BigZ.Pos dy)) (BigZ.mul ny (BigZ.Pos dx)) in
+         let d := BigN.mul dx dy in
          norm n d
     end
   end.
@@ -846,15 +848,15 @@ Module Qbi.
 
  Definition mul x y :=
   match x, y with
-  | Qz zx, Qz zy => Qz (Z.mul zx zy)
-  | Qz zx, Qq ny dy => Qq (Z.mul zx ny) dy
-  | Qq nx dx, Qz zy => Qq (Z.mul nx zy) dx
-  | Qq nx dx, Qq ny dy => Qq (Z.mul nx ny) (N.mul dx dy)
+  | Qz zx, Qz zy => Qz (BigZ.mul zx zy)
+  | Qz zx, Qq ny dy => Qq (BigZ.mul zx ny) dy
+  | Qq nx dx, Qz zy => Qq (BigZ.mul nx zy) dx
+  | Qq nx dx, Qq ny dy => Qq (BigZ.mul nx ny) (BigN.mul dx dy)
   end.
 
  Definition mul_norm x y := 
   match x, y with
-  | Qz zx, Qz zy => Qz (Z.mul zx zy)
+  | Qz zx, Qz zy => Qz (BigZ.mul zx zy)
   | Qz zx, Qq ny dy => mul (Qz ny) (norm zx dy)
   | Qq nx dx, Qz zy => mul (Qz nx) (norm zy dx)
   | Qq nx dx, Qq ny dy => mul (norm nx dy) (norm ny dx)
@@ -862,34 +864,34 @@ Module Qbi.
 
  Definition inv x := 
   match x with
-  | Qz (Z.Pos n) => Qq Z.one n
-  | Qz (Z.Neg n) => Qq Z.minus_one n
-  | Qq (Z.Pos n) d => Qq (Z.Pos d) n
-  | Qq (Z.Neg n) d => Qq (Z.Neg d) n
+  | Qz (BigZ.Pos n) => Qq BigZ.one n
+  | Qz (BigZ.Neg n) => Qq BigZ.minus_one n
+  | Qq (BigZ.Pos n) d => Qq (BigZ.Pos d) n
+  | Qq (BigZ.Neg n) d => Qq (BigZ.Neg d) n
   end.
 
  Definition inv_norm x := 
   match x with
-  | Qz (Z.Pos n) => 
-    if N.eq_bool n N.zero then zero else Qq Z.one n
-  | Qz (Z.Neg n) => 
-    if N.eq_bool n N.zero then zero else Qq Z.minus_one n
-  | Qq (Z.Pos n) d => 
-    if N.eq_bool n N.zero then zero else Qq (Z.Pos d) n
-  | Qq (Z.Neg n) d => 
-    if N.eq_bool n N.zero then zero else Qq (Z.Neg d) n
+  | Qz (BigZ.Pos n) => 
+    if BigN.eq_bool n BigN.zero then zero else Qq BigZ.one n
+  | Qz (BigZ.Neg n) => 
+    if BigN.eq_bool n BigN.zero then zero else Qq BigZ.minus_one n
+  | Qq (BigZ.Pos n) d => 
+    if BigN.eq_bool n BigN.zero then zero else Qq (BigZ.Pos d) n
+  | Qq (BigZ.Neg n) d => 
+    if BigN.eq_bool n BigN.zero then zero else Qq (BigZ.Neg d) n
   end.
 
  Definition square x :=
   match x with
-  | Qz zx => Qz (Z.square zx)
-  | Qq nx dx => Qq (Z.square nx) (N.square dx)
+  | Qz zx => Qz (BigZ.square zx)
+  | Qq nx dx => Qq (BigZ.square nx) (BigN.square dx)
   end.
 
  Definition power_pos x p :=
   match x with
-  | Qz zx => Qz (Z.power_pos zx p)
-  | Qq nx dx => Qq (Z.power_pos nx p) (N.power_pos dx p)
+  | Qz zx => Qz (BigZ.power_pos zx p)
+  | Qq nx dx => Qq (BigZ.power_pos nx p) (BigN.power_pos dx p)
   end.
 
 End Qbi.