From 75681234e0ba2ae283cc22c2c3e0c4045b205879 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 27 Apr 2008 16:23:04 +0000
Subject: 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
---
 theories/Ints/Basic_type.v     |   7 +
 theories/Ints/BigN.v           |  16 +-
 theories/Ints/Z/ZAux.v         | 324 -----------------------------------------
 theories/Ints/Zaux.v           | 324 +++++++++++++++++++++++++++++++++++++++++
 theories/Ints/num/BigQ.v       |  10 ++
 theories/Ints/num/GenAdd.v     |   9 +-
 theories/Ints/num/GenBase.v    |  25 +++-
 theories/Ints/num/GenDiv.v     |   2 +-
 theories/Ints/num/GenDivn1.v   |   2 +-
 theories/Ints/num/GenLift.v    |   2 +-
 theories/Ints/num/GenMul.v     |   2 +-
 theories/Ints/num/GenSqrt.v    |   2 +-
 theories/Ints/num/GenSub.v     |   2 +-
 theories/Ints/num/MemoFn.v     |   8 +
 theories/Ints/num/NMake.v      |  36 +++--
 theories/Ints/num/Nbasic.v     |  10 +-
 theories/Ints/num/Q0Make.v     |  19 ++-
 theories/Ints/num/QMake_base.v |  23 ++-
 theories/Ints/num/QbiMake.v    |  28 ++--
 theories/Ints/num/QifMake.v    |  24 +--
 theories/Ints/num/QpMake.v     |  15 +-
 theories/Ints/num/QvMake.v     |  16 +-
 theories/Ints/num/ZMake.v      |  10 +-
 theories/Ints/num/Zn2Z.v       |   2 +-
 theories/Ints/num/ZnZ.v        |  32 ++--
 25 files changed, 544 insertions(+), 406 deletions(-)
 delete mode 100644 theories/Ints/Z/ZAux.v
 create mode 100644 theories/Ints/Zaux.v

