Report des quelques modifs faites avec Pierre Letouzey sur les

fichiers en attendant une intégration à theories/Numbers



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

24 files changed, 220 insertions, 82 deletions

diff --git a/theories/Ints/Basic_type.v b/theories/Ints/Basic_type.v
index 72a027cb6..2116aaddd 100644
--- a/theories/Ints/Basic_type.v
+++ b/theories/Ints/Basic_type.v
@@ -1,3 +1,10 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 (*************************************************************)
 (*      This file is distributed under the terms of the      *)
diff --git a/theories/Ints/BigN.v b/theories/Ints/BigN.v
index e8b92186b..b64a853fd 100644
--- a/theories/Ints/BigN.v
+++ b/theories/Ints/BigN.v
@@ -1,3 +1,17 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** * Natural numbers in base 2^31 *)
+
+(**
+Author: Arnaud Spiwack
+*)
+
 Require Export Int31.
 Require Import NMake.
 Require Import ZnZ.
@@ -90,7 +104,7 @@ Defined.
 Definition int31_spec : znz_spec int31_op.
 Admitted.
 
- 
+
 
 Module Int31_words <: W0Type.
   Definition w := int31.
diff --git a/theories/Ints/Z/ZAux.v b/theories/Ints/Zaux.v
index 8e4b1d64f..8e4b1d64f 100644
--- a/theories/Ints/Z/ZAux.v
+++ b/theories/Ints/Zaux.v
diff --git a/theories/Ints/num/BigQ.v b/theories/Ints/num/BigQ.v
index bd889e12f..33e5f669c 100644
--- a/theories/Ints/num/BigQ.v
+++ b/theories/Ints/num/BigQ.v
@@ -1,3 +1,13 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* *)
+
 Require Export QMake_base.
 Require Import QpMake.
 Require Import QvMake.
diff --git a/theories/Ints/num/GenAdd.v b/theories/Ints/num/GenAdd.v
index 77f5e2301..fae16aad6 100644
--- a/theories/Ints/num/GenAdd.v
+++ b/theories/Ints/num/GenAdd.v
@@ -1,3 +1,10 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 (*************************************************************)
 (*      This file is distributed under the terms of the      *)
@@ -9,7 +16,7 @@
 Set Implicit Arguments.
 
 Require Import ZArith.
-Require Import ZAux.
+Require Import Zaux.
 Require Import Basic_type.
 Require Import GenBase.
 
