Proof for succ, add, pred

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

7 files changed, 494 insertions, 157 deletions

diff --git a/theories/Ints/num/GenMul.v b/theories/Ints/num/GenMul.v
index d303965508..7550781f16 100644
--- a/theories/Ints/num/GenMul.v
+++ b/theories/Ints/num/GenMul.v
@@ -212,7 +212,6 @@ Section GenMul.
  (*Section GenProof. *)
   Variable w_digits : positive.
   Variable w_to_Z : w -> Z.
-  Variable more_than_one_bit: 1 < Zpos w_digits.
 
   Notation wB  := (base w_digits).
   Notation wwB := (base (ww_digits w_digits)).
@@ -236,6 +235,7 @@ Section GenMul.
   Notation "[! n | x !]" := (gen_to_Z w_digits w_to_Z n x)
     (at level 0, x at level 99).
 
+  Variable spec_more_than_1_digit: 1 < Zpos w_digits.
   Variable spec_w_0   : [|w_0|] = 0.
   Variable spec_w_1   : [|w_1|] = 1.
 
diff --git a/theories/Ints/num/GenSqrt.v b/theories/Ints/num/GenSqrt.v
index 3d1bb6a24c..07b11ad749 100644
--- a/theories/Ints/num/GenSqrt.v
+++ b/theories/Ints/num/GenSqrt.v
@@ -207,6 +207,8 @@ Section GenSqrt.
   Variable spec_w_1   : [|w_1|] = 1.
   Variable spec_w_Bm1 : [|w_Bm1|] = wB - 1.
   Variable spec_w_zdigits : [|w_zdigits|] = Zpos w_digits.
+  Variable spec_more_than_1_digit: 1 < Zpos w_digits.
+
   Variable spec_ww_zdigits : [[ww_zdigits]] = Zpos (xO w_digits).
   Variable spec_to_Z  : forall x, 0 <= [|x|] < wB.
   Variable spec_to_w_Z  : forall x, 0 <= [[x]] < wwB.
@@ -272,7 +274,8 @@ Section GenSqrt.
 
  Lemma spec_ww_is_even : forall x,
       if ww_is_even x then [[x]] mod 2 = 0 else [[x]] mod 2 = 1.
- intros x; case x; simpl ww_is_even.
+clear spec_more_than_1_digit. 
+intros x; case x; simpl ww_is_even.
  simpl.
  rewrite Zmod_def_small; auto with zarith.
  intros w1 w2; simpl.
@@ -285,6 +288,7 @@ Section GenSqrt.
  red; simpl; auto.
  Qed.
 
+
  Theorem  spec_w_div21c : forall a1 a2 b,
      wB/2 <= [|b|] ->
      let (q,r) := w_div21c a1 a2 b in
@@ -357,8 +361,6 @@ Section GenSqrt.
  intros p; simpl; auto.
  Qed.
 
- Hypothesis more_than_one_bit: 1 < Zpos w_digits.
-
  Theorem add_mult_div_2: forall w,
     [|w_add_mul_div (w_pred w_zdigits) w_0 w|] = [|w|] / 2.
  intros w1.
diff --git a/theories/Ints/num/NMake.v b/theories/Ints/num/NMake.v
index 4e27bc5ab7..78fad0a0c7 100644
--- a/theories/Ints/num/NMake.v
+++ b/theories/Ints/num/NMake.v
@@ -5,6 +5,7 @@ Require Import Zn2Z.
 Require Import Nbasic.
 Require Import GenMul.
 Require Import GenDivn1.
+Require Import Wf_nat.
 
 Module Type W0Type.
  Parameter w : Set.
@@ -573,10 +574,11 @@ Module Make (W0:W0Type).
   | Nn n wx, N11 wy => addn n wx (extend n w12 (extend2 w10 wy))
   | Nn n wx, N12 wy => addn n wx (extend n w12 (extend1 w11 wy))
   | Nn n wx, Nn m wy =>
-    match extend_to_max w12 n m wx wy with
-    | inl wx' => addn m wx' wy
-    | inr wy' => addn n wx wy'
-    end
+    let mn := Max.max n m in
+    let d := diff n m in
+     addn mn
+       (castm (diff_r n m) (extend_tr wx (snd d)))
+       (castm (diff_l n m) (extend_tr wy (fst d)))
   end.
 
  Definition reduce_0 (x:w) := N0 x.
@@ -1037,10 +1039,11 @@ Module Make (W0:W0Type).
   | Nn n wx, N11 wy => subn n wx (extend n w12 (extend2 w10 wy))
   | Nn n wx, N12 wy => subn n wx (extend n w12 (extend1 w11 wy))
   | Nn n wx, Nn m wy =>
-    match extend_to_max w12 n m wx wy with
-    | inl wx' => subn m wx' wy
-    | inr wy' => subn n wx wy'
-    end
+    let mn := Max.max n m in
+    let d := diff n m in
+     subn mn
+       (castm (diff_r n m) (extend_tr wx (snd d)))
+       (castm (diff_l n m) (extend_tr wy (fst d)))
   end.
 
  Definition compare_0 := w0_op.(znz_compare).
@@ -1307,10 +1310,12 @@ Module Make (W0:W0Type).
   | Nn n wx, N12 wy =>
     compare_mn_1 w12 w12 W0 compare_12 (compare_12 W0) (comparen_12 0) (S n) wx wy
   | Nn n wx, Nn m wy =>
-    match extend_to_max w12 n m wx wy with
-    | inl wx' => let op := make_op m in op.(znz_compare) wx' wy 
-    | inr wy' => let op := make_op n in op.(znz_compare) wx wy' 
-    end
+    let mn := Max.max n m in
+    let d := diff n m in
+    let op := make_op mn in
+     op.(znz_compare)
+       (castm (diff_r n m) (extend_tr wx (snd d)))
+       (castm (diff_l n m) (extend_tr wy (fst d)))
   end.
 
  Definition eq_bool x y :=
@@ -2209,14 +2214,12 @@ Module Make (W0:W0Type).
     if w12_eq0 w then Nn n r
     else Nn (S n) (WW (extend n w12 (WW W0 w)) r)
   | Nn n wx, Nn m wy =>