diff --git a/theories/Ints/Basic_type.v b/theories/Ints/Basic_type.v
index 72a027cb68..2116aaddd3 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 e8b92186bd..b64a853fd6 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/Z/ZAux.v
deleted file mode 100644
index 8e4b1d64f0..0000000000
--- a/theories/Ints/Z/ZAux.v
+++ /dev/null
@@ -1,324 +0,0 @@
-
-(*************************************************************)
-(*      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      *)
-(*************************************************************)
-
-(**********************************************************************
-     Aux.v
-
-     Auxillary functions & Theorems
- **********************************************************************)
-
-Require Import ArithRing.
-Require Export ZArith.
-Require Export Znumtheory.
-Require Export Zpow_facts.
-
-(* *** Nota Bene ***
-   All results that were general enough has been moved in ZArith.
-   Only remain here specialized lemmas and compatibility elements.
-   (P.L. 5/11/2007).
-*)
-
-
-Open Local Scope Z_scope. 
-
-Hint  Extern 2 (Zle _ _) => 
- (match goal with
-   |- Zpos _ <= Zpos _ => exact (refl_equal _)
-|   H: _ <=  ?p |- _ <= ?p => apply Zle_trans with (2 := H)
-|   H: _ <  ?p |- _ <= ?p => apply Zlt_le_weak; apply Zle_lt_trans with (2 := H)
-  end).
-
-Hint  Extern 2 (Zlt _ _) => 
- (match goal with
-   |- Zpos _ < Zpos _ => exact (refl_equal _)
-|      H: _ <=  ?p |- _ <= ?p => apply Zlt_le_trans with (2 := H)
-|   H: _ <  ?p |- _ <= ?p => apply Zle_lt_trans with (2 := H)
-  end).
-
-
-Hint Resolve Zlt_gt Zle_ge Z_div_pos: zarith.
-
-(************************************** 
-   Properties of order and product
- **************************************)
-
- Theorem beta_lex: forall a b c d beta, 
-       a * beta + b <= c * beta + d -> 
-       0 <= b < beta -> 0 <= d < beta -> 
-       a <= c.
- Proof.
-  intros a b c d beta H1 (H3, H4) (H5, H6).
-  assert (a - c < 1); auto with zarith.
-  apply Zmult_lt_reg_r with beta; auto with zarith.
-  apply Zle_lt_trans with (d  - b); auto with zarith.
-  rewrite Zmult_minus_distr_r; auto with zarith.
- Qed.
-
- Theorem beta_lex_inv: forall a b c d beta,
-      a < c -> 0 <= b < beta ->
-      0 <= d < beta -> 
-      a * beta + b < c * beta  + d. 
- Proof.
-  intros a b c d beta H1 (H3, H4) (H5, H6).
-  case (Zle_or_lt (c * beta + d) (a * beta + b)); auto with zarith.
-  intros H7; contradict H1;apply Zle_not_lt;apply beta_lex with (1 := H7);auto.
- Qed.
-
- Lemma beta_mult : forall h l beta, 
-   0 <= h < beta -> 0 <= l < beta -> 0 <= h*beta+l < beta^2.
- Proof.
-  intros h l beta H1 H2;split. auto with zarith.
-  rewrite <- (Zplus_0_r (beta^2)); rewrite Zpower_2;
-   apply beta_lex_inv;auto with zarith.
- Qed.
-
- Lemma Zmult_lt_b : 
-   forall b x y, 0 <= x < b -> 0 <= y < b -> 0 <= x * y <= b^2 - 2*b + 1.
- Proof.
-  intros b x y (Hx1,Hx2) (Hy1,Hy2);split;auto with zarith.
-  apply Zle_trans with ((b-1)*(b-1)).
-  apply Zmult_le_compat;auto with zarith.
-  apply Zeq_le;ring.
- Qed.
-
- Lemma sum_mul_carry : forall xh xl yh yl wc cc beta,
-   1 < beta -> 
-   0 <= wc < beta ->
-   0 <= xh < beta ->
-   0 <= xl < beta ->
-   0 <= yh < beta ->
-   0 <= yl < beta ->
-   0 <= cc < beta^2 ->
-   wc*beta^2 + cc = xh*yl + xl*yh -> 
-   0 <= wc <= 1.
- Proof.
-  intros xh xl yh yl wc cc beta U H1 H2 H3 H4 H5 H6 H7. 
-  assert (H8 := Zmult_lt_b beta xh yl H2 H5).
-  assert (H9 := Zmult_lt_b beta xl yh H3 H4).
-  split;auto with zarith.
-  apply beta_lex with (cc) (beta^2 - 2) (beta^2); auto with zarith.
- Qed.
-
- Theorem mult_add_ineq: forall x y cross beta,
-   0 <= x < beta ->
-   0 <= y < beta ->
-   0 <= cross < beta ->
-   0 <= x * y + cross < beta^2.
- Proof.
-  intros x y cross beta HH HH1 HH2.
-  split; auto with zarith.
-  apply Zle_lt_trans with  ((beta-1)*(beta-1)+(beta-1)); auto with zarith.
-  apply Zplus_le_compat; auto with zarith.
-  apply Zmult_le_compat; auto with zarith.
-  repeat (rewrite Zmult_minus_distr_l || rewrite Zmult_minus_distr_r); 
-  rewrite Zpower_2; auto with zarith.
- Qed.
-
- Theorem mult_add_ineq2: forall x y c cross beta,
-   0 <= x < beta ->
-   0 <= y < beta ->
-   0 <= c*beta + cross <= 2*beta - 2 ->
-   0 <= x * y + (c*beta + cross) < beta^2.
- Proof.
-  intros x y c cross beta HH HH1 HH2.
-  split; auto with zarith.
-  apply Zle_lt_trans with ((beta-1)*(beta-1)+(2*beta-2));auto with zarith.
-  apply Zplus_le_compat; auto with zarith.
-  apply Zmult_le_compat; auto with zarith.
-  repeat (rewrite Zmult_minus_distr_l || rewrite Zmult_minus_distr_r); 
-   rewrite Zpower_2; auto with zarith.
- Qed.
-
-Theorem mult_add_ineq3: forall x y c cross beta,
-   0 <= x < beta ->
-   0 <= y < beta ->
-   0 <= cross <= beta - 2 ->
-   0 <= c <= 1 ->
-   0 <= x * y + (c*beta + cross) < beta^2.
- Proof.
-  intros x y c cross beta HH HH1 HH2 HH3.
-  apply mult_add_ineq2;auto with zarith.
-  split;auto with zarith.
-  apply Zle_trans with (1*beta+cross);auto with zarith.
- Qed.
-
-Hint Rewrite Zmult_1_r Zmult_0_r Zmult_1_l Zmult_0_l Zplus_0_l Zplus_0_r Zminus_0_r: rm10.
-
-
-(**************************************
- Properties of Zdiv and Zmod
-**************************************)
-
-Theorem Zmod_le_first: forall a b, 0 <= a -> 0 < b -> 0 <= a mod b <= a.
- Proof.
-  intros a b H H1;case (Z_mod_lt a b);auto with zarith;intros H2 H3;split;auto.
-  case (Zle_or_lt b a); intros H4; auto with zarith.
-  rewrite Zmod_small; auto with zarith.
- Qed.
-
-
- Theorem Zmod_distr: forall a b r t, 0 <= a <= b -> 0 <= r -> 0 <= t < 2 ^a ->
-  (2 ^a * r + t) mod (2 ^ b) = (2 ^a * r) mod (2 ^ b) + t.
- Proof.
-  intros a b r t (H1, H2) H3 (H4, H5).
-  assert (t < 2 ^ b).
-  apply Zlt_le_trans with (1:= H5); auto with zarith.
-  apply Zpower_le_monotone; auto with zarith.
-  rewrite Zplus_mod; auto with zarith.
-  rewrite Zmod_small with (a := t); auto with zarith.
-  apply Zmod_small; auto with zarith.
-  split; auto with zarith.
-  assert (0 <= 2 ^a * r); auto with zarith.
-  apply Zplus_le_0_compat; auto with zarith.
-  match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end;
-   auto with zarith.
-  pattern (2 ^ b) at 2; replace (2 ^ b) with ((2 ^ b - 2 ^a) + 2 ^ a);
-    try ring.
-  apply Zplus_le_lt_compat; auto with zarith.
-  replace b with ((b - a) + a); try ring.
-  rewrite Zpower_exp; auto with zarith.
-  pattern (2 ^a) at 4; rewrite <- (Zmult_1_l (2 ^a)); 
-   try rewrite <- Zmult_minus_distr_r.
-  rewrite (Zmult_comm (2 ^(b - a))); rewrite  Zmult_mod_distr_l; 
-   auto with zarith.
-  rewrite (Zmult_comm (2 ^a)); apply Zmult_le_compat_r; auto with zarith.
-  match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end;
-   auto with zarith.
- Qed.
-
- Theorem Zmod_shift_r:
-   forall a b r t, 0 <= a <= b -> 0 <= r -> 0 <= t < 2 ^a ->
-     (r * 2 ^a + t) mod (2 ^ b) = (r * 2 ^a) mod (2 ^ b) + t.
- Proof.
-  intros a b r t (H1, H2) H3 (H4, H5).
-  assert (t < 2 ^ b).
-  apply Zlt_le_trans with (1:= H5); auto with zarith.
-  apply Zpower_le_monotone; auto with zarith.
-  rewrite Zplus_mod; auto with zarith.
-  rewrite Zmod_small with (a := t); auto with zarith.
-  apply Zmod_small; auto with zarith.
-  split; auto with zarith.
-  assert (0 <= 2 ^a * r); auto with zarith.
-  apply Zplus_le_0_compat; auto with zarith.
-  match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end; 
-   auto with zarith.
-  pattern (2 ^ b) at 2;replace (2 ^ b) with ((2 ^ b - 2 ^a) + 2 ^ a); try ring.
-  apply Zplus_le_lt_compat; auto with zarith.
-  replace b with ((b - a) + a); try ring.
-  rewrite Zpower_exp; auto with zarith.
-  pattern (2 ^a) at 4; rewrite <- (Zmult_1_l (2 ^a)); 
-   try rewrite <- Zmult_minus_distr_r.
-  repeat rewrite (fun x => Zmult_comm x (2 ^ a)); rewrite Zmult_mod_distr_l;
-   auto with zarith.
-  apply Zmult_le_compat_l; auto with zarith.
-  match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end; 
-   auto with zarith.
- Qed.
-
-  Theorem Zdiv_shift_r: 
-    forall a b r t, 0 <= a <= b -> 0 <= r -> 0 <= t < 2 ^a ->
-      (r * 2 ^a + t) /  (2 ^ b) = (r * 2 ^a) / (2 ^ b).
-  Proof.
-   intros a b r t (H1, H2) H3 (H4, H5).
-   assert (Eq: t < 2 ^ b); auto with zarith.
-   apply Zlt_le_trans with (1 := H5); auto with zarith.
-   apply Zpower_le_monotone; auto with zarith.
-   pattern (r * 2 ^ a) at 1; rewrite Z_div_mod_eq with (b := 2 ^ b);
-    auto with zarith.
-   rewrite <- Zplus_assoc.
-   rewrite <- Zmod_shift_r; auto with zarith.
-   rewrite (Zmult_comm (2 ^ b)); rewrite Z_div_plus_full_l; auto with zarith.
-   rewrite (fun x y => @Zdiv_small (x mod y)); auto with zarith.
-   match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end; 
-    auto with zarith.
-  Qed.
-
-
- Lemma shift_unshift_mod : forall n p a,
-     0 <= a < 2^n ->
-     0 <= p <= n ->
-     a * 2^p = a / 2^(n - p) * 2^n + (a*2^p) mod 2^n.
- Proof.
-  intros n p a H1 H2.
-  pattern (a*2^p) at 1;replace (a*2^p) with 
-     (a*2^p/2^n * 2^n + a*2^p mod 2^n). 
-  2:symmetry;rewrite (Zmult_comm (a*2^p/2^n));apply Z_div_mod_eq.
-  replace (a * 2 ^ p / 2 ^ n) with (a / 2 ^ (n - p));trivial.
-  replace (2^n) with (2^(n-p)*2^p).
-  symmetry;apply Zdiv_mult_cancel_r.
-  destruct H1;trivial.
-  cut (0 < 2^p); auto with zarith.
-  rewrite <- Zpower_exp.
-  replace (n-p+p) with n;trivial. ring.
-  omega. omega.
-  apply Zlt_gt. apply Zpower_gt_0;auto with zarith.
- Qed.
-
- Lemma div_le_0 : forall p x, 0 <= x -> 0 <= x / 2 ^ p.
- Proof.
-  intros p x Hle;destruct (Z_le_gt_dec 0 p).
-  apply  Zdiv_le_lower_bound;auto with zarith. 
-  replace (2^p) with 0.
-  destruct x;compute;intro;discriminate.
-  destruct p;trivial;discriminate z.
- Qed.
- 
- Lemma div_lt : forall p x y, 0 <= x < y -> x / 2^p < y.
- Proof.
-  intros p x y H;destruct (Z_le_gt_dec 0 p).
-  apply Zdiv_lt_upper_bound;auto with zarith. 
-  apply Zlt_le_trans with y;auto with zarith.
-  rewrite <- (Zmult_1_r y);apply Zmult_le_compat;auto with zarith.
-  assert (0 < 2^p);auto with zarith.
-  replace (2^p) with 0.
-  destruct x;change (0<y);auto with zarith.
-  destruct p;trivial;discriminate z.
- Qed.
-
- Theorem Zgcd_div_pos a b:
-   (0 < b)%Z -> (0 < Zgcd a b)%Z -> (0 < b / Zgcd a b)%Z.
- Proof.
- intros a b Ha Hg.
- case (Zle_lt_or_eq 0 (b/Zgcd a b)); auto.
- apply Z_div_pos; auto with zarith.
- intros H; generalize Ha.
- pattern b at 1; rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto.
- rewrite <- H; auto with zarith.
- assert (F := (Zgcd_is_gcd a b)); inversion F; auto.
- Qed.
- 
-(* For compatibility of scripts, weaker version of some lemmas of Zdiv *)
-
-Lemma Zlt0_not_eq : forall n, 0<n -> n<>0.
-Proof.
- auto with zarith.
-Qed.
-
-Definition Zdiv_mult_cancel_r a b c H := Zdiv.Zdiv_mult_cancel_r a b c (Zlt0_not_eq _ H).
-Definition Zdiv_mult_cancel_l a b c H := Zdiv.Zdiv_mult_cancel_r a b c (Zlt0_not_eq _ H).
-Definition Z_div_plus_l a b c H := Zdiv.Z_div_plus_full_l a b c (Zlt0_not_eq _ H).
-
-Theorem Zbounded_induction :
-  (forall Q : Z -> Prop, forall b : Z,
-    Q 0 ->
-    (forall n, 0 <= n -> n < b - 1 -> Q n -> Q (n + 1)) ->
-      forall n, 0 <= n -> n < b -> Q n)%Z.
-Proof.
-intros Q b Q0 QS.
-set (Q' := fun n => (n < b /\ Q n) \/ (b <= n)).
-assert (H : forall n, 0 <= n -> Q' n).
-apply natlike_rec2; unfold Q'.
-destruct (Zle_or_lt b 0) as [H | H]. now right. left; now split.
-intros n H IH. destruct IH as [[IH1 IH2] | IH].
-destruct (Zle_or_lt (b - 1) n) as [H1 | H1].
-right; auto with zarith.
-left. split; [auto with zarith | now apply (QS n)].
-right; auto with zarith.
-unfold Q' in *; intros n H1 H2. destruct (H n H1) as [[H3 H4] | H3].
-assumption. apply Zle_not_lt in H3. false_hyp H2 H3.
-Qed.
diff --git a/theories/Ints/Zaux.v b/theories/Ints/Zaux.v
new file mode 100644
index 0000000000..8e4b1d64f0
--- /dev/null
+++ b/theories/Ints/Zaux.v
@@ -0,0 +1,324 @@
+
+(*************************************************************)
+(*      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      *)
+(*************************************************************)
+
+(**********************************************************************
+     Aux.v
+
+     Auxillary functions & Theorems
+ **********************************************************************)
+
+Require Import ArithRing.
+Require Export ZArith.
+Require Export Znumtheory.
+Require Export Zpow_facts.
+
+(* *** Nota Bene ***
+   All results that were general enough has been moved in ZArith.
+   Only remain here specialized lemmas and compatibility elements.
+   (P.L. 5/11/2007).
+*)
+
+
+Open Local Scope Z_scope. 
+
+Hint  Extern 2 (Zle _ _) => 
+ (match goal with
+   |- Zpos _ <= Zpos _ => exact (refl_equal _)
+|   H: _ <=  ?p |- _ <= ?p => apply Zle_trans with (2 := H)
+|   H: _ <  ?p |- _ <= ?p => apply Zlt_le_weak; apply Zle_lt_trans with (2 := H)
+  end).
+
+Hint  Extern 2 (Zlt _ _) => 
+ (match goal with
+   |- Zpos _ < Zpos _ => exact (refl_equal _)
+|      H: _ <=  ?p |- _ <= ?p => apply Zlt_le_trans with (2 := H)
+|   H: _ <  ?p |- _ <= ?p => apply Zle_lt_trans with (2 := H)
+  end).
+
+
+Hint Resolve Zlt_gt Zle_ge Z_div_pos: zarith.
+
+(************************************** 
+   Properties of order and product
+ **************************************)
+
+ Theorem beta_lex: forall a b c d beta, 
+       a * beta + b <= c * beta + d -> 
+       0 <= b < beta -> 0 <= d < beta -> 
+       a <= c.
+ Proof.
+  intros a b c d beta H1 (H3, H4) (H5, H6).
+  assert (a - c < 1); auto with zarith.
+  apply Zmult_lt_reg_r with beta; auto with zarith.
+  apply Zle_lt_trans with (d  - b); auto with zarith.
+  rewrite Zmult_minus_distr_r; auto with zarith.
+ Qed.
+
+ Theorem beta_lex_inv: forall a b c d beta,
+      a < c -> 0 <= b < beta ->
+      0 <= d < beta -> 
+      a * beta + b < c * beta  + d. 
+ Proof.
+  intros a b c d beta H1 (H3, H4) (H5, H6).
+  case (Zle_or_lt (c * beta + d) (a * beta + b)); auto with zarith.
+  intros H7; contradict H1;apply Zle_not_lt;apply beta_lex with (1 := H7);auto.
+ Qed.
+
+ Lemma beta_mult : forall h l beta, 
+   0 <= h < beta -> 0 <= l < beta -> 0 <= h*beta+l < beta^2.
+ Proof.
+  intros h l beta H1 H2;split. auto with zarith.
+  rewrite <- (Zplus_0_r (beta^2)); rewrite Zpower_2;
+   apply beta_lex_inv;auto with zarith.
+ Qed.
+
+ Lemma Zmult_lt_b : 
+   forall b x y, 0 <= x < b -> 0 <= y < b -> 0 <= x * y <= b^2 - 2*b + 1.
+ Proof.
+  intros b x y (Hx1,Hx2) (Hy1,Hy2);split;auto with zarith.
+  apply Zle_trans with ((b-1)*(b-1)).
+  apply Zmult_le_compat;auto with zarith.
+  apply Zeq_le;ring.
+ Qed.
+
+ Lemma sum_mul_carry : forall xh xl yh yl wc cc beta,
+   1 < beta -> 
+   0 <= wc < beta ->
+   0 <= xh < beta ->
+   0 <= xl < beta ->
+   0 <= yh < beta ->
+   0 <= yl < beta ->
+   0 <= cc < beta^2 ->
+   wc*beta^2 + cc = xh*yl + xl*yh -> 
+   0 <= wc <= 1.
+ Proof.
+  intros xh xl yh yl wc cc beta U H1 H2 H3 H4 H5 H6 H7. 
+  assert (H8 := Zmult_lt_b beta xh yl H2 H5).
+  assert (H9 := Zmult_lt_b beta xl yh H3 H4).
+  split;auto with zarith.
+  apply beta_lex with (cc) (beta^2 - 2) (beta^2); auto with zarith.
+ Qed.
+
+ Theorem mult_add_ineq: forall x y cross beta,
+   0 <= x < beta ->
+   0 <= y < beta ->
+   0 <= cross < beta ->
+   0 <= x * y + cross < beta^2.
+ Proof.
+  intros x y cross beta HH HH1 HH2.
+  split; auto with zarith.
+  apply Zle_lt_trans with  ((beta-1)*(beta-1)+(beta-1)); auto with zarith.
+  apply Zplus_le_compat; auto with zarith.
+  apply Zmult_le_compat; auto with zarith.
+  repeat (rewrite Zmult_minus_distr_l || rewrite Zmult_minus_distr_r); 
+  rewrite Zpower_2; auto with zarith.
+ Qed.
+
+ Theorem mult_add_ineq2: forall x y c cross beta,
+   0 <= x < beta ->
+   0 <= y < beta ->
+   0 <= c*beta + cross <= 2*beta - 2 ->
+   0 <= x * y + (c*beta + cross) < beta^2.
+ Proof.
+  intros x y c cross beta HH HH1 HH2.
+  split; auto with zarith.
+  apply Zle_lt_trans with ((beta-1)*(beta-1)+(2*beta-2));auto with zarith.
+  apply Zplus_le_compat; auto with zarith.
+  apply Zmult_le_compat; auto with zarith.
+  repeat (rewrite Zmult_minus_distr_l || rewrite Zmult_minus_distr_r); 
+   rewrite Zpower_2; auto with zarith.
+ Qed.
+
+Theorem mult_add_ineq3: forall x y c cross beta,
+   0 <= x < beta ->
+   0 <= y < beta ->
+   0 <= cross <= beta - 2 ->
+   0 <= c <= 1 ->
+   0 <= x * y + (c*beta + cross) < beta^2.
+ Proof.
+  intros x y c cross beta HH HH1 HH2 HH3.
+  apply mult_add_ineq2;auto with zarith.
+  split;auto with zarith.
+  apply Zle_trans with (1*beta+cross);auto with zarith.
+ Qed.
+
+Hint Rewrite Zmult_1_r Zmult_0_r Zmult_1_l Zmult_0_l Zplus_0_l Zplus_0_r Zminus_0_r: rm10.
+
+
+(**************************************
+ Properties of Zdiv and Zmod
+**************************************)
+
+Theorem Zmod_le_first: forall a b, 0 <= a -> 0 < b -> 0 <= a mod b <= a.
+ Proof.
+  intros a b H H1;case (Z_mod_lt a b);auto with zarith;intros H2 H3;split;auto.
+  case (Zle_or_lt b a); intros H4; auto with zarith.
+  rewrite Zmod_small; auto with zarith.
+ Qed.
+
+
+ Theorem Zmod_distr: forall a b r t, 0 <= a <= b -> 0 <= r -> 0 <= t < 2 ^a ->
+  (2 ^a * r + t) mod (2 ^ b) = (2 ^a * r) mod (2 ^ b) + t.
+ Proof.
+  intros a b r t (H1, H2) H3 (H4, H5).
+  assert (t < 2 ^ b).
+  apply Zlt_le_trans with (1:= H5); auto with zarith.
+  apply Zpower_le_monotone; auto with zarith.
+  rewrite Zplus_mod; auto with zarith.
+  rewrite Zmod_small with (a := t); auto with zarith.
+  apply Zmod_small; auto with zarith.
+  split; auto with zarith.
+  assert (0 <= 2 ^a * r); auto with zarith.
+  apply Zplus_le_0_compat; auto with zarith.
+  match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end;
+   auto with zarith.
+  pattern (2 ^ b) at 2; replace (2 ^ b) with ((2 ^ b - 2 ^a) + 2 ^ a);
+    try ring.
+  apply Zplus_le_lt_compat; auto with zarith.
+  replace b with ((b - a) + a); try ring.
+  rewrite Zpower_exp; auto with zarith.
+  pattern (2 ^a) at 4; rewrite <- (Zmult_1_l (2 ^a)); 
+   try rewrite <- Zmult_minus_distr_r.
+  rewrite (Zmult_comm (2 ^(b - a))); rewrite  Zmult_mod_distr_l; 
+   auto with zarith.
+  rewrite (Zmult_comm (2 ^a)); apply Zmult_le_compat_r; auto with zarith.
+  match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end;
+   auto with zarith.
+ Qed.
+
+ Theorem Zmod_shift_r:
+   forall a b r t, 0 <= a <= b -> 0 <= r -> 0 <= t < 2 ^a ->
+     (r * 2 ^a + t) mod (2 ^ b) = (r * 2 ^a) mod (2 ^ b) + t.
+ Proof.
+  intros a b r t (H1, H2) H3 (H4, H5).
+  assert (t < 2 ^ b).
+  apply Zlt_le_trans with (1:= H5); auto with zarith.
+  apply Zpower_le_monotone; auto with zarith.
+  rewrite Zplus_mod; auto with zarith.
+  rewrite Zmod_small with (a := t); auto with zarith.
+  apply Zmod_small; auto with zarith.
+  split; auto with zarith.
+  assert (0 <= 2 ^a * r); auto with zarith.
+  apply Zplus_le_0_compat; auto with zarith.
+  match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end; 
+   auto with zarith.
+  pattern (2 ^ b) at 2;replace (2 ^ b) with ((2 ^ b - 2 ^a) + 2 ^ a); try ring.
+  apply Zplus_le_lt_compat; auto with zarith.
+  replace b with ((b - a) + a); try ring.
+  rewrite Zpower_exp; auto with zarith.
+  pattern (2 ^a) at 4; rewrite <- (Zmult_1_l (2 ^a)); 
+   try rewrite <- Zmult_minus_distr_r.
+  repeat rewrite (fun x => Zmult_comm x (2 ^ a)); rewrite Zmult_mod_distr_l;
+   auto with zarith.
+  apply Zmult_le_compat_l; auto with zarith.
+  match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end; 
+   auto with zarith.
+ Qed.
+
+  Theorem Zdiv_shift_r: 
+    forall a b r t, 0 <= a <= b -> 0 <= r -> 0 <= t < 2 ^a ->
+      (r * 2 ^a + t) /  (2 ^ b) = (r * 2 ^a) / (2 ^ b).
+  Proof.
+   intros a b r t (H1, H2) H3 (H4, H5).
+   assert (Eq: t < 2 ^ b); auto with zarith.
+   apply Zlt_le_trans with (1 := H5); auto with zarith.
+   apply Zpower_le_monotone; auto with zarith.
+   pattern (r * 2 ^ a) at 1; rewrite Z_div_mod_eq with (b := 2 ^ b);
+    auto with zarith.
+   rewrite <- Zplus_assoc.
+   rewrite <- Zmod_shift_r; auto with zarith.
+   rewrite (Zmult_comm (2 ^ b)); rewrite Z_div_plus_full_l; auto with zarith.
+   rewrite (fun x y => @Zdiv_small (x mod y)); auto with zarith.
+   match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end; 
+    auto with zarith.
+  Qed.
+
+
+ Lemma shift_unshift_mod : forall n p a,
+     0 <= a < 2^n ->
+     0 <= p <= n ->
+     a * 2^p = a / 2^(n - p) * 2^n + (a*2^p) mod 2^n.
+ Proof.
+  intros n p a H1 H2.
+  pattern (a*2^p) at 1;replace (a*2^p) with 
+     (a*2^p/2^n * 2^n + a*2^p mod 2^n). 
+  2:symmetry;rewrite (Zmult_comm (a*2^p/2^n));apply Z_div_mod_eq.
+  replace (a * 2 ^ p / 2 ^ n) with (a / 2 ^ (n - p));trivial.
+  replace (2^n) with (2^(n-p)*2^p).
+  symmetry;apply Zdiv_mult_cancel_r.
+  destruct H1;trivial.
+  cut (0 < 2^p); auto with zarith.
+  rewrite <- Zpower_exp.
+  replace (n-p+p) with n;trivial. ring.
+  omega. omega.
+  apply Zlt_gt. apply Zpower_gt_0;auto with zarith.
+ Qed.
+
+ Lemma div_le_0 : forall p x, 0 <= x -> 0 <= x / 2 ^ p.
+ Proof.
+  intros p x Hle;destruct (Z_le_gt_dec 0 p).
+  apply  Zdiv_le_lower_bound;auto with zarith. 
+  replace (2^p) with 0.
+  destruct x;compute;intro;discriminate.
+  destruct p;trivial;discriminate z.
+ Qed.
+ 
+ Lemma div_lt : forall p x y, 0 <= x < y -> x / 2^p < y.
+ Proof.
+  intros p x y H;destruct (Z_le_gt_dec 0 p).
+  apply Zdiv_lt_upper_bound;auto with zarith. 
+  apply Zlt_le_trans with y;auto with zarith.
+  rewrite <- (Zmult_1_r y);apply Zmult_le_compat;auto with zarith.
+  assert (0 < 2^p);auto with zarith.
+  replace (2^p) with 0.
+  destruct x;change (0<y);auto with zarith.
+  destruct p;trivial;discriminate z.
+ Qed.
+
+ Theorem Zgcd_div_pos a b:
+   (0 < b)%Z -> (0 < Zgcd a b)%Z -> (0 < b / Zgcd a b)%Z.
+ Proof.
+ intros a b Ha Hg.
+ case (Zle_lt_or_eq 0 (b/Zgcd a b)); auto.
+ apply Z_div_pos; auto with zarith.
+ intros H; generalize Ha.
+ pattern b at 1; rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto.
+ rewrite <- H; auto with zarith.
+ assert (F := (Zgcd_is_gcd a b)); inversion F; auto.
+ Qed.
+ 
+(* For compatibility of scripts, weaker version of some lemmas of Zdiv *)
+
+Lemma Zlt0_not_eq : forall n, 0<n -> n<>0.
+Proof.
+ auto with zarith.
+Qed.
+
+Definition Zdiv_mult_cancel_r a b c H := Zdiv.Zdiv_mult_cancel_r a b c (Zlt0_not_eq _ H).
+Definition Zdiv_mult_cancel_l a b c H := Zdiv.Zdiv_mult_cancel_r a b c (Zlt0_not_eq _ H).
+Definition Z_div_plus_l a b c H := Zdiv.Z_div_plus_full_l a b c (Zlt0_not_eq _ H).
+
+Theorem Zbounded_induction :
+  (forall Q : Z -> Prop, forall b : Z,
+    Q 0 ->
+    (forall n, 0 <= n -> n < b - 1 -> Q n -> Q (n + 1)) ->
+      forall n, 0 <= n -> n < b -> Q n)%Z.
+Proof.
+intros Q b Q0 QS.
+set (Q' := fun n => (n < b /\ Q n) \/ (b <= n)).
+assert (H : forall n, 0 <= n -> Q' n).
+apply natlike_rec2; unfold Q'.
+destruct (Zle_or_lt b 0) as [H | H]. now right. left; now split.
+intros n H IH. destruct IH as [[IH1 IH2] | IH].
+destruct (Zle_or_lt (b - 1) n) as [H1 | H1].
+right; auto with zarith.
+left. split; [auto with zarith | now apply (QS n)].
+right; auto with zarith.
+unfold Q' in *; intros n H1 H2. destruct (H n H1) as [[H3 H4] | H3].
+assumption. apply Zle_not_lt in H3. false_hyp H2 H3.
+Qed.
diff --git a/theories/Ints/num/BigQ.v b/theories/Ints/num/BigQ.v
index bd889e12f2..33e5f669cd 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 77f5e23016..fae16aad69 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 a9936f1dd0..e93e3a4893 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 237adb48b0..ea6868a901 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 7987741dad..3c70adb615 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 06c76067eb..f74cdc30bb 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 c7ac1ea3ea..9a56f1ee3c 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 d1ed6353df..63a0930edc 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 9b09248532..6ffb245757 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 7f3703a1b8..7d2c7af015 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 5cc8f0284a..c857da3857 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 0d85c92ed1..1398e8f559 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 c39a63301a..d5809ea591 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 f82c5d25b2..0cd2d2122f 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 9eb5de5e18..a98fda9d7f 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 c5fc425209..83c182ee08 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 906cf8d159..a28434baf2 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 c3db44bc6f..85655dafcd 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 d00f14ec6c..75fc19584d 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 a244635ea8..48cf268409 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 61d1ced604..d5b798a18c 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).
-- 
cgit v1.2.3