diff --git a/theories/Ints/num/GenBase.v b/theories/Ints/num/GenBase.v
index a9936f1dd..e93e3a489 100644
--- a/theories/Ints/num/GenBase.v
+++ b/theories/Ints/num/GenBase.v
@@ -1,15 +1,26 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
-(*************************************************************)
-(*      This file is distributed under the terms of the      *)
-(*      GNU Lesser General Public License Version 2.1        *)
-(*************************************************************)
-(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
-(*************************************************************)
+(* $Id:$ *)
+
+(** * *)
+
+(** 
+- Authors: Benjamin Grégoire, Laurent Théry
+- Institution: INRIA
+- Date: 2007
+- Remark: File automatically generated
+*)
 
 Set Implicit Arguments.
 
 Require Import ZArith.
-Require Import ZAux.
+Require Import Zaux.
 Require Import Basic_type.
 Require Import JMeq.
 
diff --git a/theories/Ints/num/GenDiv.v b/theories/Ints/num/GenDiv.v
index 237adb48b..ea6868a90 100644
--- a/theories/Ints/num/GenDiv.v
+++ b/theories/Ints/num/GenDiv.v
@@ -9,7 +9,7 @@
 Set Implicit Arguments.
 
 Require Import ZArith.
-Require Import ZAux.
+Require Import Zaux.
 Require Import Basic_type.
 Require Import GenBase.
 Require Import GenDivn1.
diff --git a/theories/Ints/num/GenDivn1.v b/theories/Ints/num/GenDivn1.v
index 7987741da..3c70adb61 100644
--- a/theories/Ints/num/GenDivn1.v
+++ b/theories/Ints/num/GenDivn1.v
@@ -9,7 +9,7 @@
 Set Implicit Arguments.
 
 Require Import ZArith.
-Require Import ZAux.
+Require Import Zaux.
 Require Import Basic_type.
 Require Import GenBase.
 
diff --git a/theories/Ints/num/GenLift.v b/theories/Ints/num/GenLift.v
index 06c76067e..f74cdc30b 100644
--- a/theories/Ints/num/GenLift.v
+++ b/theories/Ints/num/GenLift.v
@@ -9,7 +9,7 @@
 Set Implicit Arguments.
 
 Require Import ZArith.
-Require Import ZAux.
+Require Import Zaux.
 Require Import Basic_type.
 Require Import GenBase.
 
diff --git a/theories/Ints/num/GenMul.v b/theories/Ints/num/GenMul.v
index c7ac1ea3e..9a56f1ee3 100644
--- a/theories/Ints/num/GenMul.v
+++ b/theories/Ints/num/GenMul.v
@@ -9,7 +9,7 @@
 Set Implicit Arguments.
 
 Require Import ZArith.
-Require Import ZAux.
+Require Import Zaux.
 Require Import Basic_type.
 Require Import GenBase.
 
diff --git a/theories/Ints/num/GenSqrt.v b/theories/Ints/num/GenSqrt.v
index d1ed6353d..63a0930ed 100644
--- a/theories/Ints/num/GenSqrt.v
+++ b/theories/Ints/num/GenSqrt.v
@@ -9,7 +9,7 @@
 Set Implicit Arguments.
 
 Require Import ZArith.
-Require Import ZAux.
+Require Import Zaux.
 Require Import Basic_type.
 Require Import GenBase.
 
diff --git a/theories/Ints/num/GenSub.v b/theories/Ints/num/GenSub.v
index 9b0924853..6ffb24575 100644
--- a/theories/Ints/num/GenSub.v
+++ b/theories/Ints/num/GenSub.v
@@ -9,7 +9,7 @@
 Set Implicit Arguments.
 
 Require Import ZArith.
-Require Import ZAux.
+Require Import Zaux.
 Require Import Basic_type.
 Require Import GenBase.
 
diff --git a/theories/Ints/num/MemoFn.v b/theories/Ints/num/MemoFn.v
index 7f3703a1b..7d2c7af01 100644
--- a/theories/Ints/num/MemoFn.v
+++ b/theories/Ints/num/MemoFn.v
@@ -1,3 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 Require Import Eqdep_dec.
 
 Section MemoFunction.
diff --git a/theories/Ints/num/NMake.v b/theories/Ints/num/NMake.v
index 5cc8f0284..c857da385 100644
--- a/theories/Ints/num/NMake.v
+++ b/theories/Ints/num/NMake.v
@@ -1,4 +1,23 @@
-Require Import ZAux.
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+(** * *)
+
+(** 
+- Authors: Benjamin Grégoire, Laurent Théry
+- Institution: INRIA
+- Date: 2007
+- Remark: File automatically generated
+*)
+
+Require Import Zaux.
 Require Import ZArith.
 Require Import Basic_type.
 Require Import ZnZ.
@@ -9,20 +28,6 @@ Require Import GenDivn1.
 Require Import Wf_nat.
 Require Import MemoFn.
 
-(***************************************************************)
-(*                                                             *)
-(*        File automatically generated DO NOT EDIT             *)
-(*        Constructors: 6  Generated Proofs: true              *)
-(*                                                             *)
-(*  To change this file, edit in genN.ml the two lines         *)
-(*   let size = 6                                              *)
-(*   let gen_proof = true                                      *)
-(*  Recompile the file                                         *)
-(*   camlopt -o genN unix.cmxa genN.ml                         *)
-(*  Regenerate NMake.v                                         *)
-(*   ./genN                                                    *)
-(***************************************************************)
-
 Module Type W0Type.
  Parameter w : Set.
  Parameter w_op : znz_op w.
@@ -6796,4 +6801,3 @@ Qed.
  Qed.
 
 End Make.
-
diff --git a/theories/Ints/num/Nbasic.v b/theories/Ints/num/Nbasic.v
index 0d85c92ed..1398e8f55 100644
--- a/theories/Ints/num/Nbasic.v
+++ b/theories/Ints/num/Nbasic.v
@@ -1,5 +1,13 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 Require Import ZArith.
-Require Import ZAux.
+Require Import Zaux.
 Require Import Basic_type.
 Require Import Max.
 Require Import GenBase.
diff --git a/theories/Ints/num/Q0Make.v b/theories/Ints/num/Q0Make.v
index c39a63301..d5809ea59 100644
--- a/theories/Ints/num/Q0Make.v
+++ b/theories/Ints/num/Q0Make.v
@@ -1,7 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 Require Import Bool.
 Require Import ZArith.
 Require Import Znumtheory.
-Require Import ZAux.
+Require Import Zaux.
 Require Import Arith.
 Require Export BigN.
 Require Export BigZ.
@@ -12,11 +20,10 @@ Require Import QMake_base.
 
 Module Q0.
 
- (* Troisieme solution :
-    0 a de nombreuse representation :
-         0, -0, 1/0, ... n/0,
-    il faut alors faire attention avec la comparaison et l'addition 
- *)
+ (** The notation of a rational number is either an integer x,
+     interpreted as itself or a pair (x,y) of an integer x and a naturel
+     number y interpreted as x/y. The pairs (x,0) and (0,y) are all
+     interpreted as 0. *)
 
  Definition t := q_type.
 
diff --git a/theories/Ints/num/QMake_base.v b/theories/Ints/num/QMake_base.v
index f82c5d25b..0cd2d2122 100644
--- a/theories/Ints/num/QMake_base.v
+++ b/theories/Ints/num/QMake_base.v
@@ -1,15 +1,30 @@
-Require Export BigN.
-Require Export BigZ.
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
 
+(** * An implementation of rational numbers based on big integers *)
 
+(** 
+- Authors: Benjamin Grégoire, Laurent Théry
+- Institution: INRIA
+- Date: 2007
+*)
+
+Require Export BigN.
+Require Export BigZ.
 
 (* Basic type for Q: a Z or a pair of a Z and an N *)
+
 Inductive q_type : Set := 
  | Qz : BigZ.t -> q_type
  | Qq : BigZ.t -> BigN.t -> q_type.
 
-
-
 Definition print_type x := 
  match x with
  | Qz _ => Z
diff --git a/theories/Ints/num/QbiMake.v b/theories/Ints/num/QbiMake.v
index 9eb5de5e1..a98fda9d7 100644
--- a/theories/Ints/num/QbiMake.v
+++ b/theories/Ints/num/QbiMake.v
@@ -1,7 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 Require Import Bool.
 Require Import ZArith.
 Require Import Znumtheory.
-Require Import ZAux.
+Require Import Zaux.
 Require Import Arith.
 Require Export BigN.
 Require Export BigZ.
@@ -12,18 +20,14 @@ Require Import QMake_base.
 
 Module Qbi.
 
- (* Troisieme solution :
-    0 a de nombreuse representation :
-         0, -0, 1/0, ... n/0,
-    il faut alors faire attention avec la comparaison et l'addition 
-    
-    Les fonctions de normalization s'effectue seulement si les
-    nombres sont grands.
- *)
+ (** The notation of a rational number is either an integer x,
+     interpreted as itself or a pair (x,y) of an integer x and a naturel
+     number y interpreted as x/y. The pairs (x,0) and (0,y) are all
+     interpreted as 0. *)
 
  Definition t := q_type.
 
- Definition zero:t := Qz BigZ.zero.
+ Definition zero: t := Qz BigZ.zero.
  Definition one: t  := Qz BigZ.one.
  Definition minus_one: t := Qz BigZ.minus_one.
 
@@ -1052,7 +1056,3 @@ Module Qbi.
 
 
 End Qbi.
-
-
-
-
diff --git a/theories/Ints/num/QifMake.v b/theories/Ints/num/QifMake.v
index c5fc42520..83c182ee0 100644
--- a/theories/Ints/num/QifMake.v
+++ b/theories/Ints/num/QifMake.v
@@ -1,7 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 Require Import Bool.
 Require Import ZArith.
 Require Import Znumtheory.
-Require Import ZAux.
+Require Import Zaux.
 Require Import Arith.
 Require Export BigN.
 Require Export BigZ.
@@ -12,19 +20,15 @@ Require Import QMake_base.
 
 Module Qif.
 
- (* Troisieme solution :
-    0 a de nombreuse representation :
-         0, -0, 1/0, ... n/0,
-    il faut alors faire attention avec la comparaison et l'addition 
-    
-    Les fonctions de normalization s'effectue seulement si les
-    nombres sont grands.
- *)
+ (** The notation of a rational number is either an integer x,
+     interpreted as itself or a pair (x,y) of an integer x and a naturel
+     number y interpreted as x/y. The pairs (x,0) and (0,y) are all
+     interpreted as 0. *)
 
  Definition t := q_type.
 
  Definition zero: t := Qz BigZ.zero.
- Definition one: t  := Qz BigZ.one.
+ Definition one: t := Qz BigZ.one.
  Definition minus_one: t := Qz BigZ.minus_one.
 
  Definition of_Z x: t := Qz (BigZ.of_Z x).
diff --git a/theories/Ints/num/QpMake.v b/theories/Ints/num/QpMake.v
index 906cf8d15..a28434baf 100644
--- a/theories/Ints/num/QpMake.v
+++ b/theories/Ints/num/QpMake.v
@@ -1,7 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 Require Import Bool.
 Require Import ZArith.
 Require Import Znumtheory.
-Require Import ZAux.
+Require Import Zaux.
 Require Import Arith.
 Require Export BigN.
 Require Export BigZ.
@@ -10,9 +18,12 @@ Require Import Qcanon.
 Require Import Qpower.
 Require Import QMake_base.
 
-
 Module Qp.
 
+ (** The notation of a rational number is either an integer x,
+     interpreted as itself or a pair (x,y) of an integer x and a naturel
+     number y interpreted as x/(y+1). *)
+
  Definition t := q_type.
 
  Definition zero: t := Qz BigZ.zero.
diff --git a/theories/Ints/num/QvMake.v b/theories/Ints/num/QvMake.v
index c3db44bc6..85655dafc 100644
--- a/theories/Ints/num/QvMake.v
+++ b/theories/Ints/num/QvMake.v
@@ -1,7 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 Require Import Bool.
 Require Import ZArith.
 Require Import Znumtheory.
-Require Import ZAux.
+Require Import Zaux.
 Require Import Arith.
 Require Export BigN.
 Require Export BigZ.
@@ -12,8 +20,10 @@ Require Import QMake_base.
 
 Module Qv.
 
- (* /!\  Invariant maintenu par les fonctions :
-         - le denominateur n'est jamais nul *)
+ (** The notation of a rational number is either an integer x,
+     interpreted as itself or a pair (x,y) of an integer x and a naturel
+     number y interpreted as x/y. All functions maintain the invariant
+     that y is never zero. *)
 
  Definition t := q_type.
 
diff --git a/theories/Ints/num/ZMake.v b/theories/Ints/num/ZMake.v
index d00f14ec6..75fc19584 100644
--- a/theories/Ints/num/ZMake.v
+++ b/theories/Ints/num/ZMake.v
@@ -1,5 +1,13 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 Require Import ZArith.
-Require Import ZAux.
+Require Import Zaux.
 
 Open Scope Z_scope.
 
diff --git a/theories/Ints/num/Zn2Z.v b/theories/Ints/num/Zn2Z.v
index a244635ea..48cf26840 100644
--- a/theories/Ints/num/Zn2Z.v
+++ b/theories/Ints/num/Zn2Z.v
@@ -9,7 +9,7 @@
 Set Implicit Arguments.
 
 Require Import ZArith.
-Require Import ZAux.
+Require Import Zaux.
 Require Import Basic_type.
 Require Import GenBase.
 Require Import GenAdd.
diff --git a/theories/Ints/num/ZnZ.v b/theories/Ints/num/ZnZ.v
index 61d1ced60..d5b798a18 100644
--- a/theories/Ints/num/ZnZ.v
+++ b/theories/Ints/num/ZnZ.v
@@ -1,10 +1,22 @@
-
-(*************************************************************)
-(*      This file is distributed under the terms of the      *)
-(*      GNU Lesser General Public License Version 2.1        *)
-(*************************************************************)
-(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
-(*************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*        Benjamin Gregoire, INRIA          Laurent Thery, INRIA        *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+(** * Signature and specification of a bounded integer structure *)
+
+(** 
+- Authors: Benjamin Grégoire, Laurent Théry
+- Institution: INRIA
+- Date: 2007
+*)
 
 Set Implicit Arguments.
 
@@ -20,6 +32,7 @@ Section ZnZ_Op.
  Variable znz : Set.
 
  Record znz_op : Set := mk_znz_op {
+
     (* Conversion functions with Z *)
     znz_digits : positive;
     znz_zdigits: znz;
@@ -27,6 +40,7 @@ Section ZnZ_Op.
     znz_of_pos : positive -> N * znz;
     znz_head0  : znz -> znz;
     znz_tail0  : znz -> znz;
+
     (* Basic constructors *)
     znz_0   : znz;
     znz_1   : znz;
@@ -42,7 +56,7 @@ Section ZnZ_Op.
     (* Basic arithmetic operations *)
     znz_opp_c       : znz -> carry znz;
     znz_opp         : znz -> znz;
-    znz_opp_carry   : znz -> znz; (* the carry is know to be -1 *)
+    znz_opp_carry   : znz -> znz; (* the carry is known to be -1 *)
 
     znz_succ_c      : znz -> carry znz;
     znz_add_c       : znz -> znz -> carry znz;
@@ -87,7 +101,7 @@ Section Spec.
  Variable w_op : znz_op w.
 
  Let w_digits      := w_op.(znz_digits).
- Let w_zdigits      := w_op.(znz_zdigits).
+ Let w_zdigits     := w_op.(znz_zdigits).
  Let w_to_Z        := w_op.(znz_to_Z).
  Let w_of_pos      := w_op.(znz_of_pos).
  Let w_head0       := w_op.(znz_head0).