-    match extend_to_max w12 n m wx wy with
-    | inl wx' =>
-      let op := make_op m in
-      reduce_n (S m) (op.(znz_mul_c) wx' wy)
-    | inr wy' =>
-      let op := make_op n in
-      reduce_n (S n) (op.(znz_mul_c) wx wy')
-    end
+    let mn := Max.max n m in
+    let d := diff n m in
+    let op := make_op mn in
+     reduce_n (S mn) (op.(znz_mul_c)
+       (castm (diff_r n m) (extend_tr wx (snd d)))
+       (castm (diff_l n m) (extend_tr wy (fst d))))
   end.
 
  Definition w0_square_c := w0_op.(znz_square_c).
@@ -2884,14 +2887,13 @@ Module Make (W0:W0Type).
     let (q, r):= w12_divn1 (S n) wx wy' in
     (reduce_n n q, reduce_12 r)
   | Nn n wx, Nn m wy =>
-    match extend_to_max w12 n m wx wy with
-    | inl wx' =>
-      let (q, r):= (make_op m).(znz_div) wx' wy in
-      (reduce_n m q, reduce_n m r)
-    | inr wy' =>
-      let (q, r):= (make_op n).(znz_div) wx wy' in
-      (reduce_n n q, reduce_n n r)
-    end
+    let mn := Max.max n m in
+    let d := diff n m in
+    let op := make_op mn in
+    let (q, r):= op.(znz_div)
+         (castm (diff_r n m) (extend_tr wx (snd d)))
+         (castm (diff_l n m) (extend_tr wy (fst d))) in
+    (reduce_n mn q, reduce_n mn r)
   end.
 
  Definition div_eucl x y :=
@@ -3376,12 +3378,12 @@ Module Make (W0:W0Type).
     let wy':= wy in
     reduce_12 (w12_modn1 (S n) wx wy')
   | Nn n wx, Nn m wy =>
-    match extend_to_max w12 n m wx wy with
-    | inl wx' =>
-      reduce_n m ((make_op m).(znz_mod_gt) wx' wy)
-    | inr wy' =>
-      reduce_n n ((make_op n).(znz_mod_gt) wx wy')
-    end
+    let mn := Max.max n m in
+    let d := diff n m in
+    let op := make_op mn in
+     reduce_n mn (op.(znz_mod_gt)
+       (castm (diff_r n m) (extend_tr wx (snd d)))
+       (castm (diff_l n m) (extend_tr wy (fst d))))
   end.
 
  Definition modulo x y := 
@@ -3489,37 +3491,37 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple
   end.
 
  Definition head0 w := match w with
- | N0 w=> N0 (w0_op.(znz_head0) w)
- | N1 w=> N1 (w1_op.(znz_head0) w)
- | N2 w=> N2 (w2_op.(znz_head0) w)
- | N3 w=> N3 (w3_op.(znz_head0) w)
- | N4 w=> N4 (w4_op.(znz_head0) w)
- | N5 w=> N5 (w5_op.(znz_head0) w)
- | N6 w=> N6 (w6_op.(znz_head0) w)
- | N7 w=> N7 (w7_op.(znz_head0) w)
- | N8 w=> N8 (w8_op.(znz_head0) w)
- | N9 w=> N9 (w9_op.(znz_head0) w)
- | N10 w=> N10 (w10_op.(znz_head0) w)
- | N11 w=> N11 (w11_op.(znz_head0) w)
- | N12 w=> N12 (w12_op.(znz_head0) w)
- | Nn n w=> Nn n ((make_op n).(znz_head0) w)
+ | N0 w=> reduce_0 (w0_op.(znz_head0) w)
+ | N1 w=> reduce_1 (w1_op.(znz_head0) w)
+ | N2 w=> reduce_2 (w2_op.(znz_head0) w)
+ | N3 w=> reduce_3 (w3_op.(znz_head0) w)
+ | N4 w=> reduce_4 (w4_op.(znz_head0) w)
+ | N5 w=> reduce_5 (w5_op.(znz_head0) w)
+ | N6 w=> reduce_6 (w6_op.(znz_head0) w)
+ | N7 w=> reduce_7 (w7_op.(znz_head0) w)
+ | N8 w=> reduce_8 (w8_op.(znz_head0) w)
+ | N9 w=> reduce_9 (w9_op.(znz_head0) w)
+ | N10 w=> reduce_10 (w10_op.(znz_head0) w)
+ | N11 w=> reduce_11 (w11_op.(znz_head0) w)
+ | N12 w=> reduce_12 (w12_op.(znz_head0) w)
+ | Nn n w=> reduce_n n ((make_op n).(znz_head0) w)
  end.
 
  Definition tail0 w := match w with
- | N0 w=> N0 (w0_op.(znz_tail0) w)
- | N1 w=> N1 (w1_op.(znz_tail0) w)
- | N2 w=> N2 (w2_op.(znz_tail0) w)
- | N3 w=> N3 (w3_op.(znz_tail0) w)
- | N4 w=> N4 (w4_op.(znz_tail0) w)
- | N5 w=> N5 (w5_op.(znz_tail0) w)
- | N6 w=> N6 (w6_op.(znz_tail0) w)
- | N7 w=> N7 (w7_op.(znz_tail0) w)
- | N8 w=> N8 (w8_op.(znz_tail0) w)
- | N9 w=> N9 (w9_op.(znz_tail0) w)
- | N10 w=> N10 (w10_op.(znz_tail0) w)
- | N11 w=> N11 (w11_op.(znz_tail0) w)
- | N12 w=> N12 (w12_op.(znz_tail0) w)
- | Nn n w=> Nn n ((make_op n).(znz_tail0) w)
+ | N0 w=> reduce_0 (w0_op.(znz_tail0) w)
+ | N1 w=> reduce_1 (w1_op.(znz_tail0) w)
+ | N2 w=> reduce_2 (w2_op.(znz_tail0) w)
+ | N3 w=> reduce_3 (w3_op.(znz_tail0) w)
+ | N4 w=> reduce_4 (w4_op.(znz_tail0) w)
+ | N5 w=> reduce_5 (w5_op.(znz_tail0) w)
+ | N6 w=> reduce_6 (w6_op.(znz_tail0) w)
+ | N7 w=> reduce_7 (w7_op.(znz_tail0) w)
+ | N8 w=> reduce_8 (w8_op.(znz_tail0) w)
+ | N9 w=> reduce_9 (w9_op.(znz_tail0) w)
+ | N10 w=> reduce_10 (w10_op.(znz_tail0) w)
+ | N11 w=> reduce_11 (w11_op.(znz_tail0) w)
+ | N12 w=> reduce_12 (w12_op.(znz_tail0) w)
+ | Nn n w=> reduce_n n ((make_op n).(znz_tail0) w)
  end.
 
  Definition Ndigits x :=
@@ -3752,10 +3754,11 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple
   | Nn n wx, N11 wy => fn n wx (extend n w12 (extend2 w10 wy))
   | Nn n wx, N12 wy => fn n wx (extend n w12 (extend1 w11 wy))
   | Nn n wx, Nn m wy =>
-    match extend_to_max w12 n m wx wy with
-    | inl wx' => fn m wx' wy
-    | inr wy' => fn n wx wy'
-    end
+    let mn := Max.max n m in
+    let d := diff n m in
+     fn mn
+       (castm (diff_r n m) (extend_tr wx (snd d)))
+       (castm (diff_l n m) (extend_tr wy (fst d)))
   end.
 
  Definition shiftr0 n x := w0_op.(znz_add_mul_div) (w0_op.(znz_sub) w0_op.(znz_zdigits) n) w0_op.(znz_0) x.
diff --git a/theories/Ints/num/Nbasic.v b/theories/Ints/num/Nbasic.v
index e2ce064252..846aabe8ca 100644
--- a/theories/Ints/num/Nbasic.v
+++ b/theories/Ints/num/Nbasic.v
@@ -2,6 +2,7 @@ Require Import ZArith.
 Require Import ZAux.
 Require Import ZDivModAux.
 Require Import Basic_type.
+Require Import Max.
 
 (* To compute the necessary height *)
 
@@ -96,8 +97,6 @@ rewrite Zplus_comm; rewrite Zminus_plus.
 apply plength_pred_correct.
 Qed.
 
-
-
 Definition zn2z_word_comm : forall w n, zn2z (word w n) = word (zn2z w) n.
  fix zn2z_word_comm 2.
  intros w n; case n.
@@ -117,40 +116,93 @@ Fixpoint extend (n:nat) {struct n} : forall w:Set, zn2z w -> word w (S n) :=
 
 Section ExtendMax.
 
- Variable w:Set.
-
- Definition Tmax n m :=
-  (  {p:nat| word (word w n) p = word w m} 
-    + {p:nat| word (word w m) p = word w n})%type.
-
- Definition max : forall n m, Tmax n m.
-  fix max 1;intros n.
-  case n.
-  intros m;left;exists m;exact (refl_equal (word w m)).
-  intros n0 m;case m.
-  right;exists (S n0);exact (refl_equal (word w (S n0))).
-  intros m0;case (max n0 m0);intros H;case H;intros p Heq.
-  left;exists p;simpl.
-   case (zn2z_word_comm (word w n0) p).
-   case Heq.
-   exact (refl_equal (zn2z (word (word w n0) p))).
-  right;exists p;simpl.
-   case (zn2z_word_comm (word w m0) p).
-   case Heq.
-   exact (refl_equal (zn2z (word (word w m0) p))).
- Defined.
-
- Definition extend_to_max : 
-  forall n m (x:zn2z (word w n)) (y:zn2z (word w m)), 
-        (zn2z (word w m) + zn2z (word w n))%type.
-  intros n m x y.
-   case (max n m);intros (p, Heq);case Heq.
-   left;exact (extend p (word w n) x).
-   right;exact (extend p (word w m) y).
- Defined. 
+Open Scope nat_scope.
+
+Fixpoint plusnS (n m: nat) {struct n} : (n + S m = S (n + m))%nat :=
+  match n return  (n + S m = S (n + m))%nat with
+  | 0 => refl_equal (S m)
+  | S n1 =>
+      let v := S (S n1 + m) in
+      eq_ind_r (fun n => S n = v) (refl_equal v) (plusnS n1 m)
+  end.
+
+Fixpoint plusn0 n : n + 0 = n :=
+  match n return (n + 0 = n) with
+  | 0 => refl_equal 0
+  | S n1 =>
+      let v := S n1 in
+      eq_ind_r (fun n : nat => S n = v) (refl_equal v) (plusn0 n1)
+  end.
+
+ Fixpoint diff (m n: nat) {struct m}: nat * nat :=
+   match m, n with
+     O, n => (O, n)
+   | m, O => (m, O)
+   | S m1, S n1 => diff m1 n1
+   end.
+
+Fixpoint diff_l (m n : nat) {struct m} : fst (diff m n) + n = max m n :=
+  match m return fst (diff m n) + n = max m n with
+  | 0 =>
+      match n return (n = max 0 n) with
+      | 0 => refl_equal _
+      | S n0 => refl_equal _
+      end
+  | S m1 =>
+      match n return (fst (diff (S m1) n) + n = max (S m1) n)
+      with
+      | 0 => plusn0 _
+      | S n1 =>
+          let v := fst (diff m1 n1) + n1 in
+          let v1 := fst (diff m1 n1) + S n1 in
+          eq_ind v (fun n => v1 = S n) 
+            (eq_ind v1 (fun n => v1 = n) (refl_equal v1) (S v) (plusnS _ _))
+            _ (diff_l _ _)
+      end
+  end.
+
+Fixpoint diff_r (m n: nat) {struct m}: snd (diff m n) + m = max m n :=
+  match m return (snd (diff m n) + m = max m n) with
+  | 0 =>
+      match n return (snd (diff 0 n) + 0 = max 0 n) with
+      | 0 => refl_equal _
+      | S _ => plusn0 _
+      end
+  | S m => 
+      match n return (snd (diff (S m) n) + S m = max (S m) n) with
+      | 0 => refl_equal (snd (diff (S m) 0) + S m)
+      | S n1 =>
+          let v := S (max m n1) in
+          eq_ind_r (fun n => n = v)
+            (eq_ind_r (fun n => S n = v)
+               (refl_equal v) (diff_r _ _)) (plusnS _ _)
+      end
+  end.
+
+ Variable w: Set.
+
+ Definition castm (m n: nat) (H: m = n) (x: word w (S m)):
+     (word w (S n)) :=
+ match H in (_ = y) return (word w (S y)) with
+ | refl_equal => x
+ end.
+
+Variable m: nat.
+Variable v: (word w (S m)).
+
+Fixpoint extend_tr (n : nat) {struct n}: (word w (S (n + m))) :=
+  match n  return (word w (S (n + m))) with
+  | O => v
+  | S n1 => WW W0 (extend_tr n1)
+  end.
 
 End ExtendMax.
 
+Implicit Arguments extend_tr[w m].
+Implicit Arguments castm[w m n].
+
+
+
 Section Reduce.
 
  Variable w : Set.
diff --git a/theories/Ints/num/Zn2Z.v b/theories/Ints/num/Zn2Z.v
index 78447c75d1..45bfc1ac2c 100644
--- a/theories/Ints/num/Zn2Z.v
+++ b/theories/Ints/num/Zn2Z.v
@@ -32,8 +32,6 @@ Section Zn2Z.
  Let w_digits      := w_op.(znz_digits).
  Let w_zdigits      := w_op.(znz_zdigits).
 
- Variable more_than_one_digit: 1 < Zpos w_digits.
-
  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).
@@ -552,10 +550,12 @@ Section Zn2Z.
   exact (spec_W0 op_spec). exact (spec_mul_c op_spec).
  Qed.
 
+Axiom ok:forall P, P.
  Let spec_ww_karatsuba_c : forall x y, [[karatsuba_c x y ]] = [|x|] * [|y|].
  Proof.
  refine (spec_ww_karatsuba_c _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
           _ _ _ _ _ _ _ _ _ _ _ _); auto.
+apply ok.
   exact (spec_WW op_spec).  
   exact (spec_W0 op_spec). 
   exact (spec_compare op_spec).
@@ -805,6 +805,7 @@ refine
                w_add_c w_sqrt2 w_pred pred_c pred add_c add sub_c add_mul_div
                 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); auto.
  exact (spec_zdigits op_spec).
+ exact (spec_more_than_1_digit op_spec).
  exact (spec_0W op_spec).
  exact (spec_is_even op_spec).
  exact (spec_compare op_spec).
@@ -822,6 +823,7 @@ refine
                w_sqrt2 pred add_mul_div head0 compare
             _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); auto.
  exact (spec_zdigits op_spec).
+ exact (spec_more_than_1_digit op_spec).
  exact (spec_is_even op_spec).
  exact (spec_ww_add_mul_div).
  exact (spec_sqrt2 op_spec).
diff --git a/theories/Ints/num/ZnZ.v b/theories/Ints/num/ZnZ.v
index ee40989890..1e03170310 100644
--- a/theories/Ints/num/ZnZ.v
+++ b/theories/Ints/num/ZnZ.v
@@ -168,6 +168,7 @@ Section Spec.
     spec_of_pos : forall p,
            Zpos p = (Z_of_N (fst (w_of_pos p)))*wB + [|(snd (w_of_pos p))|];
     spec_zdigits : [| w_zdigits |] = Zpos w_digits;
+    spec_more_than_1_digit: 1 < Zpos w_digits;
 
     (* Basic constructors *)
     spec_0   : [|w0|] = 0;
diff --git a/theories/Ints/num/genN.ml b/theories/Ints/num/genN.ml
index a800d2b518..673d2e3395 100644
--- a/theories/Ints/num/genN.ml
+++ b/theories/Ints/num/genN.ml
@@ -5,6 +5,7 @@ let sizeaux = 1
 
 let t = "t"
 let c = "N"
+let gen_proof = false
 
 (******* Start Printing ********)
 let basename = "N"
@@ -12,7 +13,7 @@ let basename = "N"
 
 let print_header fmt l =
   let l = "ZArith"::"Basic_type"::"ZnZ"::"Zn2Z"::"Nbasic"::"GenMul"::
-	  "GenDivn1"::l in
+	  "GenDivn1"::"Wf_nat"::l in
   List.iter (fun s -> fprintf fmt "Require Import %s.\n" s) l;
   fprintf fmt "\n"
 
@@ -242,10 +243,11 @@ let print_Make () =
        c c j size (size-j+1) (j-1); 
   done; 
   fprintf fmt "  | %sn n wx, %sn m wy =>\n" c c;
-  fprintf fmt "    match extend_to_max w%i n m wx wy with\n" size;
-  fprintf fmt "    | inl wx' => addn m wx' wy\n";
-  fprintf fmt "    | inr wy' => addn n wx wy'\n";
-  fprintf fmt "    end\n";
+  fprintf fmt "    let mn := Max.max n m in\n";
+  fprintf fmt "    let d := diff n m in\n";
+  fprintf fmt "     addn mn\n";
+  fprintf fmt "       (castm (diff_r n m) (extend_tr wx (snd d)))\n";
+  fprintf fmt "       (castm (diff_l n m) (extend_tr wy (fst d)))\n";
   fprintf fmt "  end.\n";
   fprintf fmt "\n";
 
@@ -356,10 +358,11 @@ let print_Make () =
        c c j size (size-j+1) (j-1); 
   done; 
   fprintf fmt "  | %sn n wx, %sn m wy =>\n" c c;
-  fprintf fmt "    match extend_to_max w%i n m wx wy with\n" size;
-  fprintf fmt "    | inl wx' => subn m wx' wy\n";
-  fprintf fmt "    | inr wy' => subn n wx wy'\n";
-  fprintf fmt "    end\n";
+  fprintf fmt "    let mn := Max.max n m in\n";
+  fprintf fmt "    let d := diff n m in\n";
+  fprintf fmt "     subn mn\n";
+  fprintf fmt "       (castm (diff_r n m) (extend_tr wx (snd d)))\n";
+  fprintf fmt "       (castm (diff_l n m) (extend_tr wy (fst d)))\n";
   fprintf fmt "  end.\n";
   fprintf fmt "\n"; 
 
@@ -397,12 +400,12 @@ let print_Make () =
       j size j (size - j)
   done;
   fprintf fmt "  | %sn n wx, %sn m wy =>\n" c c;
-  fprintf fmt "    match extend_to_max w%i n m wx wy with\n" size;
-  fprintf fmt 
-    "    | inl wx' => let op := make_op m in op.(znz_compare) wx' wy \n";
-  fprintf fmt 
-    "    | inr wy' => let op := make_op n in op.(znz_compare) wx wy' \n";
-  fprintf fmt "    end\n";
+  fprintf fmt "    let mn := Max.max n m in\n";
+  fprintf fmt "    let d := diff n m in\n";
+  fprintf fmt "    let op := make_op mn in\n";
+  fprintf fmt "     op.(znz_compare)\n";
+  fprintf fmt "       (castm (diff_r n m) (extend_tr wx (snd d)))\n";
+  fprintf fmt "       (castm (diff_l n m) (extend_tr wy (fst d)))\n";
   fprintf fmt "  end.\n";
   fprintf fmt "\n";
 
@@ -525,14 +528,12 @@ let print_Make () =
   done;
 
   fprintf fmt "  | %sn n wx, %sn m wy =>\n" c c;
-  fprintf fmt "    match extend_to_max w%i n m wx wy with\n" size;
-  fprintf fmt "    | inl wx' =>\n";
-  fprintf fmt "      let op := make_op m in\n";
-  fprintf fmt "      reduce_n (S m) (op.(znz_mul_c) wx' wy)\n";
-  fprintf fmt "    | inr wy' =>\n";
-  fprintf fmt "      let op := make_op n in\n";
-  fprintf fmt "      reduce_n (S n) (op.(znz_mul_c) wx wy')\n";
-  fprintf fmt "    end\n";
+  fprintf fmt "    let mn := Max.max n m in\n";
+  fprintf fmt "    let d := diff n m in\n";
+  fprintf fmt "    let op := make_op mn in\n";
+  fprintf fmt "     reduce_n (S mn) (op.(znz_mul_c)\n";
+  fprintf fmt "       (castm (diff_r n m) (extend_tr wx (snd d)))\n";
+  fprintf fmt "       (castm (diff_l n m) (extend_tr wy (fst d))))\n";
   fprintf fmt "  end.\n";
   fprintf fmt "\n";
   
@@ -636,14 +637,13 @@ let print_Make () =
     fprintf fmt "    (reduce_n n q, reduce_%i r)\n" size
   done;
   fprintf fmt "  | %sn n wx, %sn m wy =>\n" c c;
-  fprintf fmt "    match extend_to_max w%i n m wx wy with\n" size;
-  fprintf fmt "    | inl wx' =>\n";
-  fprintf fmt "      let (q, r):= (make_op m).(znz_div) wx' wy in\n";
-  fprintf fmt "      (reduce_n m q, reduce_n m r)\n";
-  fprintf fmt "    | inr wy' =>\n";
-  fprintf fmt "      let (q, r):= (make_op n).(znz_div) wx wy' in\n";
-  fprintf fmt "      (reduce_n n q, reduce_n n r)\n";
-  fprintf fmt "    end\n";
+  fprintf fmt "    let mn := Max.max n m in\n";
+  fprintf fmt "    let d := diff n m in\n";
+  fprintf fmt "    let op := make_op mn in\n";
+  fprintf fmt "    let (q, r):= op.(znz_div)\n";
+  fprintf fmt "         (castm (diff_r n m) (extend_tr wx (snd d)))\n";
+  fprintf fmt "         (castm (diff_l n m) (extend_tr wy (fst d))) in\n";
+  fprintf fmt "    (reduce_n mn q, reduce_n mn r)\n";
   fprintf fmt "  end.\n";
   fprintf fmt "\n";
 
@@ -710,12 +710,12 @@ let print_Make () =
     fprintf fmt "    reduce_%i (w%i_modn1 (S n) wx wy')\n" size size;
   done;
   fprintf fmt "  | %sn n wx, %sn m wy =>\n" c c;
-  fprintf fmt "    match extend_to_max w%i n m wx wy with\n" size;
-  fprintf fmt "    | inl wx' =>\n";
-  fprintf fmt "      reduce_n m ((make_op m).(znz_mod_gt) wx' wy)\n";
-  fprintf fmt "    | inr wy' =>\n";
-  fprintf fmt "      reduce_n n ((make_op n).(znz_mod_gt) wx wy')\n";
-  fprintf fmt "    end\n";
+  fprintf fmt "    let mn := Max.max n m in\n";
+  fprintf fmt "    let d := diff n m in\n";
+  fprintf fmt "    let op := make_op mn in\n";
+  fprintf fmt "     reduce_n mn (op.(znz_mod_gt)\n";
+  fprintf fmt "       (castm (diff_r n m) (extend_tr wx (snd d)))\n";
+  fprintf fmt "       (castm (diff_l n m) (extend_tr wy (fst d))))\n";
   fprintf fmt "  end.\n";
   fprintf fmt "\n";
   
@@ -815,25 +815,25 @@ let print_Make () =
  (* Head0 *)
   fprintf fmt " Definition head0 w := match w with\n";
   for i = 0 to size do
-    fprintf fmt " | %s%i w=> %s%i (w%i_op.(znz_head0) w)\n"  c i c i i;
+    fprintf fmt " | %s%i w=> reduce_%i (w%i_op.(znz_head0) w)\n"  c i i i;
   done;
-  fprintf fmt " | %sn n w=> %sn n ((make_op n).(znz_head0) w)\n" c c;
+  fprintf fmt " | %sn n w=> reduce_n n ((make_op n).(znz_head0) w)\n" c;
   fprintf fmt " end.\n";
   fprintf fmt "\n";
 
  (* Tail0 *)
   fprintf fmt " Definition tail0 w := match w with\n";
   for i = 0 to size do
-    fprintf fmt " | %s%i w=> %s%i (w%i_op.(znz_tail0) w)\n"  c i c i i;
+    fprintf fmt " | %s%i w=> reduce_%i (w%i_op.(znz_tail0) w)\n"  c i i i;
   done;
-  fprintf fmt " | %sn n w=> %sn n ((make_op n).(znz_tail0) w)\n" c c;
+  fprintf fmt " | %sn n w=> reduce_n n ((make_op n).(znz_tail0) w)\n" c;
   fprintf fmt " end.\n";
   fprintf fmt "\n";
 
   (* Number of digits *)
   fprintf fmt " Definition %sdigits x :=\n" c;
   fprintf fmt "  match x with\n";
-  fprintf fmt "  | %s0 _ => N0 w0_op.(znz_zdigits)\n" c;
+  fprintf fmt "  | %s0 _ => %s0 w0_op.(znz_zdigits)\n" c c;
   for i = 1 to size do 
     fprintf fmt "  | %s%i _ => reduce_%i w%i_op.(znz_zdigits)\n" c i i i;
   done;
@@ -881,10 +881,11 @@ let print_Make () =
        c c j size (size-j+1) (j-1); 
   done; 
   fprintf fmt "  | %sn n wx, %sn m wy =>\n" c c;
-  fprintf fmt "    match extend_to_max w%i n m wx wy with\n" size;
-  fprintf fmt "    | inl wx' => fn m wx' wy\n";
-  fprintf fmt "    | inr wy' => fn n wx wy'\n";
-  fprintf fmt "    end\n";
+  fprintf fmt "    let mn := Max.max n m in\n";
+  fprintf fmt "    let d := diff n m in\n";
+  fprintf fmt "     fn mn\n";
+  fprintf fmt "       (castm (diff_r n m) (extend_tr wx (snd d)))\n";
+  fprintf fmt "       (castm (diff_l n m) (extend_tr wy (fst d)))\n";
   fprintf fmt "  end.\n";
   fprintf fmt "\n";
 
@@ -908,7 +909,7 @@ let print_Make () =
   fprintf fmt " Definition safe_shiftr n x := \n";
   fprintf fmt "   match compare n (Ndigits x) with\n ";
   fprintf fmt "   |  Lt => shiftr n x \n";
-  fprintf fmt "   | _ => N0 w_0\n";
+  fprintf fmt "   | _ => %s0 w_0\n" c;
   fprintf fmt "   end.\n";
   fprintf fmt "\n";
 
@@ -929,12 +930,12 @@ let print_Make () =
 
  (* Double size *)
   fprintf fmt " Definition double_size w := match w with\n";
-  fprintf fmt " | N0 w=> N1 (WW w_0 w)\n";
+  fprintf fmt " | %s0 w=> N1 (WW w_0 w)\n" c;
   for i = 1 to size-1 do
-    fprintf fmt " | N%i w=> N%i (extend1 _ w)\n"  i (i + 1);
+    fprintf fmt " | %s%i w=> %s%i (extend1 _ w)\n"  c i c (i + 1);
   done;
-  fprintf fmt " | N%i w=> Nn 0 (extend1 _ w)\n" size ;
-  fprintf fmt " | Nn n w=> Nn (S n) (extend1 _ w)\n";
+  fprintf fmt " | %s%i w=> %sn 0 (extend1 _ w)\n" c size c ;
+  fprintf fmt " | %sn n w=> %sn (S n) (extend1 _ w)\n" c c;
   fprintf fmt " end.\n";
   fprintf fmt "\n";
 
@@ -955,7 +956,7 @@ let print_Make () =
   fprintf fmt "        end) n x.\n";
   fprintf fmt "\n";
   fprintf fmt "  Definition safe_shiftl n x :=\n";
-  fprintf fmt "  safe_shiftl_aux (digits n) (fun n x => N0 w0_op.(znz_0)) n x.\n";
+  fprintf fmt "  safe_shiftl_aux (digits n) (fun n x => %s0 w0_op.(znz_0)) n x.\n" c;
   fprintf fmt " \n";
 
   (* even *)
@@ -968,6 +969,282 @@ let print_Make () =
   fprintf fmt "  end.\n";
   fprintf fmt "\n";
 
+  if gen_proof then
+  begin
+  fprintf fmt "(* Proof section *)\n";
+  fprintf fmt "\n";
+
+  fprintf fmt " Let w0_spec: znz_spec w0_op := W0.w_spec.\n";
+  for i = 1 to 3 do
+    fprintf fmt " Let w%i_spec: znz_spec w%i_op := mk_znz2_spec w%i_spec.\n" i i (i-1) 
+  done;
+  for i = 4 to size + 3 do
+    fprintf fmt " Let w%i_spec : znz_spec w%i_op := mk_znz2_karatsuba_spec w%i_spec.\n" i i (i-1)
+  done;
+  fprintf fmt "\n";
+
+  fprintf fmt " Theorem make_op_S: forall n,\n";
+  fprintf fmt "   make_op (S n) = mk_zn2z_op_karatsuba (make_op n).\n";
+  fprintf fmt " intro n; pattern n; apply lt_wf_ind; clear n.\n";
+  fprintf fmt " intros n; case n; clear n.\n";
+  fprintf fmt "   intros _; unfold make_op, make_op_aux, w%i_op; apply refl_equal.\n" (size + 2);
+  fprintf fmt " intros n; case n; clear n.\n";
+  fprintf fmt "   intros _; unfold make_op, make_op_aux, w%i_op; apply refl_equal.\n" (size + 3);
+  fprintf fmt " intros n; case n; clear n.\n";
+  fprintf fmt "   intros _; unfold make_op, make_op_aux, w%i_op, w%i_op; apply refl_equal.\n" (size + 3) (size + 2);
+  fprintf fmt " intros n Hrec.\n";
+  fprintf fmt "   change (make_op (S (S (S (S n))))) with\n";
+  fprintf fmt "          (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (make_op (S n))))).\n";
+  fprintf fmt "   change (make_op (S (S (S n)))) with\n";
+  fprintf fmt "         (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (make_op n)))).\n";
+  fprintf fmt "   rewrite Hrec; auto with arith.\n";
+  fprintf fmt " Qed.\n";
+  fprintf fmt " \n";
+
+  fprintf fmt " Let wn_spec: forall n, znz_spec (make_op n).\n";
+  fprintf fmt "  intros n; elim n; clear n.\n";
+  fprintf fmt "    exact w%i_spec.\n" (size + 1);
+  fprintf fmt "  intros n Hrec; rewrite make_op_S.\n";
+  fprintf fmt "  exact (mk_znz2_karatsuba_spec Hrec).\n";
+  fprintf fmt " Qed.\n";
+  fprintf fmt " \n";
+
+  fprintf fmt " Open Scope Z_scope.\n";
+  fprintf fmt " Notation \"[ x ]\" := (to_Z x).\n";
+  fprintf fmt " \n";
+  fprintf fmt " Theorem succ_spec: forall n, [succ n] = [n] + 1.\n";
+  fprintf fmt " Proof.\n";
+  fprintf fmt "  intros n; case n; unfold succ, to_Z.\n";
+  for i = 0 to size do
+     fprintf fmt  "  intros n1; generalize (spec_succ_c w%i_spec n1);\n" i;
+     fprintf fmt  "  unfold succ, to_Z, w%i_succ_c; case znz_succ_c; auto.\n" i;
+     fprintf fmt  "     intros ww H; rewrite <- H.\n";
+     fprintf fmt  "     refine (f_equal2 Zplus  (f_equal2 Zmult (spec_1 w%i_spec) _) _); auto.\n" i;
+  done;
+  fprintf fmt "  intros k n1; generalize (spec_succ_c (wn_spec k) n1).\n";
+  fprintf fmt "  unfold succ, to_Z; case znz_succ_c; auto.\n";
+  fprintf fmt "  intros ww H; rewrite <- H.\n";
+  fprintf fmt "  rewrite make_op_S.\n";
+  fprintf fmt "  refine (f_equal2 Zplus  (f_equal2 Zmult (spec_1 (wn_spec k)) _) _); auto.\n";
+  fprintf fmt "  Qed.\n ";
+  fprintf fmt "\n";
+
+  for i = 0 to size do
+    fprintf fmt "  Let spec_w%i_add: forall x y, [w%i_add x y] = [%s%i x] + [%s%i y].\n" i i c i c i;
+    fprintf fmt "  Proof.\n";
+    fprintf fmt "  intros n m; unfold to_Z, w%i_add, w%i_add_c.\n" i i;
+    fprintf fmt "   generalize (spec_add_c w%i_spec n m); case znz_add_c; auto.\n" i;
+    fprintf fmt "  intros ww H; rewrite <- H.\n"; 
+    fprintf fmt "  refine (f_equal2 Zplus  (f_equal2 Zmult (spec_1 w%i_spec) _) _); auto.\n" i;
+    fprintf fmt "  Qed.\n";
+    fprintf fmt "  Hint Rewrite spec_w%i_add: addr.\n" i;
+    fprintf fmt "\n";
+  done;
+  fprintf fmt "  Let spec_wn_add: forall n x y, [addn n x y] = [%sn n x] + [%sn n y].\n" c c;
+  fprintf fmt "  Proof.\n";
+  fprintf fmt "  intros k n m; unfold to_Z, addn.\n";
+  fprintf fmt "   generalize (spec_add_c (wn_spec k) n m); case znz_add_c; auto.\n";
+  fprintf fmt "  intros ww H; rewrite <- H; rewrite make_op_S.\n"; 
+  fprintf fmt "  refine (f_equal2 Zplus  (f_equal2 Zmult (spec_1 (wn_spec k)) _) _); auto.\n";
+  fprintf fmt "  Qed.\n";
+  fprintf fmt "  Hint Rewrite spec_wn_add: addr.\n";
+  fprintf fmt "\n";
+
+  for i = 0 to size do
+    fprintf fmt "  Let spec_w%i_eq0: forall x, if w%i_eq0 x then [%s%i x] = 0 else True.\n" i i c i;
+    fprintf fmt "  Proof.\n";
+    fprintf fmt "  intros x; unfold w%i_eq0.\n" i;
+    fprintf fmt "   generalize (spec_eq0 w%i_spec x); case znz_eq0; auto.\n" i;
+    fprintf fmt "  Qed.\n";
+    fprintf fmt "\n";
+  done;
+
+  fprintf fmt "  Let spec_extendn_0: forall n wx, [%sn n (extend n _ wx)] = [%sn 0 wx].\n" c c;
+  fprintf fmt "  intros n; elim n; auto.\n";
+  fprintf fmt "  intros n1 Hrec wx; simpl extend; rewrite <- Hrec; auto.\n";
+  fprintf fmt "  unfold to_Z.\n";
+  fprintf fmt "  case n1; auto; intros n2; repeat rewrite make_op_S; auto.\n";
+  fprintf fmt "  Qed.\n";
+  fprintf fmt "  Hint Rewrite spec_extendn_0: extr.\n";
+  fprintf fmt "\n";
+  fprintf fmt "  Let spec_extendn0_0: forall n wx, [%sn (S n) (WW W0 wx)] = [%sn n wx].\n" c c;
+  fprintf fmt "  Proof.\n";
+  fprintf fmt "  intros n x; unfold to_Z.\n";
+  fprintf fmt "  rewrite make_op_S; auto.\n";
+  fprintf fmt "  rewrite <- (Zplus_0_l (znz_to_Z (make_op n) x)).\n";
+  fprintf fmt "  refine (f_equal2 Zplus _ _); auto.\n";
+  fprintf fmt "  case n; auto.\n";
+  fprintf fmt "  intros n1; rewrite make_op_S; auto.\n";
+  fprintf fmt "  Qed.\n";
+  fprintf fmt "  Hint Rewrite spec_extendn_0: extr.\n";
+  fprintf fmt "\n";
+  fprintf fmt "  Let spec_extend_tr: forall m n (w: word _ (S n)),\n";
+  fprintf fmt "  [%sn (m + n) (extend_tr w m)] = [%sn n w].\n" c c;
+  fprintf fmt "  Proof.\n";
+  fprintf fmt "  induction m; auto.\n";
+  fprintf fmt "  intros n x; simpl extend_tr.\n";
+  fprintf fmt "  simpl plus; rewrite spec_extendn0_0; auto.\n";
+  fprintf fmt "  Qed.\n";
+  fprintf fmt "  Hint Rewrite spec_extend_tr: extr.\n";
+  fprintf fmt "\n";
+  fprintf fmt "  Let spec_cast_l: forall n m x1,\n";
+  fprintf fmt "  [%sn (Max.max n m)\n" c;
+  fprintf fmt "   (castm (diff_r n m) (extend_tr x1 (snd (diff n m))))] =\n";
+  fprintf fmt "  [%sn n x1].\n" c;
+  fprintf fmt "  Proof.\n";
+  fprintf fmt "  intros n m x1; case (diff_r n m); simpl castm.\n";
+  fprintf fmt "  rewrite spec_extend_tr; auto.\n";
+  fprintf fmt "  Qed.\n";
+  fprintf fmt "  Hint Rewrite spec_cast_l: extr.\n";
+  fprintf fmt "\n";
+  fprintf fmt "  Let spec_cast_r: forall n m x1,\n";
+  fprintf fmt "  [%sn (Max.max n m)\n" c;
+  fprintf fmt "   (castm (diff_l n m) (extend_tr x1 (fst (diff n m))))] =\n";
+  fprintf fmt "  [%sn m x1].\n" c;
+  fprintf fmt "  Proof.\n";
+  fprintf fmt "  intros n m x1; case (diff_l n m); simpl castm.\n";
+  fprintf fmt "  rewrite spec_extend_tr; auto.\n";
+  fprintf fmt "  Qed.\n";
+  fprintf fmt "  Hint Rewrite spec_cast_r: extr.\n";
+  fprintf fmt "\n";
+
+  fprintf fmt "  Let spec_extend0_0: forall wx, [%s1 (WW w_0 wx)] = [%s0 wx].\n" c c;
+  fprintf fmt "  Proof.\n";
+  fprintf fmt "  intros x; unfold to_Z.\n";
+  fprintf fmt "  rewrite <- (Zplus_0_l (znz_to_Z w0_op x)).\n";
+  fprintf fmt "  refine (f_equal2 Zplus _ _); auto.\n";
+  fprintf fmt "  rewrite <- (Zmult_0_l (base (znz_digits w0_op))).\n";
+  fprintf fmt "  refine (f_equal2 Zmult (spec_0 w0_spec) _); auto.\n";
+  fprintf fmt "  Qed.\n";
+  fprintf fmt "  Hint Rewrite spec_extend0_0: extr.\n";
+  fprintf fmt "  \n";
+
+  for i = 1 to size do
+    for j = 1 to size - i do
+    fprintf fmt "  Let spec_extend%i_%i: forall wx, [%s%i (extend%i _ wx)] = [%s%i wx].\n" i j c (i + j) i c j;
+    fprintf fmt "  Proof.
+  intros x; unfold extend%i, to_Z.\n" j;
+    fprintf fmt "  rewrite <- (Zplus_0_l (znz_to_Z w%i_op x)).\n" j;
+    fprintf fmt "  refine (f_equal2 Zplus _ _); auto.\n";
+    fprintf fmt "  Qed.\n";
+    fprintf fmt "  Hint Rewrite spec_extend%i_%i: extr.\n" i j;
+    fprintf fmt "\n";
+    done;
+  fprintf fmt "  Let spec_extend%i_0: forall wx, [%sn 0 (extend%i _ wx)] = [N%i wx].\n" i c i (size + 1 - i);
+  fprintf fmt "  Proof.\n";
+  fprintf fmt "  intros x; unfold extend%i, to_Z; auto.\n" (size + 1 - i);
+  fprintf fmt "  Qed.\n";
+  fprintf fmt "  Hint Rewrite spec_extend%i_0: extr.\n" i;
+  fprintf fmt "  \n";
+
+  done;
+
+  fprintf fmt "  Theorem spec_add: forall x y, [add x y] = [x] + [y].\n";
+  fprintf fmt "  Proof.\n";
+  fprintf fmt "  intros x y; case x; unfold add; (intros n x1 || intros x1);\n";
+  fprintf fmt "    case y; intros m y1 || intros y1; autorewrite with extr addr; auto;\n";
+  fprintf fmt "    generalize (spec_w0_eq0 x1) || generalize (spec_w0_eq0 y1); \n";
+  fprintf fmt "    case w0_eq0; intros HH; autorewrite with extr addr; try rewrite HH; \n";
+  fprintf fmt "    try rewrite Zplus_0_r; auto.\n";
+  fprintf fmt "  Qed.  \n";
+
+  fprintf fmt "  Let spec_reduce_0: forall x, [reduce_0 x] = [%s0 x].\n" c;
+  fprintf fmt "  Proof.\n";
+  fprintf fmt "  intros x; unfold to_Z, reduce_0.\n";
+  fprintf fmt "  auto.\n";
+  fprintf fmt "  Qed.\n";
+  fprintf fmt "  \n";
+
+  for i = 1 to size + 1 do
+   if (i == size + 1) then
+    fprintf fmt "  Let spec_reduce_%i: forall x, [reduce_%i x] = [%sn 0 x].\n" i i c
+   else
+    fprintf fmt "  Let spec_reduce_%i: forall x, [reduce_%i x] = [%s%i x].\n" i i c i;
+    fprintf fmt "  Proof.\n";
+    fprintf fmt "  intros x; case x; unfold reduce_%i.\n" i;
+    fprintf fmt "  exact (spec_0 w0_spec).\n";
+    fprintf fmt "  intros x1 y1.\n";
+    fprintf fmt "  generalize (spec_w%i_eq0 x1); \n" (i - 1);
+    fprintf fmt "    case w%i_eq0; intros H1; auto.\n" (i - 1);
+    if i <> 1 then 
+      fprintf fmt "  rewrite spec_reduce_%i.\n" (i - 1);
+    fprintf fmt "  rewrite <- (Zplus_0_l [N%i y1]).\n" (i - 1);
+    fprintf fmt "  refine (f_equal2 Zplus _ _); auto.\n";
+    fprintf fmt "  unfold to_Z in H1; rewrite H1; auto.\n";
+    fprintf fmt "  Qed.\n";
+    fprintf fmt "  \n";
+  done;
+
+  fprintf fmt "  Let spec_reduce_n: forall n x, [reduce_n n x] = [%sn n x].\n" c;
+  fprintf fmt "  Proof.\n";
+  fprintf fmt "  intros n; elim n; simpl reduce_n.\n";
+  fprintf fmt "    intros x; rewrite <- spec_reduce_%i; auto.\n" (size + 1);
+  fprintf fmt "  intros n1 Hrec x; case x.\n";
+  fprintf fmt "  unfold to_Z; rewrite make_op_S; auto.\n";
+  fprintf fmt "  exact (spec_0 w0_spec).\n";
+  fprintf fmt "  intros x1 y1; case x1; auto.\n";
+  fprintf fmt "  rewrite Hrec.\n";
+  fprintf fmt "  rewrite <- (Zplus_0_l [%sn n1 y1]).\n" c;
+  fprintf fmt "  unfold to_Z; rewrite make_op_S.\n";
+  fprintf fmt "  refine (f_equal2 Zplus _ _); auto.\n";
+  fprintf fmt "  case n1; auto; intros; rewrite make_op_S; auto.\n";
+  fprintf fmt "  Qed.\n";
+  fprintf fmt "  \n";
+
+  fprintf fmt "   Let to_Z_pos: forall x, 0 <= [x].\n";
+  fprintf fmt "   Proof.\n";
+  fprintf fmt "   intros x; case x; unfold to_Z.\n";
+  for i = 0 to size do
+    fprintf fmt "   intros x1; case (spec_to_Z w%i_spec x1); auto.\n" i;
+  done;
+  fprintf fmt "   intros n x1; case (spec_to_Z (wn_spec n) x1); auto.\n";
+  fprintf fmt "   Qed.\n";
+  fprintf fmt "   \n";
+
+  fprintf fmt "  Let spec_pred: forall x, 0 < [x] -> [pred x] = [x] - 1.\n";
+  fprintf fmt "  Proof.\n";
+  fprintf fmt "  intros x; case x; unfold pred.\n";
+  for i = 0 to size do
+    fprintf fmt "  intros x1 H1; unfold w%i_pred_c; \n" i;
+    fprintf fmt "  generalize (spec_pred_c w%i_spec x1); case znz_pred_c; intros y1.\n" i;
+    fprintf fmt "  rewrite spec_reduce_%i; auto.\n" i;
+    fprintf fmt "  unfold interp_carry; unfold to_Z.\n";
+    fprintf fmt "  case (spec_to_Z w%i_spec x1); intros HH1 HH2.\n" i;
+    fprintf fmt "  case (spec_to_Z w%i_spec y1); intros HH3 HH4 HH5.\n" i;
+    fprintf fmt "  assert (znz_to_Z w%i_op x1 - 1 < 0); auto with zarith.\n" i;
+    fprintf fmt "  unfold to_Z in H1; auto with zarith.\n";
+  done;
+  fprintf fmt "  intros n x1 H1;  \n";
+  fprintf fmt "    generalize (spec_pred_c (wn_spec n) x1); case znz_pred_c; intros y1.\n";
+  fprintf fmt "    rewrite spec_reduce_n; auto.\n";
+  fprintf fmt "  unfold interp_carry; unfold to_Z.\n";
+  fprintf fmt "  case (spec_to_Z (wn_spec n) x1); intros HH1 HH2.\n";
+  fprintf fmt "  case (spec_to_Z (wn_spec n) y1); intros HH3 HH4 HH5.\n";
+  fprintf fmt "  assert (znz_to_Z (make_op n) x1 - 1 < 0); auto with zarith.\n";
+  fprintf fmt "  unfold to_Z in H1; auto with zarith.\n";
+  fprintf fmt "  Qed.\n";
+  fprintf fmt "  \n";
+
+  fprintf fmt "  Let spec_pred0: forall x, [x] = 0 -> [pred x] = 0.\n";
+  fprintf fmt "  Proof.\n";
+  fprintf fmt "  intros x; case x; unfold pred.\n";
+  for i = 0 to size do
+    fprintf fmt "  intros x1 H1; unfold w%i_pred_c; \n" i;
+    fprintf fmt "    generalize (spec_pred_c w%i_spec x1); case znz_pred_c; intros y1.\n" i;
+    fprintf fmt "  unfold interp_carry; unfold to_Z.\n";
+    fprintf fmt "  unfold to_Z in H1; auto with zarith.\n";
+    fprintf fmt "  case (spec_to_Z w%i_spec y1); intros HH3 HH4; auto with zarith.\n" i;
+    fprintf fmt "  intros; exact (spec_0 w0_spec).\n";
+  done;
+  fprintf fmt "  intros n x1 H1; \n";
+  fprintf fmt "    generalize (spec_pred_c (wn_spec n) x1); case znz_pred_c; intros y1.\n";
+  fprintf fmt "  unfold interp_carry; unfold to_Z.\n";
+  fprintf fmt "  unfold to_Z in H1; auto with zarith.\n";
+  fprintf fmt "  case (spec_to_Z (wn_spec n) y1); intros HH3 HH4; auto with zarith.\n";
+  fprintf fmt "  intros; exact (spec_0 w0_spec).\n";
+  fprintf fmt "  Qed.\n";
+  fprintf fmt "  \n";
+  end;
   fprintf fmt "End Make.\n";
   fprintf fmt "\n";
   pp_print_flush fmt ()