NMake : another round of heavy rework

 - generic iterator [iter] factorized in the same way as [same_level]
 - as a consequence, remaining operations [mul] [compare] [div_gt]
   are now defined and proved in a short and nice way and moved to
   NMake.v.
 - lots of other simplifications / factorisations in NMake_gen.
   This file is still macro-generated, but is much shorter,
   and the major part of it is now invariant.
 - As advised by B. Gregoire, try to (re)create clever partial
   applications in code of operators, in order to avoid projecting
   ZnZ fields all the time in base cases. Case 0 can still be improved,
   but it's already better this way :-)

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

4 files changed, 1284 insertions, 1405 deletions

diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index ad7d322ab6..2bb79280c9 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -40,7 +40,7 @@ Notation bigN := BigN.t.
 Delimit Scope bigN_scope with bigN.
 Bind Scope bigN_scope with bigN.
 Bind Scope bigN_scope with BigN.t.
-Bind Scope bigN_scope with BigN.t_.
+Bind Scope bigN_scope with BigN.t'.
 (* Bind Scope has no retroactive effect, let's declare scopes by hand. *)
 Arguments Scope BigN.to_Z [bigN_scope].
 Arguments Scope BigN.succ [bigN_scope].
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index 7d0aef6417..d82e205a68 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -27,13 +27,15 @@ Module Make (W0:CyclicType) <: NType.
 
  Include NMake_gen.Make W0.
 
+ Open Scope Z_scope.
+
  Local Notation "[ x ]" := (to_Z x).
 
  Definition eq (x y : t) := [x] = [y].
 
  Declare Reduction red_t :=
   lazy beta iota delta
-   [iter_t reduce same_level mk_t mk_t_S dom_t dom_op].
+   [iter_t reduce same_level mk_t mk_t_S succ_t dom_t dom_op].
 
  Ltac red_t :=
   match goal with |- ?u => let v := (eval red_t in u) in change v end.
@@ -62,7 +64,7 @@ Module Make (W0:CyclicType) <: NType.
  Proof.
  intros.
  change (Zpos (ZnZ.digits (dom_op n)) <= Zpos (ZnZ.digits (dom_op m))).
- rewrite (digits_dom_op n), (digits_dom_op m).
+ rewrite !digits_dom_op, !Pshiftl_Zpower.
  apply Zmult_le_compat_l; auto with zarith.
  apply Zpower_le_monotone2; auto with zarith.
  Qed.
@@ -84,11 +86,17 @@ Module Make (W0:CyclicType) <: NType.
 
  (** * Successor *)
 
- Local Notation succn := (fun n (x:dom_t n) =>
+ (** NB: it is crucial here and for the rest of this file to preserve
+     the let-in's. They allow to pre-compute once and for all the
+     field access to Z/nZ initial structures (when n=0..6). *)
+
+ Local Notation succn := (fun n =>
   let op := dom_op n in
-  match ZnZ.succ_c x with
+  let succ_c := ZnZ.succ_c in
+  let one := ZnZ.one in
+  fun x => match succ_c x with
    | C0 r => mk_t n r
-   | C1 r => mk_t_S n (WW ZnZ.one r)
+   | C1 r => mk_t_S n (WW one r)
   end).
 
  Definition succ : t -> t := Eval red_t in iter_t succn.
@@ -107,11 +115,13 @@ Module Make (W0:CyclicType) <: NType.
 
  (** * Addition *)
 
- Local Notation addn := (fun n (x y : dom_t n) =>
+ Local Notation addn := (fun n =>
   let op := dom_op n in
-  match ZnZ.add_c x y with
+  let add_c := ZnZ.add_c in
+  let one := ZnZ.one in
+  fun x y =>match add_c x y with
   | C0 r => mk_t n r
-  | C1 r => mk_t_S n (WW ZnZ.one r)
+  | C1 r => mk_t_S n (WW one r)
   end).
 
  Definition add : t -> t -> t := Eval red_t in same_level addn.
@@ -131,8 +141,9 @@ Module Make (W0:CyclicType) <: NType.
 
  (** * Predecessor *)
 
- Local Notation predn := (fun n (x:dom_t n) =>
-  match ZnZ.pred_c x with
+ Local Notation predn := (fun n =>
+  let pred_c := ZnZ.pred_c in
+  fun x => match pred_c x with
    | C0 r => reduce n r
    | C1 _ => zero
   end).
@@ -171,9 +182,9 @@ Module Make (W0:CyclicType) <: NType.
 
  (** * Subtraction *)
 
- Local Notation subn := (fun n (x y : dom_t n) =>
-  let op := dom_op n in
-  match ZnZ.sub_c x y with
+ Local Notation subn := (fun n =>
+  let sub_c := ZnZ.sub_c in
+  fun x y => match sub_c x y with
   | C0 r => reduce n r
   | C1 r => zero
   end).
@@ -214,6 +225,68 @@ Module Make (W0:CyclicType) <: NType.
 
  (** * Comparison *)
 
+ Definition comparen_m n :
+  forall m, word (dom_t n) (S m) -> dom_t n -> comparison :=
+  let op := dom_op n in
+  let zero := @ZnZ.zero _ op in
+  let compare := @ZnZ.compare _ op in
+  let compare0 := compare zero in
+  fun m => compare_mn_1 (dom_t n) (dom_t n) zero compare compare0 compare (S m).
+
+ Let spec_comparen_m:
+  forall n m (x : word (dom_t n) (S m)) (y : dom_t n),
+   comparen_m n m x y = Zcompare (eval n (S m) x) (ZnZ.to_Z y).
+ Proof.
+  intros n m x y.
+  unfold comparen_m, eval.
+  rewrite nmake_double.
+  apply spec_compare_mn_1.
+  exact ZnZ.spec_0.
+  intros. apply ZnZ.spec_compare.
+  exact ZnZ.spec_to_Z.
+  exact ZnZ.spec_compare.
+  exact ZnZ.spec_compare.
+  exact ZnZ.spec_to_Z.
+ Qed.
+
+ Definition comparenm n m wx wy :=
+    let mn := Max.max n m in
+    let d := diff n m in
+    let op := make_op mn in
+    ZnZ.compare
+       (castm (diff_r n m) (extend_tr wx (snd d)))
+       (castm (diff_l n m) (extend_tr wy (fst d))).
+
+ Local Notation compare_folded :=
+   (iter_sym _
+      (fun n => @ZnZ.compare _ (dom_op n))
+      comparen_m
+      comparenm
+      CompOpp).
+
+ Definition compare : t -> t -> comparison :=
+  Eval lazy beta iota delta [iter_sym dom_op dom_t comparen_m] in
+  compare_folded.
+
+ Lemma compare_fold : compare = compare_folded.
+ Proof.
+ lazy beta iota delta [iter_sym dom_op dom_t comparen_m]. reflexivity.
+ Qed.
+
+(** TODO: no need for ZnZ.Spec_rect , _ind, and so on... *)
+
+ Theorem spec_compare : forall x y,
+   compare x y = Zcompare [x] [y].
+ Proof.
+  intros x y. rewrite compare_fold. apply spec_iter_sym; clear x y.
+  intros. apply ZnZ.spec_compare.
+  intros. cbv beta zeta. apply spec_comparen_m.
+  intros n m x y; unfold comparenm.
+  rewrite (spec_cast_l n m x), (spec_cast_r n m y).
+  unfold to_Z; apply ZnZ.spec_compare.
+  intros. subst. apply Zcompare_antisym.
+ Qed.
+
  Definition eq_bool (x y : t) : bool :=
   match compare x y with
   | Eq => true
@@ -241,74 +314,236 @@ Module Make (W0:CyclicType) <: NType.
  intros. unfold min, Zmin. rewrite spec_compare; destruct Zcompare; reflexivity.
  Qed.
 
- (** * Square *)
-
- (** TODO: use reduce (original version was using it for N0 only) *)
+ (** * Multiplication *)
 
- Local Notation squaren :=
-  (fun n (x : dom_t n) => mk_t_S n (ZnZ.square_c x)).
-
- Definition square : t -> t := Eval red_t in iter_t squaren.
-
- Lemma square_fold : square = iter_t squaren.
- Proof. red_t; reflexivity. Qed.
-
- Theorem spec_square: forall x, [square x] = [x] * [x].
+ Definition wn_mul n : forall m, word (dom_t n) (S m) -> dom_t n -> t :=
+  let op := dom_op n in
+  let zero := @ZnZ.zero _ op in
+  let succ := @ZnZ.succ _ op in
+  let add_c := @ZnZ.add_c _ op in
+  let mul_c := @ZnZ.mul_c _ op in
+  let ww := @ZnZ.WW _ op in
+  let ow := @ZnZ.OW _ op in
+  let eq0 := @ZnZ.eq0 _ op in
+  let mul_add := @DoubleMul.w_mul_add _ zero succ add_c mul_c in
+  let mul_add_n1 := @DoubleMul.double_mul_add_n1 _ zero ww ow mul_add in
+  fun m x y =>
+   let (w,r) := mul_add_n1 (S m) x y zero in
+   if eq0 w then mk_t_w' n m r
+   else mk_t_w' n (S m) (WW (extend n m w) r).
+
+ Definition mulnm n m x y :=
+    let mn := Max.max n m in
+    let d := diff n m in
+    let op := make_op mn in
+     reduce_n (S mn) (ZnZ.mul_c
+       (castm (diff_r n m) (extend_tr x (snd d)))
+       (castm (diff_l n m) (extend_tr y (fst d)))).
+
+ Local Notation mul_folded :=
+  (iter_sym _
+    (fun n => let mul_c := ZnZ.mul_c in
+      fun x y => reduce (S n) (succ_t _ (mul_c x y)))
+    wn_mul
+    mulnm
+    (fun x => x)).
+
+ Definition mul : t -> t -> t :=
+  Eval lazy beta iota delta
+   [iter_sym dom_op dom_t reduce succ_t extend zeron
+    wn_mul DoubleMul.w_mul_add mk_t_w'] in
+  mul_folded.
+
+ Lemma mul_fold : mul = mul_folded.
  Proof.
-  intros x. rewrite square_fold. destr_t x as (n,x).
-  rewrite spec_mk_t_S. exact (ZnZ.spec_square_c x).
+  lazy beta iota delta
+   [iter_sym dom_op dom_t reduce succ_t extend zeron
+    wn_mul  DoubleMul.w_mul_add mk_t_w']. reflexivity.
  Qed.
 
- (** * Sqrt *)
-
- Local Notation sqrtn :=
-  (fun n (x : dom_t n) => reduce n (ZnZ.sqrt x)).
+ Lemma spec_muln:
+   forall n (x: word _ (S n)) y,
+     [Nn (S n) (ZnZ.mul_c (Ops:=make_op n) x y)] = [Nn n x] * [Nn n y].
+ Proof.
+    intros n x y; unfold to_Z.
+    rewrite <- ZnZ.spec_mul_c.
+    rewrite make_op_S.
+    case ZnZ.mul_c; auto.
+ Qed.
 
- Definition sqrt : t -> t := Eval red_t in iter_t sqrtn.
+ Lemma spec_mul_add_n1: forall n m x y z,
+  let (q,r) := DoubleMul.double_mul_add_n1 ZnZ.zero ZnZ.WW ZnZ.OW
+          (DoubleMul.w_mul_add ZnZ.zero ZnZ.succ ZnZ.add_c ZnZ.mul_c)
+          (S m) x y z in
+  ZnZ.to_Z q * (base (ZnZ.digits (nmake_op _ (dom_op n) (S m))))
+   + eval n (S m) r =
+  eval n (S m) x * ZnZ.to_Z y + ZnZ.to_Z z.
+ Proof.
+ intros n m x y z.
+ rewrite digits_nmake.
+ unfold eval. rewrite nmake_double.
+ apply DoubleMul.spec_double_mul_add_n1.
+ apply ZnZ.spec_0.
+ exact ZnZ.spec_WW.
+ exact ZnZ.spec_OW.
+ apply DoubleCyclic.spec_mul_add.
+ Qed.
 
- Lemma sqrt_fold : sqrt = iter_t sqrtn.
- Proof. red_t; reflexivity. Qed.
+ Lemma spec_wn_mul : forall n m x y,
+   [wn_mul n m x y] = (eval n (S m) x) * ZnZ.to_Z y.
+ Proof.
+  intros; unfold wn_mul.
+  generalize (spec_mul_add_n1 n m x y ZnZ.zero).
+  case DoubleMul.double_mul_add_n1; intros q r Hqr.
+  rewrite ZnZ.spec_0, Zplus_0_r in Hqr. rewrite <- Hqr.
+  generalize (ZnZ.spec_eq0 q); case ZnZ.eq0; intros HH.
+  rewrite HH; auto. simpl. apply spec_mk_t_w'.
+  clear.
+  rewrite spec_mk_t_w'.
+  set (m' := S m) in *.
+  unfold eval.
+  rewrite nmake_WW. f_equal. f_equal.
+  rewrite <- spec_mk_t.
+  symmetry. apply spec_extend.
+ Qed.
 
- Theorem spec_sqrt: forall x, [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2.
+ Theorem spec_mul : forall x y, [mul x y] = [x] * [y].
  Proof.
-  intros x. rewrite sqrt_fold. destr_t x as (n,x). exact (ZnZ.spec_sqrt x).
+  intros x y. rewrite mul_fold. apply spec_iter_sym; clear x y.
+   intros n x y. cbv zeta beta.
+    rewrite spec_reduce, spec_succ_t, <- ZnZ.spec_mul_c; auto.
+   apply spec_wn_mul.
+   intros n m x y; unfold mulnm. rewrite spec_reduce_n.
+    rewrite (spec_cast_l n m x), (spec_cast_r n m y).
+    apply spec_muln.
+   intros. rewrite Zmult_comm; auto.
  Qed.
 
- (** * Power *)
+ (** * Division by a smaller number *)
 
- Fixpoint power_pos (x:t)(p:positive) : t :=
-  match p with
-  | xH => x
-  | xO p => square (power_pos x p)
-  | xI p => mul (square (power_pos x p)) x
-  end.
+ Definition wn_divn1 n :=
+  let op := dom_op n in
+  let zd := ZnZ.zdigits op in
+  let zero := @ZnZ.zero _ op in
+  let ww := @ZnZ.WW _ op in
+  let head0 := @ZnZ.head0 _ op in
+  let add_mul_div := @ZnZ.add_mul_div _ op in
+  let div21 := @ZnZ.div21 _ op in
+  let compare := @ZnZ.compare _ op in
+  let sub := @ZnZ.sub _ op in
+  let ddivn1 :=
+    DoubleDivn1.double_divn1 zd zero ww head0 add_mul_div div21 compare sub in
+  fun m x y => let (u,v) := ddivn1 (S m) x y in (mk_t_w' n m u, mk_t n v).
+
+ Let div_gtnm n m wx wy :=
+    let mn := Max.max n m in
+    let d := diff n m in
+    let op := make_op mn in
+    let (q, r):= ZnZ.div_gt
+         (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).
+
+ Local Notation div_gt_folded :=
+   (iter _
+     (fun n => let div_gt := ZnZ.div_gt in
+       fun x y => let (u,v) := div_gt x y in (reduce n u, reduce n v))
+     (fun n =>
+       let div_gt := ZnZ.div_gt in
+       fun m x y =>
+         let y' := DoubleBase.get_low (zeron n) (S m) y in
+         let (u,v) := div_gt x y' in (reduce n u, reduce n v))
+      wn_divn1
+      div_gtnm).
+
+ Definition div_gt :=
+  Eval lazy beta iota delta
+   [iter dom_op dom_t reduce zeron wn_divn1 mk_t_w' mk_t] in
+  div_gt_folded.
+
+ Lemma div_gt_fold : div_gt = div_gt_folded.
+ Proof.
+  lazy beta iota delta [iter dom_op dom_t reduce zeron wn_divn1 mk_t_w' mk_t].
+  reflexivity.
+ Qed.
 
- Theorem spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n.
+ Lemma spec_get_endn: forall n m x y,
+  eval n m x  <= [mk_t n y] ->
+   [mk_t n (DoubleBase.get_low (zeron n) m x)] = eval n m x.
  Proof.
- intros x n; generalize x; elim n; clear n x; simpl power_pos.
- intros; rewrite spec_mul; rewrite spec_square; rewrite H.
- rewrite Zpos_xI; rewrite Zpower_exp; auto with zarith.
- rewrite (Zmult_comm 2); rewrite Zpower_mult; auto with zarith.
- rewrite Zpower_2; rewrite Zpower_1_r; auto.
- intros; rewrite spec_square; rewrite H.
- rewrite Zpos_xO; auto with zarith.
- rewrite (Zmult_comm 2); rewrite Zpower_mult; auto with zarith.
- rewrite Zpower_2; auto.
- intros; rewrite Zpower_1_r; auto.
+  intros n m x y H.
+  unfold eval. rewrite nmake_double.
+  rewrite spec_mk_t in *.
+  apply DoubleBase.spec_get_low.
+  apply spec_zeron.
+  exact ZnZ.spec_to_Z.
+  apply Zle_lt_trans with (ZnZ.to_Z y); auto.
+    rewrite <- nmake_double; auto.
+  case (ZnZ.spec_to_Z y); auto.
  Qed.
 
- Definition power (x:t)(n:N) : t := match n with
-  | BinNat.N0 => one
-  | BinNat.Npos p => power_pos x p
- end.
+ Let spec_divn1 n :=
+   DoubleDivn1.spec_double_divn1
+    (ZnZ.zdigits (dom_op n)) (ZnZ.zero:dom_t n)
+    ZnZ.WW ZnZ.head0
+    ZnZ.add_mul_div ZnZ.div21
+    ZnZ.compare ZnZ.sub ZnZ.to_Z
+    ZnZ.spec_to_Z
+    ZnZ.spec_zdigits
+    ZnZ.spec_0 ZnZ.spec_WW ZnZ.spec_head0
+    ZnZ.spec_add_mul_div ZnZ.spec_div21
+    ZnZ.spec_compare ZnZ.spec_sub.
+
+ Lemma spec_div_gt_aux : forall x y, [x] > [y] -> 0 < [y] ->
+   let (q,r) := div_gt x y in
+   [x] = [q] * [y] + [r] /\ 0 <= [r] < [y].
+ Proof.
+  intros x y. rewrite div_gt_fold. apply spec_iter; clear x y.
+   intros n x y H1 H2. simpl.
+    generalize (ZnZ.spec_div_gt x y H1 H2); case ZnZ.div_gt.
+    intros u v. rewrite 2 spec_reduce. auto.
+   intros n m x y H1 H2. cbv zeta beta.
+    generalize (ZnZ.spec_div_gt x
+                (DoubleBase.get_low (zeron n) (S m) y)).
+    case ZnZ.div_gt.
+    intros u v H3; repeat rewrite spec_reduce.
+    generalize (spec_get_endn n (S m) y x). rewrite !spec_mk_t. intros H4.
+    rewrite H4 in H3; auto with zarith.
+   intros n m x y H1 H2.
+    generalize (spec_divn1 n (S m) x y H2).
+    unfold wn_divn1; case DoubleDivn1.double_divn1.
+    intros u v H3.
+    rewrite spec_mk_t_w', spec_mk_t.
+    rewrite <- !nmake_double in H3; auto.
+   intros n m x y H1 H2; unfold div_gtnm.
+    generalize (ZnZ.spec_div_gt
+                   (castm (diff_r n m)
+                     (extend_tr x (snd (diff n m))))
+                   (castm (diff_l n m)
+                     (extend_tr y (fst (diff n m))))).
+    case ZnZ.div_gt.
+    intros xx yy HH.
+    repeat rewrite spec_reduce_n.
+    rewrite (spec_cast_l n m x), (spec_cast_r n m y).
+    unfold to_Z; apply HH.
+    rewrite (spec_cast_l n m x) in H1; auto.
+    rewrite (spec_cast_r n m y) in H1; auto.
+    rewrite (spec_cast_r n m y) in H2; auto.
+ Qed.
 
- Theorem spec_power: forall x n, [power x n] = [x] ^ Z_of_N n.
+ Theorem spec_div_gt: forall x y, [x] > [y] -> 0 < [y] ->
+  let (q,r) := div_gt x y in
+  [q] = [x] / [y] /\ [r] = [x] mod [y].
  Proof.
- destruct n; simpl. apply spec_1.
- apply spec_power_pos.
+  intros x y H1 H2; generalize (spec_div_gt_aux x y H1 H2); case div_gt.
+  intros q r (H3, H4); split.
+  apply (Zdiv_unique [x] [y] [q] [r]); auto.
+  rewrite Zmult_comm; auto.
+  apply (Zmod_unique [x] [y] [q] [r]); auto.
+  rewrite Zmult_comm; auto.
  Qed.
 
- (** * Div *)
+ (** * General Division *)
 
  Definition div_eucl (x y : t) : t * t :=
   if eq_bool y zero then (zero,zero) else
@@ -353,7 +588,87 @@ Module Make (W0:CyclicType) <: NType.
   injection H; auto.
  Qed.
 
- (** * Modulo *)
+ (** * Modulo by a smaller number *)
+
+ Definition wn_modn1 n :=
+  let op := dom_op n in
+  let zd := ZnZ.zdigits op in
+  let zero := @ZnZ.zero _ op in
+  let head0 := @ZnZ.head0 _ op in
+  let add_mul_div := @ZnZ.add_mul_div _ op in
+  let div21 := @ZnZ.div21 _ op in
+  let compare := @ZnZ.compare _ op in
+  let sub := @ZnZ.sub _ op in
+  let dmodn1 :=
+    DoubleDivn1.double_modn1 zd zero head0 add_mul_div div21 compare sub in
+  fun m x y => reduce n (dmodn1 (S m) x y).
+
+ Let mod_gtnm n m wx wy :=
+    let mn := Max.max n m in
+    let d := diff n m in
+    let op := make_op mn in
+    reduce_n mn (ZnZ.modulo_gt
+         (castm (diff_r n m) (extend_tr wx (snd d)))
+         (castm (diff_l n m) (extend_tr wy (fst d)))).
+
+ Local Notation mod_gt_folded :=
+   (iter _
+      (fun n => let modulo_gt := ZnZ.modulo_gt in
+        fun x y => reduce n (modulo_gt x y))
+      (fun n => let modulo_gt := ZnZ.modulo_gt in
+        fun m x y =>
+          reduce n (modulo_gt x (DoubleBase.get_low (zeron n) (S m) y)))
+      wn_modn1
+      mod_gtnm).
+
+ Definition mod_gt :=
+  Eval lazy beta iota delta [iter dom_op dom_t reduce wn_modn1 zeron] in
+  mod_gt_folded.
+
+ Lemma mod_gt_fold : mod_gt = mod_gt_folded.
+ Proof.
+  lazy beta iota delta [iter dom_op dom_t reduce wn_modn1 zeron].
+  reflexivity.
+ Qed.
+
+ Let spec_modn1 n :=
+   DoubleDivn1.spec_double_modn1
+    (ZnZ.zdigits (dom_op n)) (ZnZ.zero:dom_t n)
+    ZnZ.WW ZnZ.head0
+    ZnZ.add_mul_div ZnZ.div21
+    ZnZ.compare ZnZ.sub ZnZ.to_Z
+    ZnZ.spec_to_Z
+    ZnZ.spec_zdigits
+    ZnZ.spec_0 ZnZ.spec_WW ZnZ.spec_head0
+    ZnZ.spec_add_mul_div ZnZ.spec_div21
+    ZnZ.spec_compare ZnZ.spec_sub.
+
+ Theorem spec_mod_gt:
+   forall x y, [x] > [y] -> 0 < [y] -> [mod_gt x y] = [x] mod [y].
+ Proof.
+ intros x y. rewrite mod_gt_fold. apply spec_iter; clear x y.
+ intros n x y H1 H2. simpl. rewrite spec_reduce.
+   exact (ZnZ.spec_modulo_gt x y H1 H2).
+ intros n m x y H1 H2. cbv zeta beta. rewrite spec_reduce.
+  rewrite <- spec_mk_t in H1.
+  rewrite <- (spec_get_endn n (S m) y x); auto with zarith.
+  rewrite spec_mk_t.
+  apply ZnZ.spec_modulo_gt; auto.
+  rewrite <- (spec_get_endn n (S m) y x), !spec_mk_t in H1; auto with zarith.
+  rewrite <- (spec_get_endn n (S m) y x), !spec_mk_t in H2; auto with zarith.
+ intros n m x y H1 H2. unfold wn_modn1. rewrite spec_reduce.
+  unfold eval; rewrite nmake_double.
+  apply (spec_modn1 n); auto.
+ intros n m x y H1 H2; unfold mod_gtnm.
+  repeat rewrite spec_reduce_n.
+  rewrite (spec_cast_l n m x), (spec_cast_r n m y).
+  unfold to_Z; apply ZnZ.spec_modulo_gt.
+  rewrite (spec_cast_l n m x) in H1; auto.
+  rewrite (spec_cast_r n m y) in H1; auto.
+  rewrite (spec_cast_r n m y) in H2; auto.
+ Qed.
+
+ (** * General Modulo *)
 
  Definition modulo (x y : t) : t :=
   if eq_bool y zero then zero else
@@ -381,6 +696,74 @@ Module Make (W0:CyclicType) <: NType.
  apply spec_mod_gt; auto with zarith.
  Qed.
 
+ (** * Square *)
+
+ Local Notation squaren := (fun n =>
+   let square_c := ZnZ.square_c in
+   fun x => reduce (S n) (succ_t _ (square_c x))).
+
+ Definition square : t -> t := Eval red_t in iter_t squaren.
+
+ Lemma square_fold : square = iter_t squaren.
+ Proof. red_t; reflexivity. Qed.
+
+ Theorem spec_square: forall x, [square x] = [x] * [x].
+ Proof.
+  intros x. rewrite square_fold. destr_t x as (n,x).
+  rewrite spec_succ_t. exact (ZnZ.spec_square_c x).
+ Qed.
+
+ (** * Square Root *)
+
+ Local Notation sqrtn := (fun n =>
+   let sqrt := ZnZ.sqrt in
+   fun x => reduce n (sqrt x)).
+
+ Definition sqrt : t -> t := Eval red_t in iter_t sqrtn.
+
+ Lemma sqrt_fold : sqrt = iter_t sqrtn.
+ Proof. red_t; reflexivity. Qed.
+
+ Theorem spec_sqrt: forall x, [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2.
+ Proof.
+  intros x. rewrite sqrt_fold. destr_t x as (n,x). exact (ZnZ.spec_sqrt x).
+ Qed.
+
+ (** * Power *)
+
+ Fixpoint power_pos (x:t)(p:positive) : t :=
+  match p with
+  | xH => x
+  | xO p => square (power_pos x p)
+  | xI p => mul (square (power_pos x p)) x
+  end.
+
+ Theorem spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n.
+ Proof.
+ intros x n; generalize x; elim n; clear n x; simpl power_pos.
+ intros; rewrite spec_mul; rewrite spec_square; rewrite H.
+ rewrite Zpos_xI; rewrite Zpower_exp; auto with zarith.
+ rewrite (Zmult_comm 2); rewrite Zpower_mult; auto with zarith.
+ rewrite Zpower_2; rewrite Zpower_1_r; auto.
+ intros; rewrite spec_square; rewrite H.
+ rewrite Zpos_xO; auto with zarith.
+ rewrite (Zmult_comm 2); rewrite Zpower_mult; auto with zarith.
+ rewrite Zpower_2; auto.
+ intros; rewrite Zpower_1_r; auto.
+ Qed.
+
+ Definition power (x:t)(n:N) : t := match n with
+  | BinNat.N0 => one
+  | BinNat.Npos p => power_pos x p
+ end.
+
+ Theorem spec_power: forall x n, [power x n] = [x] ^ Z_of_N n.
+ Proof.
+ destruct n; simpl. apply spec_1.
+ apply spec_power_pos.
+ Qed.
+
+
  (** * digits
 
      Number of digits in the representation of a numbers
@@ -388,7 +771,9 @@ Module Make (W0:CyclicType) <: NType.
      NB: This function isn't a morphism for setoid [eq].
  *)
 
- Local Notation digitsn := (fun n _ => ZnZ.digits (dom_op n)).
+ Local Notation digitsn := (fun n =>
+   let digits := ZnZ.digits (dom_op n) in
+   fun _ => digits).
 
  Definition digits : t -> positive := Eval red_t in iter_t digitsn.
 
@@ -598,7 +983,7 @@ Module Make (W0:CyclicType) <: NType.
  unfold base.
  apply Zlt_le_trans with (1 := pheight_correct x).
  apply Zpower_le_monotone2; auto with zarith.
- rewrite (digits_dom_op (_ _)); auto with zarith.
+ rewrite (digits_dom_op (_ _)), Pshiftl_Zpower. auto with zarith.
  Qed.
 
  Definition of_N (x:N) : t :=
@@ -624,7 +1009,9 @@ Module Make (W0:CyclicType) <: NType.
      NB: these functions are not morphism for setoid [eq].
  *)
 
- Local Notation head0n := (fun n x => reduce n (ZnZ.head0 x)).
+ Local Notation head0n := (fun n =>
+   let head0 := ZnZ.head0 in
+   fun x => reduce n (head0 x)).
 
  Definition head0 : t -> t := Eval red_t in iter_t head0n.
 
@@ -652,7 +1039,9 @@ Module Make (W0:CyclicType) <: NType.
  rewrite head0_fold, digits_fold. destr_t x as (n,x). exact (ZnZ.spec_head0 x).
  Qed.
 
- Local Notation tail0n := (fun n x => reduce n (ZnZ.tail0 x)).
+ Local Notation tail0n := (fun n =>
+  let tail0 := ZnZ.tail0 in
+  fun x => reduce n (tail0 x)).
 
  Definition tail0 : t -> t := Eval red_t in iter_t tail0n.
 
@@ -677,7 +1066,9 @@ Module Make (W0:CyclicType) <: NType.
      NB: this function is not a morphism for setoid [eq].
  *)
 
- Local Notation Ndigitsn := (fun n _ => reduce n (ZnZ.zdigits (dom_op n))).
+ Local Notation Ndigitsn := (fun n =>
+  let d := reduce n (ZnZ.zdigits (dom_op n)) in
+  fun _ => d).
 
  Definition Ndigits : t -> t := Eval red_t in iter_t Ndigitsn.
 
@@ -692,12 +1083,16 @@ Module Make (W0:CyclicType) <: NType.
 
  (** * Binary logarithm *)
 
- Local Notation log2n := (fun n x =>
+ Local Notation log2n := (fun n =>
   let op := dom_op n in
-  reduce n (ZnZ.sub_carry (ZnZ.zdigits op) (ZnZ.head0 x))).
+  let zdigits := ZnZ.zdigits op in
+  let head0 := ZnZ.head0 in
+  let sub_carry := ZnZ.sub_carry in
+  fun x => reduce n (sub_carry zdigits (head0 x))).
 
  Definition log2 : t -> t := Eval red_t in
-   fun x => if eq_bool x zero then zero else iter_t log2n x.
+   let log2 := iter_t log2n in
+   fun x => if eq_bool x zero then zero else log2 x.
 
  Lemma log2_fold :
    log2 = fun x => if eq_bool x zero then zero else iter_t log2n x.
@@ -775,10 +1170,14 @@ Module Make (W0:CyclicType) <: NType.
 
  (** * Right shift *)
 
- Local Notation shiftrn := (fun n (p x : dom_t n) =>
+ Local Notation shiftrn := (fun n =>
    let op := dom_op n in
-   match ZnZ.sub_c (ZnZ.zdigits op) p with
-   | C0 d => reduce n (ZnZ.add_mul_div d ZnZ.zero x)
+   let zdigits := ZnZ.zdigits op in
+   let sub_c := ZnZ.sub_c in
+   let add_mul_div := ZnZ.add_mul_div in
+   let zzero := ZnZ.zero in
+   fun p x => match sub_c zdigits p with
+   | C0 d => reduce n (add_mul_div d zzero x)
    | C1 _ => zero
    end).
 
@@ -834,9 +1233,11 @@ Module Make (W0:CyclicType) <: NType.
  (** First an unsafe version, working correctly only if
      the representation is large enough *)
 
- Local Notation unsafe_shiftln := (fun n p x =>
-   let ops := dom_op n in
-   reduce n (ZnZ.add_mul_div p x ZnZ.zero)).
+ Local Notation unsafe_shiftln := (fun n =>
+   let op := dom_op n in
+   let add_mul_div := ZnZ.add_mul_div in
+   let zero := ZnZ.zero in
+   fun p x => reduce n (add_mul_div p x zero)).
 
  Definition unsafe_shiftl : t -> t -> t := Eval red_t in
    same_level unsafe_shiftln.
@@ -857,7 +1258,7 @@ Module Make (W0:CyclicType) <: NType.
   transitivity (Zpos (ZnZ.digits (dom_op n))); auto.
   apply digits_dom_op_incr; auto.
  clear p x.
- intros n p x K HK Hx Hp. lazy zeta. rewrite spec_reduce.
+ intros n p x K HK Hx Hp. simpl. rewrite spec_reduce.
  destruct (ZnZ.spec_to_Z x).
  destruct (ZnZ.spec_to_Z p).
  rewrite ZnZ.spec_add_mul_div by (omega with *).
@@ -891,8 +1292,9 @@ Module Make (W0:CyclicType) <: NType.
  (** Then we define a function doubling the size of the representation
      but without changing the value of the number. *)
 
- Local Notation double_size_n :=
-  (fun n x => mk_t_S n (WW ZnZ.zero x)).
+ Local Notation double_size_n := (fun n =>
+  let zero := ZnZ.zero in
+  fun x => mk_t_S n (WW zero x)).
 
  Definition double_size : t -> t := Eval red_t in
    iter_t double_size_n.
@@ -910,7 +1312,8 @@ Module Make (W0:CyclicType) <: NType.
    forall x, Zpos (digits (double_size x)) = 2 * (Zpos (digits x)).
  Proof.
  intros x. rewrite ! digits_level, double_size_level.
- rewrite !(digits_dom_op (_ _)), inj_S, Zpower_Zsucc; auto with zarith.
+ rewrite 2 digits_dom_op, 2 Pshiftl_Zpower,
+         inj_S, Zpower_Zsucc; auto with zarith.
  ring.
  Qed.
 
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index c1bd20c789..2736013c64 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -8,95 +8,76 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*S NMake_gen.ml : this file generates NMake.v *)
+(*S NMake_gen.ml : this file generates NMake_gen.v *)
 
 
-(*s The two parameters that control the generation: *)
+(*s The parameter that control the generation: *)
 
 let size = 6 (* how many times should we repeat the Z/nZ --> Z/2nZ
                 process before relying on a generic construct *)
-let gen_proof = true  (* should we generate proofs ? *)
-
 
 (*s Some utilities *)
 
-let t = "t"
-let c = "N"
-let pz n = if n == 0 then "ZnZ.zero" else "W0"
-let rec gen2 n = if n == 0 then "1" else if n == 1 then "2"
-                 else "2 * " ^ (gen2 (n - 1))
-let rec genxO n s =
-  if n == 0 then s else " (xO" ^ (genxO (n - 1) s) ^ ")"
-
 let rec iter_str n s = if n = 0 then "" else (iter_str (n-1) s) ^ s
 
+let rec iter_str_gen n f = if n < 0 then "" else (iter_str_gen (n-1) f) ^ (f n)
+
 let rec iter_name i j base sep =
   if i >= j then base^(string_of_int i)
   else (iter_name i (j-1) base sep)^sep^" "^base^(string_of_int j)
 
-(* Standard printer, with a final newline *)
 let pr s = Printf.printf (s^^"\n")
-(* Printing to /dev/null *)
-let pn s = Printf.ifprintf stdout s
-(* Proof printer : prints iff gen_proof is true *)
-let pp = if gen_proof then pr else pn
-(* Printer for admitted parts : prints iff gen_proof is false *)
-let pa = if not gen_proof then pr else pn
-(* Same as before, but without the final newline *)
-let pr0 = Printf.printf
-let pp0 = if gen_proof then pr0 else pn
-
 
 (*s The actual printing *)
 
 let _ =
 
-  pr "(************************************************************************)";
-  pr "(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)";
-  pr "(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)";
-  pr "(*   \\VV/  **************************************************************)";
-  pr "(*    //   *      This file is distributed under the terms of the       *)";
-  pr "(*         *       GNU Lesser General Public License Version 2.1        *)";
-  pr "(************************************************************************)";
-  pr "(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)";
-  pr "(************************************************************************)";
-  pr "";
-  pr "(** * NMake_gen *)";
-  pr "";
-  pr "(** From a cyclic Z/nZ representation to arbitrary precision natural numbers.*)";
-  pr "";
-  pr "(** Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT ! *)";
-  pr "";
-  pr "Require Import BigNumPrelude ZArith CyclicAxioms";
-  pr " DoubleType DoubleMul DoubleDivn1 DoubleCyclic Nbasic";
-  pr " Wf_nat StreamMemo.";
-  pr "";
-  pr "Module Make (W0:CyclicType) <: NAbstract.";
-  pr "";
+pr
+"(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \\VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
 
-  pr " (** * The word types *)";
-  pr "";
+(** * NMake_gen *)
 
-  pr " Local Notation w0 := W0.t.";
-  for i = 1 to size do
-    pr " Definition w%i := zn2z w%i." i (i-1)
-  done;
-  pr "";
+(** From a cyclic Z/nZ representation to arbitrary precision natural numbers.*)
 
-  pr " (** * The operation type classes for the word types *)";
-  pr "";
+(** Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT ! *)
 
-  pr " Local Notation w0_op := W0.ops.";
-  for i = 1 to min 3 size do
-    pr " Instance w%i_op : ZnZ.Ops w%i := mk_zn2z_ops w%i_op." i i (i-1)
-  done;
-  for i = 4 to size do
-    pr " Instance w%i_op : ZnZ.Ops w%i := mk_zn2z_ops_karatsuba w%i_op." i i (i-1)
-  done;
-  for i = size+1 to size+3 do
-    pr " Instance w%i_op : ZnZ.Ops (word w%i %i%%nat) := mk_zn2z_ops_karatsuba w%i_op." i size (i-size) (i-1)
-  done;
-  pr "";
+Require Import BigNumPrelude ZArith CyclicAxioms
+ DoubleType DoubleMul DoubleDivn1 DoubleCyclic Nbasic
+ Wf_nat StreamMemo.
+
+Module Make (W0:CyclicType) <: NAbstract.
+
+ (** * The word types *)
+";
+
+pr " Local Notation w0 := W0.t.";
+for i = 1 to size do
+  pr " Definition w%i := zn2z w%i." i (i-1)
+done;
+pr "";
+
+pr " (** * The operation type classes for the word types *)
+";
+
+pr " Local Notation w0_op := W0.ops.";
+for i = 1 to min 3 size do
+  pr " Instance w%i_op : ZnZ.Ops w%i := mk_zn2z_ops w%i_op." i i (i-1)
+done;
+for i = 4 to size do
+  pr " Instance w%i_op : ZnZ.Ops w%i := mk_zn2z_ops_karatsuba w%i_op." i i (i-1)
+done;
+for i = size+1 to size+3 do
+  pr " Instance w%i_op : ZnZ.Ops (word w%i %i) := mk_zn2z_ops_karatsuba w%i_op." i size (i-size) (i-1)
+done;
+pr "";
 
   pr " Section Make_op.";
   pr "  Variable mk : forall w', ZnZ.Ops w' -> ZnZ.Ops (zn2z w').";
@@ -126,24 +107,36 @@ let _ =
   pr "  := dmemo_get _ omake_op n make_op_list.";
   pr "";
 
-  pr "";
-  pr " Lemma make_op_omake: forall n, make_op n = omake_op n.";
-  pr " intros n; unfold make_op, make_op_list.";
-  pr " refine (dmemo_get_correct _ _ _).";
-  pr " Qed.";
-  pr "";
+pr " Ltac unfold_ops := unfold omake_op, make_op_aux, w%i_op, w%i_op." (size+3) (size+2);
+
+pr
+"
+ Lemma make_op_omake: forall n, make_op n = omake_op n.
+ Proof.
+ intros n; unfold make_op, make_op_list.
+ refine (dmemo_get_correct _ _ _).
+ Qed.
 
+ Theorem make_op_S: forall n,
+   make_op (S n) = mk_zn2z_ops_karatsuba (make_op n).
+ Proof.
+ intros n. do 2 rewrite make_op_omake.
+ revert n. fix IHn 1.
+ do 3 (destruct n; [unfold_ops; reflexivity|]).
+ simpl mk_zn2z_ops_karatsuba. simpl word in *.
+ rewrite <- IHn. auto.
+ Qed.
 
-  pr " (** * The main type [t], isomorphic with [exists n, word w0 n] *)";
-  pr "";
+ (** * The main type [t], isomorphic with [exists n, word w0 n] *)
+";
 
-  pr " Inductive %s_ :=" t;
+  pr " Inductive t' :=";
   for i = 0 to size do
-    pr "  | %s%i : w%i -> %s_" c i i t
+    pr "  | N%i : w%i -> t'" i i
   done;
-  pr "  | %sn : forall n, word w%i (S n) -> %s_." c size t;
+  pr "  | Nn : forall n, word w%i (S n) -> t'." size;
   pr "";
-  pr " Definition %s := %s_." t t;
+  pr " Definition t := t'.";
   pr "";
 
   pr " (** * A generic toolbox for building and deconstructing [t] *)";
@@ -151,6 +144,10 @@ let _ =
 
   pr " Local Notation SizePlus n := %sn%s."
     (iter_str size "(S ") (iter_str size ")");
+  pr " Local Notation Size := (SizePlus O).";
+  pr "";
+
+  pr " Tactic Notation \"do_size\" tactic(t) := do %i t." (size+1);
   pr "";
 
   pr " Definition dom_t n := match n with";
@@ -161,34 +158,38 @@ let _ =
   pr " end.";
   pr "";
 
-  pr " Instance dom_op n : ZnZ.Ops (dom_t n) | 10.";
-  pa " Admitted.";
-  pp " Proof.";
-  pp "  do %i (destruct n; [simpl;auto with *|])." (size+1);
-  pp "  unfold dom_t. auto with *.";
-  pp " Defined.";
-  pr "";
+pr
+" Instance dom_op n : ZnZ.Ops (dom_t n) | 10.
+ Proof.
+  do_size (destruct n; [simpl;auto with *|]).
+  unfold dom_t. auto with *.
+ Defined.
+";
 
-  pr " Definition iter_t {A:Type}(f : forall n, dom_t n -> A)(x:t) : A :=";
-  pr "  match x with";
+  pr " Definition iter_t {A:Type}(f : forall n, dom_t n -> A) : t -> A :=";
+  for i = 0 to size do
+   pr "  let f%i := f %i in" i i;
+  done;
+  pr "  let fn n := f (SizePlus (S n)) in";
+  pr "  fun x => match x with";
   for i = 0 to size do
-    pr "   | %s%i wx => f %i wx" c i i;
+    pr "   | N%i wx => f%i wx" i i;
   done;
-  pr "   | %sn n wx => f (SizePlus (S n)) wx" c;
+  pr "   | Nn n wx => fn n wx";
   pr "  end.";
   pr "";
 
   pr " Definition mk_t (n:nat) : dom_t n -> t :=";
   pr "  match n as n' return dom_t n' -> t with";
   for i = 0 to size do
-    pr "   | %i => %s%i" i c i;
+    pr "   | %i => N%i" i i;
   done;
-  pr "   | %s(S n) => %sn n" (if size=0 then "" else "SizePlus ") c;
+  pr "   | %s(S n) => Nn n" (if size=0 then "" else "SizePlus ");
   pr "  end.";
   pr "";
 
-pr "
- Definition level := iter_t (fun n _ => n).
+pr
+" Definition level := iter_t (fun n _ => n).
 
  Inductive View_t : t -> Prop :=
   Mk_t : forall n (x : dom_t n), View_t (mk_t n x).
@@ -196,511 +197,518 @@ pr "
  Lemma destr_t : forall x, View_t x.
  Proof.
  intros x. generalize (Mk_t (level x)). destruct x; simpl; auto.
- Qed.
-";
+ Defined.
 
-pr "
  Lemma iter_mk_t : forall A (f:forall n, dom_t n -> A),
  forall n x, iter_t f (mk_t n x) = f n x.
  Proof.
- do %i (destruct n; try reflexivity).
+ do_size (destruct n; try reflexivity).
  Qed.
-" (size+1);
 
-pr "
  (** * Projection to ZArith *)
 
  Definition to_Z : t -> Z :=
   Eval lazy beta iota delta [iter_t dom_t dom_op] in
   iter_t (fun _ x => ZnZ.to_Z x).
-";
 
-  pr " Open Scope Z_scope.";
-  pr " Notation \"[ x ]\" := (to_Z x).";
-  pr "";
+ Notation \"[ x ]\" := (to_Z x).
 
-pr "
  Theorem spec_mk_t : forall n (x:dom_t n), [mk_t n x] = ZnZ.to_Z x.
  Proof.
  intros. change to_Z with (iter_t (fun _ x => ZnZ.to_Z x)).
  rewrite iter_mk_t; auto.
  Qed.
-";
 
-  pp " (* Regular make op (no karatsuba) *)";
-  pp " Fixpoint nmake_op (ww:Type) (ww_op: ZnZ.Ops ww) (n: nat) :";
-  pp "       ZnZ.Ops (word ww n) :=";
-  pp "  match n return ZnZ.Ops (word ww n) with";
-  pp "   O => ww_op";
-  pp "  | S n1 => mk_zn2z_ops (nmake_op ww ww_op n1)";
-  pp "  end.";
-  pp "";
-  pp " (* Simplification by rewriting for nmake_op *)";
-  pp " Theorem nmake_op_S: forall ww (w_op: ZnZ.Ops ww) x,";
-  pp "   nmake_op _ w_op (S x) = mk_zn2z_ops (nmake_op _ w_op x).";
-  pp " auto.";
-  pp " Qed.";
-  pp "";
-
-
-  pr " (* Eval and extend functions for each level *)";
-  for i = 0 to size do
-    pp " Let nmake_op%i := nmake_op _ w%i_op." i i;
-    pp " Let eval%in n := ZnZ.to_Z (Ops:=nmake_op%i n)." i i;
-    if i == 0 then
-      pr " Let extend%i := DoubleBase.extend (WW (ZnZ.zero:w0))." i
-    else
-      pr " Let extend%i := DoubleBase.extend (WW (W0: w%i))." i i;
-  done;
-  pr "";
+ (** * Regular make op, without memoization or karatsuba
 
+     This will normally never be used for actual computations,
+     but only for specification purpose when using
+     [word (dom_t n) m] intermediate values. *)
 
-  pp " Theorem digits_doubled:forall n ww (w_op: ZnZ.Ops ww),";
-  pp "    ZnZ.digits (nmake_op _ w_op n) =";
-  pp "    DoubleBase.double_digits (ZnZ.digits w_op) n.";
-  pp " Proof.";
-  pp " intros n; elim n; auto; clear n.";
-  pp " intros n Hrec ww ww_op; simpl DoubleBase.double_digits.";
-  pp " rewrite <- Hrec; auto.";
-  pp " Qed.";
-  pp "";
-  pp " Theorem nmake_double: forall n ww (w_op: ZnZ.Ops ww),";
-  pp "    ZnZ.to_Z (Ops:=nmake_op _ w_op n) =";
-  pp "    @DoubleBase.double_to_Z _ (ZnZ.digits w_op) (ZnZ.to_Z (Ops:=w_op)) n.";
-  pp " Proof.";
-  pp " intros n; elim n; auto; clear n.";
-  pp " intros n Hrec ww ww_op; simpl DoubleBase.double_to_Z; unfold zn2z_to_Z.";
-  pp " rewrite <- Hrec; auto.";
-  pp " unfold DoubleBase.double_wB; rewrite <- digits_doubled; auto.";
-  pp " Qed.";
-  pp "";
-
-
-  pp " Theorem digits_nmake:forall n ww (w_op: ZnZ.Ops ww),";
-  pp "    ZnZ.digits (nmake_op _ w_op (S n)) =";
-  pp "    xO (ZnZ.digits (nmake_op _ w_op n)).";
-  pp " Proof.";
-  pp " auto.";
-  pp " Qed.";
-  pp "";
-
-
-  pp " Theorem znz_nmake_op: forall ww ww_op n xh xl,";
-  pp "  ZnZ.to_Z (Ops:=nmake_op ww ww_op (S n)) (WW xh xl) =";
-  pp "   ZnZ.to_Z (Ops:=nmake_op ww ww_op n) xh *";
-  pp "    base (ZnZ.digits (nmake_op ww ww_op n)) +";
-  pp "   ZnZ.to_Z (Ops:=nmake_op ww ww_op n) xl.";
-  pp " Proof.";
-  pp " auto.";
-  pp " Qed.";
-  pp "";
-
-  pp " Theorem make_op_S: forall n,";
-  pp "   make_op (S n) = mk_zn2z_ops_karatsuba (make_op n).";
-  pp " intro n.";
-  pp " do 2 rewrite make_op_omake.";
-  pp " pattern n; apply lt_wf_ind; clear n.";
-  pp " intros n; case n; clear n.";
-  pp "   intros _; unfold omake_op, make_op_aux, w%i_op; apply refl_equal." (size + 2);
-  pp " intros n; case n; clear n.";
-  pp "   intros _; unfold omake_op, make_op_aux, w%i_op; apply refl_equal." (size + 3);
-  pp " intros n; case n; clear n.";
-  pp "   intros _; unfold omake_op, make_op_aux, w%i_op, w%i_op; apply refl_equal." (size + 3) (size + 2);
-  pp " intros n Hrec.";
-  pp "   change (omake_op (S (S (S (S n))))) with";
-  pp "          (mk_zn2z_ops_karatsuba (mk_zn2z_ops_karatsuba (mk_zn2z_ops_karatsuba (omake_op (S n))))).";
-  pp "   change (omake_op (S (S (S n)))) with";
-  pp "         (mk_zn2z_ops_karatsuba (mk_zn2z_ops_karatsuba (mk_zn2z_ops_karatsuba (omake_op n)))).";
-  pp "   rewrite Hrec; auto with arith.";
-  pp " Qed.";
-  pp "";
+ Fixpoint nmake_op (ww:Type) (ww_op: ZnZ.Ops ww) (n: nat) :
+       ZnZ.Ops (word ww n) :=
+  match n return ZnZ.Ops (word ww n) with
+   O => ww_op
+  | S n1 => mk_zn2z_ops (nmake_op ww ww_op n1)
+  end.
 
-pr "
- Lemma dom_t_S : forall n, zn2z (dom_t n) = dom_t (S n).
+ Let eval n m := ZnZ.to_Z (Ops:=nmake_op _ (dom_op n) m).
+
+ Theorem nmake_op_S: forall ww (w_op: ZnZ.Ops ww) x,
+   nmake_op _ w_op (S x) = mk_zn2z_ops (nmake_op _ w_op x).
  Proof.
-  do %i (destruct n; try reflexivity).
- Defined.
+ auto.
+ Qed.
 
- Definition cast w w' (H:w=w') (x:w) : w' :=
-   match H in _=y return y with
-   | eq_refl => x
-   end.
+ Theorem digits_nmake_S :forall n ww (w_op: ZnZ.Ops ww),
+    ZnZ.digits (nmake_op _ w_op (S n)) =
+    xO (ZnZ.digits (nmake_op _ w_op n)).
+ Proof.
+ auto.
+ Qed.
 
- Definition mk_t_S n (x:zn2z (dom_t n)) : t :=
-  Eval lazy beta delta [cast dom_t_S] in
-  mk_t (S n) (cast _ _ (dom_t_S n) x).
+ Theorem digits_nmake : forall n ww (w_op: ZnZ.Ops ww),
+    ZnZ.digits (nmake_op _ w_op n) = Pshiftl (ZnZ.digits w_op) n.
+ Proof.
+ induction n. auto.
+ intros ww ww_op; simpl Pshiftl. rewrite <- IHn; auto.
+ Qed.
 
- Theorem spec_mk_t_S : forall n (x:zn2z (dom_t n)),
-  [mk_t_S n x] = zn2z_to_Z (base (ZnZ.digits (dom_op n))) ZnZ.to_Z x.
+ Theorem nmake_double: forall n ww (w_op: ZnZ.Ops ww),
+    ZnZ.to_Z (Ops:=nmake_op _ w_op n) =
+    @DoubleBase.double_to_Z _ (ZnZ.digits w_op) (ZnZ.to_Z (Ops:=w_op)) n.
  Proof.
- intros.
- do %i (destruct n; [reflexivity|]).
- simpl. rewrite !make_op_S. reflexivity.
+ intros n; elim n; auto; clear n.
+ intros n Hrec ww ww_op; simpl DoubleBase.double_to_Z; unfold zn2z_to_Z.
+ rewrite <- Hrec; auto.
+ unfold DoubleBase.double_wB; rewrite <- digits_nmake; auto.
  Qed.
 
- Lemma mk_t_S_level : forall n x, level (mk_t_S n x) = S n.
+ Theorem nmake_WW: forall ww ww_op n xh xl,
+  (ZnZ.to_Z (Ops:=nmake_op ww ww_op (S n)) (WW xh xl) =
+   ZnZ.to_Z (Ops:=nmake_op ww ww_op n) xh *
+    base (ZnZ.digits (nmake_op ww ww_op n)) +
+   ZnZ.to_Z (Ops:=nmake_op ww ww_op n) xl)%%Z.
  Proof.
- do %i (destruct n; try reflexivity).
+ auto.
  Qed.
-" (size+1) (size+1) (size+1);
 
-  pr " (** * The specification proofs for the word operators *)";
-  pr "";
+ (** * The specification proofs for the word operators *)
+";
 
   if size <> 0 then
-  pr " Typeclasses Opaque %s." (iter_name 1 size "w" " ");
+  pr " Typeclasses Opaque %s." (iter_name 1 size "w" "");
   pr "";
 
-  pp " Instance w0_spec: ZnZ.Specs w0_op := W0.specs.";
+  pr " Instance w0_spec: ZnZ.Specs w0_op := W0.specs.";
   for i = 1 to min 3 size do
-    pp " Instance w%i_spec: ZnZ.Specs w%i_op := mk_zn2z_specs w%i_spec." i i (i-1)
+    pr " Instance w%i_spec: ZnZ.Specs w%i_op := mk_zn2z_specs w%i_spec." i i (i-1)
   done;
   for i = 4 to size do
-    pp " Instance w%i_spec: ZnZ.Specs w%i_op := mk_zn2z_specs_karatsuba w%i_spec." i i (i-1)
-  done;
-  for i = size+1 to size+3 do
-    pp " Instance w%i_spec: ZnZ.Specs w%i_op := mk_zn2z_specs_karatsuba w%i_spec." i i (i-1)
+    pr " Instance w%i_spec: ZnZ.Specs w%i_op := mk_zn2z_specs_karatsuba w%i_spec." i i (i-1)
   done;
-  pp "";
+  pr " Instance w%i_spec: ZnZ.Specs w%i_op := mk_zn2z_specs_karatsuba w%i_spec." (size+1) (size+1) size;
 
-  pp " Instance wn_spec (n:nat) : ZnZ.Specs (make_op n).";
-  pp " Proof.";
-  pp "  elim n; clear n.";
-  pp "    exact w%i_spec." (size + 1);
-  pp "  intros n Hrec; rewrite make_op_S.";
-  pp "  exact (mk_zn2z_specs_karatsuba Hrec).";
-  pp " Qed.";
-  pp "";
 
 pr "
+ Instance wn_spec (n:nat) : ZnZ.Specs (make_op n).
+ Proof.
+  induction n.
+  rewrite make_op_omake; simpl; auto with *.
+  rewrite make_op_S. exact (mk_zn2z_specs_karatsuba IHn).
+ Qed.
+
  Instance dom_spec n : ZnZ.Specs (dom_op n) | 10.
  Proof.
-  do %i (destruct n; auto with *). apply wn_spec.
+  do_size (destruct n; auto with *). apply wn_spec.
  Qed.
-" (size+1);
-
-  for i = 1 to size + 2 do
-    pp " Let to_Z_%i: forall x y," i;
-    pp "   ZnZ.to_Z (Ops:=w%i_op) (WW x y) =" i;
-    pp "    ZnZ.to_Z (Ops:=w%i_op) x * base (ZnZ.digits w%i_op) + ZnZ.to_Z (Ops:=w%i_op) y." (i-1) (i-1) (i-1);
-    pp " Proof.";
-    pp " auto.";
-    pp " Qed.";
-    pp "";
-  done;
 
-  pp " Let to_Z_n: forall n x y,";
-  pp "   ZnZ.to_Z (Ops:=make_op (S n)) (WW x y) =";
-  pp "    ZnZ.to_Z (Ops:=make_op n) x * base (ZnZ.digits (make_op n)) + ZnZ.to_Z (Ops:=make_op n) y.";
-  pp " Proof.";
-  pp " intros n x y; rewrite make_op_S; auto.";
-  pp " Qed.";
-  pp "";
+ Let make_op_WW : forall n x y,
+   (ZnZ.to_Z (Ops:=make_op (S n)) (WW x y) =
+    ZnZ.to_Z (Ops:=make_op n) x * base (ZnZ.digits (make_op n))
+     + ZnZ.to_Z (Ops:=make_op n) y)%%Z.
+ Proof.
+ intros n x y; rewrite make_op_S; auto.
+ Qed.
 
-  for i = 0 to size do
-    pp " Theorem digits_w%i:  ZnZ.digits w%i_op = ZnZ.digits (nmake_op _ w0_op %i)." i i i;
-    if i == 0 then
-      pp " auto."
-    else
-      pp " rewrite digits_nmake; rewrite <- digits_w%i; auto." (i - 1);
-    pp " Qed.";
-    pp "";
-    pp " Let spec_double_eval%in: forall n, eval%in n = DoubleBase.double_to_Z (ZnZ.digits w%i_op) (ZnZ.to_Z (Ops:=w%i_op)) n." i i i i;
-    pp " Proof.";
-    pp "  intros n; exact (nmake_double n w%i w%i_op)." i i;
-    pp " Qed.";
-    pp "";
-  done;
+ (** * Zero *)
 
-  for i = 0 to size do
-    for j = 0 to (size - i) do
-      pp " Theorem digits_w%in%i: ZnZ.digits w%i_op = ZnZ.digits (nmake_op _ w%i_op %i)." i j (i + j) i j;
-      pp " Proof.";
-      if j == 0 then
-        if i == 0 then
-          pp " auto."
-        else
-          begin
-            pp " apply trans_equal with (xO (ZnZ.digits w%i_op))." (i + j -1);
-            pp "  auto.";
-            pp "  unfold nmake_op; auto.";
-          end
-      else
-        begin
-          pp " apply trans_equal with (xO (ZnZ.digits w%i_op))." (i + j -1);
-          pp "  auto.";
-          pp " rewrite digits_nmake.";
-          pp " rewrite digits_w%in%i." i (j - 1);
-          pp " auto.";
-        end;
-      pp " Qed.";
-      pp "";
-      pp " Let spec_eval%in%i: forall x, [%s%i x] = eval%in %i x." i j c (i + j) i j;
-      pp " Proof.";
-      if j == 0 then
-        pp " intros x; rewrite spec_double_eval%in; unfold DoubleBase.double_to_Z, to_Z; auto." i
-      else
-        begin
-          pp " intros x; case x.";
-          pp "   auto.";
-          pp " intros xh xl; unfold to_Z; rewrite to_Z_%i." (i + j);
-          pp " rewrite digits_w%in%i." i (j - 1);
-          pp " generalize (spec_eval%in%i); unfold to_Z; intros HH; repeat rewrite HH." i (j - 1);
-          pp " unfold eval%in, nmake_op%i." i i;
-          pp " rewrite (znz_nmake_op _ w%i_op %i); auto." i (j - 1);
-        end;
-      pp " Qed.";
-      if i + j <> size  then
-        begin
-          pp " Let spec_extend%in%i: forall x, [%s%i x] = [%s%i (extend%i %i x)]." i (i + j + 1) c i c (i + j + 1) i j;
-          if j == 0 then
-            begin
-              pp " intros x; change (extend%i 0 x) with (WW (ZnZ.zero (Ops:=w%i_op)) x)." i (i + j);
-              pp " unfold to_Z; rewrite to_Z_%i." (i + j + 1);
-              pp " rewrite ZnZ.spec_0; auto.";
-            end
-          else
-            begin
-              pp " intros x; change (extend%i %i x) with (WW (ZnZ.zero (Ops:=w%i_op)) (extend%i %i x))." i j (i + j) i (j - 1);
-              pp " unfold to_Z; rewrite to_Z_%i." (i + j + 1);
-              pp " rewrite ZnZ.spec_0.";
-              pp " generalize (spec_extend%in%i x); unfold to_Z." i (i + j);
-              pp " intros HH; rewrite <- HH; auto.";
-            end;
-          pp " Qed.";
-          pp "";
-        end;
-    done;
-
-    pp " Theorem digits_w%in%i: ZnZ.digits w%i_op = ZnZ.digits (nmake_op _ w%i_op %i)." i (size - i + 1) (size + 1) i (size - i + 1);
-    pp " Proof.";
-    pp " apply trans_equal with (xO (ZnZ.digits w%i_op))." size;
-    pp "  auto.";
-    pp " rewrite digits_nmake.";
-    pp " rewrite digits_w%in%i." i (size - i);
-    pp " auto.";
-    pp " Qed.";
-    pp "";
-
-    pp " Let spec_eval%in%i: forall x, [%sn 0  x] = eval%in %i x." i (size - i + 1) c i (size - i + 1);
-    pp " Proof.";
-    pp " intros x; case x.";
-    pp "   auto.";
-    pp " intros xh xl; unfold to_Z; rewrite to_Z_%i." (size + 1);
-    pp " rewrite digits_w%in%i." i (size - i);
-    pp " generalize (spec_eval%in%i); unfold to_Z; intros HH; repeat rewrite HH." i (size - i);
-    pp " unfold eval%in, nmake_op%i." i i;
-    pp " rewrite (znz_nmake_op _ w%i_op %i); auto." i (size - i);
-    pp " Qed.";
-    pp "";
-
-    pp " Let spec_eval%in%i: forall x, [%sn 1  x] = eval%in %i x." i (size - i + 2) c i (size - i + 2);
-    pp " intros x; case x.";
-    pp "   auto.";
-    pp " intros xh xl; unfold to_Z; rewrite to_Z_%i." (size + 2);
-    pp " rewrite digits_w%in%i." i (size + 1 - i);
-    pp " generalize (spec_eval%in%i); unfold to_Z; change (make_op 0) with (w%i_op); intros HH; repeat rewrite HH." i (size + 1 - i) (size + 1);
-    pp " unfold eval%in, nmake_op%i." i i;
-    pp " rewrite (znz_nmake_op _ w%i_op %i); auto." i (size + 1 - i);
-    pp " Qed.";
-    pp "";
-  done;
+ Definition zero0 : w0 := ZnZ.zero.
 
-  pp " Let digits_w%in: forall n," size;
-  pp "   ZnZ.digits (make_op n) = ZnZ.digits (nmake_op _ w%i_op (S n))." size;
-  pp " intros n; elim n; clear n.";
-  pp "  change (ZnZ.digits (make_op 0)) with (xO (ZnZ.digits w%i_op))." size;
-  pp "  rewrite nmake_op_S; apply sym_equal; auto.";
-  pp "  intros  n Hrec.";
-  pp "  replace (ZnZ.digits (make_op (S n))) with (xO (ZnZ.digits (make_op n))).";
-  pp "  rewrite Hrec.";
-  pp "  rewrite nmake_op_S; apply sym_equal; auto.";
-  pp "  rewrite make_op_S; apply sym_equal; auto.";
-  pp " Qed.";
-  pp "";
-
-  pp " Let spec_eval%in: forall n x, [%sn n x] = eval%in (S n) x." size c size;
-  pp " intros n; elim n; clear n.";
-  pp "   exact spec_eval%in1." size;
-  pp " intros n Hrec x; case x; clear x.";
-  pp "  unfold to_Z, eval%in, nmake_op%i." size size;
-  pp "    rewrite make_op_S; rewrite nmake_op_S; auto.";
-  pp " intros xh xl.";
-  pp "  unfold to_Z in Hrec |- *.";
-  pp "  rewrite to_Z_n.";
-  pp "  rewrite digits_w%in." size;
-  pp "  repeat rewrite Hrec.";
-  pp "  unfold eval%in, nmake_op%i." size size;
-  pp "  apply sym_equal; rewrite nmake_op_S; auto.";
-  pp " Qed.";
-  pp "";
-
-  pp " Let spec_extend%in: forall n x, [%s%i x] = [%sn n (extend%i n x)]." size c size c size ;
-  pp " intros n; elim n; clear n.";
-  pp "   intros x; change (extend%i 0 x) with (WW (ZnZ.zero (Ops:=w%i_op)) x)." size size;
-  pp "   unfold to_Z.";
-  pp "   change (make_op 0) with w%i_op." (size + 1);
-  pp "   rewrite to_Z_%i; rewrite ZnZ.spec_0; auto." (size + 1);
-  pp " intros n Hrec x.";
-  pp "   change (extend%i (S n) x) with (WW W0 (extend%i n x))." size size;
-  pp "   unfold to_Z in Hrec |- *; rewrite to_Z_n; auto.";
-  pp "   rewrite <- Hrec.";
-  pp "  replace (ZnZ.to_Z (Ops:=make_op n) W0) with 0; auto.";
-  pp "  case n; auto; intros; rewrite make_op_S; auto.";
-  pp " Qed.";
-  pp "";
+ Definition zeron n : dom_t n :=
+  match n with
+   | O => zero0
+   | SizePlus (S n) => W0
+   | _ => W0
+  end.
+
+ Lemma spec_zeron : forall n, ZnZ.to_Z (zeron n) = 0%%Z.
+ Proof.
+  do_size (destruct n; [exact ZnZ.spec_0|]).
+  destruct n; auto. simpl. rewrite make_op_S. exact ZnZ.spec_0.
+ Qed.
+
+ (** * Digits *)
+
+ Lemma digits_make_op_0 : forall n,
+  ZnZ.digits (make_op n) = Pshiftl (ZnZ.digits (dom_op Size)) (S n).
+ Proof.
+ induction n.
+ auto.
+ replace (ZnZ.digits (make_op (S n))) with (xO (ZnZ.digits (make_op n))).
+  rewrite IHn; auto.
+ rewrite make_op_S; auto.
+ Qed.
+
+ Lemma digits_make_op : forall n,
+  ZnZ.digits (make_op n) = Pshiftl (ZnZ.digits w0_op) (SizePlus (S n)).
+ Proof.
+ intros. rewrite digits_make_op_0.
+ replace (SizePlus (S n)) with (S n + Size) by (rewrite <- plus_comm; auto).
+ rewrite Pshiftl_plus. auto.
+ Qed.
 
-pr "
  Lemma digits_dom_op : forall n,
-  Zpos (ZnZ.digits (dom_op n)) = Zpos (ZnZ.digits W0.ops) * 2 ^ Z_of_nat n.
+  ZnZ.digits (dom_op n) = Pshiftl (ZnZ.digits w0_op) n.
  Proof.
- intros. rewrite Zmult_comm.
- do %i (destruct n; try reflexivity).
- simpl.
- rewrite <- shift_pos_correct. f_equal.
- rewrite shift_pos_nat.
- rewrite ?nat_of_P_succ_morphism, nat_of_P_o_P_of_succ_nat_eq_succ.
- unfold shift_nat. simpl.
- generalize (digits_w%in n); simpl; intros ->.
- rewrite digits_doubled.
- rewrite digits_w%i, ?digits_nmake. simpl.
- induction n; simpl; congruence.
+ do_size (destruct n; try reflexivity).
+ exact (digits_make_op n).
  Qed.
-" (size+1) size size;
-
-  pp " Let spec_extendn_0: forall n wx, [%sn n (extend n _ wx)] = [%sn 0 wx]." c c;
-  pp " intros n; elim n; auto.";
-  pp " intros n1 Hrec wx; simpl extend; rewrite <- Hrec; auto.";
-  pp " unfold to_Z.";
-  pp " case n1; auto; intros n2; repeat rewrite make_op_S; auto.";
-  pp " Qed.";
-  pp "";
-  pp " Let spec_extendn0_0: forall n wx, [%sn (S n) (WW W0 wx)] = [%sn n wx]." c c;
-  pp " Proof.";
-  pp " intros n x; unfold to_Z.";
-  pp " rewrite to_Z_n.";
-  pp " rewrite <- (Zplus_0_l (ZnZ.to_Z (Ops:=make_op n) x)).";
-  pp " apply (f_equal2 Zplus); auto.";
-  pp " case n; auto.";
-  pp " intros n1; rewrite make_op_S; auto.";
-  pp " Qed.";
-  pp "";
-  pp " Let spec_extend_tr: forall m n (w: word _ (S n)),";
-  pp " [%sn (m + n) (extend_tr w m)] = [%sn n w]." c c;
-  pp " Proof.";
-  pp " induction m; auto.";
-  pp " intros n x; simpl extend_tr.";
-  pp " simpl plus; rewrite spec_extendn0_0; auto.";
-  pp " Qed.";
-  pp "";
-  pp " Let spec_cast_l: forall n m x1,";
-  pp " [%sn (Max.max n m)" c;
-  pp " (castm (diff_r n m) (extend_tr x1 (snd (diff n m))))] =";
-  pp " [%sn n x1]." c;
-  pp " Proof.";
-  pp " intros n m x1; case (diff_r n m); simpl castm.";
-  pp " rewrite spec_extend_tr; auto.";
-  pp " Qed.";
-  pp "";
-  pp " Let spec_cast_r: forall n m x1,";
-  pp " [%sn (Max.max n m)" c;
-  pp "  (castm (diff_l n m) (extend_tr x1 (fst (diff n m))))] =";
-  pp " [%sn m x1]." c;
-  pp " Proof.";
-  pp " intros n m x1; case (diff_l n m); simpl castm.";
-  pp " rewrite spec_extend_tr; auto.";
-  pp " Qed.";
-  pp "";
-
-  pr " Section SameLevel.";
-  pr "";
-  pr "  Variable res: Type.";
-  pr "  Variable P : Z -> Z -> res -> Prop.";
-  pr "  Variable f : forall n, dom_t n -> dom_t n -> res.";
-  pr "  Variable Pf : forall n x y, P (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y).";
-  pr "";
-  for i = 0 to size do
-    pr "  Let f%i : w%i -> w%i -> res := f %i." i i i i;
-  done;
-  pr "  Let fn n := f (SizePlus (S n)).";
-  pr "";
-  for i = 0 to size do
-    pr "  Let Pf%i : forall x y : w%i, P [%s%i x] [%s%i y] (f%i x y) := Pf %i." i i c i c i i i;
-  done;
-  pr "  Let Pfn n : forall x y, P [%sn n x] [%sn n y] (fn n x y) := Pf (SizePlus (S n))." c c;
-  pr "";
-  pr "  (* We level the two arguments before applying *)";
-  pr "  (* the functions at each level                *)";
-  pr "";
-  pr "  Definition same_level (x y: t_): res := Eval lazy zeta beta iota delta";
-  pr "   [ DoubleBase.extend DoubleBase.extend_aux %s ]" (iter_name 0 (size-1) "extend" "");
-  pr "  in match x, y with";
-  for i = 0 to size do
-    for j = 0 to i - 1 do
-      pr "  | %s%i wx, %s%i wy => f%i wx (extend%i %i wy)" c i c j i j (i - j -1);
-    done;
-    pr "  | %s%i wx, %s%i wy => f%i wx wy" c i c i i;
-    for j = i + 1 to size do
-      pr "  | %s%i wx, %s%i wy => f%i (extend%i %i wx) wy" c i c j j i (j - i - 1);
-    done;
-    if i == size then
-      pr "  | %s%i wx, %sn m wy => fn m (extend%i m wx) wy" c size c size
-    else
-      pr "  | %s%i wx, %sn m wy => fn m (extend%i m (extend%i %i wx)) wy" c i c size i (size - i - 1);
-  done;
-  for i = 0 to size do
-    if i == size then
-      pr "  | %sn n wx, %s%i wy => fn n wx (extend%i n wy)" c c size size
-    else
-      pr "  | %sn n wx, %s%i wy => fn n wx (extend%i n (extend%i %i wy))" c c i size i (size - i - 1);
-  done;
-  pr "  | %sn n wx, Nn m wy =>" c;
-  pr "    let mn := Max.max n m in";
-  pr "    let d := diff n m in";
-  pr "     fn mn";
-  pr "       (castm (diff_r n m) (extend_tr wx (snd d)))";
-  pr "       (castm (diff_l n m) (extend_tr wy (fst d)))";
-  pr "  end.";
-  pr "";
 
-  pp "  Lemma spec_same_level_0: forall x y, P [x] [y] (same_level x y).";
-  pp "  Proof.";
-  pp "  intros x; case x; clear x; unfold same_level.";
-  for i = 0 to size do
-    pp "    intros x y; case y; clear y.";
-    for j = 0 to i - 1 do
-      pp "     intros y; rewrite spec_extend%in%i; apply Pf%i." j i i;
-    done;
-    pp "     intros y; apply Pf%i." i;
-    for j = i + 1 to size do
-      pp "     intros y; rewrite spec_extend%in%i; apply Pf%i." i j j;
-    done;
-    if i == size then
-      pp "     intros m y; rewrite (spec_extend%in m); apply (Pfn m)." size
-    else
-      pp "     intros m y; rewrite spec_extend%in%i; rewrite (spec_extend%in m); apply (Pfn m)." i size size;
-  done;
-  pp "    intros n x y; case y; clear y.";
-  for i = 0 to size do
-    if i == size then
-      pp "    intros y; rewrite (spec_extend%in n); apply (Pfn n)." size
-    else
-      pp "    intros y; rewrite spec_extend%in%i; rewrite (spec_extend%in n); apply (Pfn n)." i size size;
+ Lemma digits_dom_op_nmake : forall n m,
+  ZnZ.digits (dom_op (m+n)) = ZnZ.digits (nmake_op _ (dom_op n) m).
+ Proof.
+ intros. rewrite digits_nmake, 2 digits_dom_op. apply Pshiftl_plus.
+ Qed.
+
+ (** * Conversion between [zn2z (dom_t n)] and [dom_t (S n)].
+
+     These two types are provably equal, but not convertible,
+     hence we need some work. We now avoid using generic casts
+     (i.e. rewrite via proof of equalities in types), since
+     proving things with them is a mess.
+ *)
+
+ Definition succ_t n : zn2z (dom_t n) -> dom_t (S n) :=
+  match n with
+   | SizePlus (S _) => fun x => x
+   | _ => fun x => x
+  end.
+
+ Lemma spec_succ_t : forall n x,
+  ZnZ.to_Z (succ_t n x) =
+  zn2z_to_Z (base (ZnZ.digits (dom_op n))) ZnZ.to_Z x.
+ Proof.
+ do_size (destruct n ; [reflexivity|]).
+ intros. simpl. rewrite make_op_S. simpl. auto.
+ Qed.
+
+ Definition pred_t n : dom_t (S n) -> zn2z (dom_t n) :=
+  match n with
+   | SizePlus (S _) => fun x => x
+   | _ => fun x => x
+  end.
+
+ Lemma succ_pred_t : forall n x, succ_t n (pred_t n x) = x.
+ Proof.
+ do_size (destruct n ; [reflexivity|]). reflexivity.
+ Qed.
+
+ (** We can hence project from [zn2z (dom_t n)] to [t] : *)
+
+ Definition mk_t_S n (x : zn2z (dom_t n)) : t :=
+  mk_t (S n) (succ_t n x).
+
+ Lemma spec_mk_t_S : forall n x,
+  [mk_t_S n x] = zn2z_to_Z (base (ZnZ.digits (dom_op n))) ZnZ.to_Z x.
+ Proof.
+ intros. unfold mk_t_S. rewrite spec_mk_t. apply spec_succ_t.
+ Qed.
+
+ Lemma mk_t_S_level : forall n x, level (mk_t_S n x) = S n.
+ Proof.
+ intros. unfold mk_t_S, level. rewrite iter_mk_t; auto.
+ Qed.
+
+ (** * Conversion from [word (dom_t n) m] to [dom_t (m+n)].
+
+     Things are more complex here. We start with a naive version
+     that breaks zn2z-trees and reconstruct them. Doing this is
+     quite unfortunate, but I don't know how to fully avoid that.
+     (cast someday ?). Then we build an optimized version where
+     all basic cases (n<=6 or m<=7) are nicely handled.
+ *)
+
+ Definition zn2z_map {A} {B} (f:A->B) (x:zn2z A) : zn2z B :=
+  match x with
+   | W0 => W0
+   | WW h l => WW (f h) (f l)
+  end.
+
+ Lemma zn2z_map_id : forall A f (x:zn2z A), (forall u, f u = u) ->
+   zn2z_map f x = x.
+ Proof.
+  destruct x; auto; intros.
+  simpl; f_equal; auto.
+ Qed.
+
+ (** The naive version *)
+
+ Fixpoint plus_t n m : word (dom_t n) m -> dom_t (m+n) :=
+  match m as m' return word (dom_t n) m' -> dom_t (m'+n) with
+   | O => fun x => x
+   | S m => fun x => succ_t _ (zn2z_map (plus_t n m) x)
+  end.
+
+ Theorem spec_plus_t : forall n m (x:word (dom_t n) m),
+  ZnZ.to_Z (plus_t n m x) = eval n m x.
+ Proof.
+ unfold eval.
+ induction m.
+ simpl; auto.
+ intros.
+ simpl plus_t; simpl plus. rewrite spec_succ_t.
+ destruct x.
+ simpl; auto.
+ fold word in w, w0.
+ simpl. rewrite 2 IHm. f_equal. f_equal. f_equal.
+ apply digits_dom_op_nmake.
+ Qed.
+
+ Definition mk_t_w n m (x:word (dom_t n) m) : t :=
+   mk_t (m+n) (plus_t n m x).
+
+ Theorem spec_mk_t_w : forall n m (x:word (dom_t n) m),
+  [mk_t_w n m x] = eval n m x.
+ Proof.
+ intros. unfold mk_t_w. rewrite spec_mk_t. apply spec_plus_t.
+ Qed.
+
+ (** The optimized version.
+
+     NB: the last particular case for m could depend on n,
+     but it's simplier to just expand everywhere up to m=7
+     (cf [mk_t_w'] later).
+ *)
+
+ Definition plus_t' n : forall m, word (dom_t n) m -> dom_t (m+n) :=
+   match n return (forall m, word (dom_t n) m -> dom_t (m+n)) with
+     | SizePlus (S n') as n => plus_t n
+     | _ as n =>
+         fun m => match m return (word (dom_t n) m -> dom_t (m+n)) with
+                    | SizePlus (S (S m')) as m => plus_t n m
+                    | _ => fun x => x
+                  end
+   end.
+
+ Lemma plus_t_equiv : forall n m x,
+  plus_t' n m x = plus_t n m x.
+ Proof.
+  (do_size try destruct n); try reflexivity;
+   (do_size try destruct m); try destruct m; try reflexivity;
+     simpl; symmetry; repeat (intros; apply zn2z_map_id; trivial).
+ Qed.
+
+ Lemma spec_plus_t' : forall n m x,
+  ZnZ.to_Z (plus_t' n m x) = eval n m x.
+ Proof.
+ intros; rewrite plus_t_equiv. apply spec_plus_t.
+ Qed.
+
+ (** Particular cases [Nk x] = eval i j x with specific k,i,j
+     can be solved by the following tactic *)
+
+ Ltac solve_eval :=
+  intros; rewrite <- spec_plus_t'; unfold to_Z; simpl dom_op; reflexivity.
+
+ (** The last particular case that remains useful *)
+
+ Lemma spec_eval_size : forall n x, [Nn n x] = eval Size (S n) x.
+ Proof.
+ induction n.
+ solve_eval.
+ destruct x as [ | xh xl ].
+  simpl. unfold eval. rewrite make_op_S. rewrite nmake_op_S. auto.
+ fold word in *.
+ unfold to_Z in *. rewrite make_op_WW.
+ unfold eval in *. rewrite nmake_WW.
+ f_equal; auto.
+ f_equal; auto.
+ f_equal.
+ rewrite <- digits_dom_op_nmake. rewrite plus_comm; auto.
+ Qed.
+
+ (** An optimized [mk_t_w].
+
+     We could say mk_t_w' := mk_t _ (plus_t' n m x)
+     (TODO: WHY NOT, BTW ??).
+     Instead we directly define functions for all intersting [n],
+     reverting to naive [mk_t_w] at places that should normally
+     never be used (see [mul] and [div_gt]).
+ *)
+";
+
+for i = 0 to size-1 do
+let pattern = (iter_str (size+1-i) "(S ") ^ "_" ^ (iter_str (size+1-i) ")") in
+pr
+" Let mk_t_%iw m := Eval cbv beta zeta iota delta [ mk_t plus ] in
+  match m return word w%i (S m) -> t with
+    | %s as p => mk_t_w %i (S p)
+    | p => mk_t (%i+p)
+  end.
+" i i pattern i (i+1)
+done;
+
+pr
+" Let mk_t_w' n : forall m, word (dom_t n) (S m) -> t :=
+  match n return (forall m, word (dom_t n) (S m) -> t) with";
+for i = 0 to size-1 do pr "    | %i => mk_t_%iw" i i done;
+pr
+"    | Size => Nn
+    | _ as n' => fun m => mk_t_w n' (S m)
+  end.
+";
+
+pr
+" Ltac solve_spec_mk_t_w' :=
+  rewrite <- spec_plus_t';
+  match goal with _ : word (dom_t ?n) ?m |- _ => apply (spec_mk_t (n+m)) end.
+
+ Theorem spec_mk_t_w' :
+  forall n m x, [mk_t_w' n m x] = eval n (S m) x.
+ Proof.
+ intros.
+ repeat (apply spec_mk_t_w || (destruct n;
+  [repeat (apply spec_mk_t_w || (destruct m; [solve_spec_mk_t_w'|]))|])).
+ apply spec_eval_size.
+ Qed.
+
+ (** * Extend : injecting [dom_t n] into [word (dom_t n) (S m)] *)
+
+ Definition extend n m (x:dom_t n) : word (dom_t n) (S m) :=
+  DoubleBase.extend_aux m (WW (zeron n) x).
+
+ Lemma spec_extend : forall n m x,
+  [mk_t n x] = eval n (S m) (extend n m x).
+ Proof.
+ intros. unfold eval, extend.
+ rewrite spec_mk_t.
+ assert (H : forall (x:dom_t n),
+              (ZnZ.to_Z (zeron n) * base (ZnZ.digits (dom_op n)) + ZnZ.to_Z x =
+              ZnZ.to_Z x)%%Z).
+  clear; intros; rewrite spec_zeron; auto.
+ rewrite <- (@DoubleBase.spec_extend _
+              (WW (zeron n)) (ZnZ.digits (dom_op n)) ZnZ.to_Z H m x).
+ simpl. rewrite digits_nmake, <- nmake_double. auto.
+ Qed.
+
+ (** A particular case of extend, used in [same_level]:
+     [extend_size] is [extend Size] *)
+
+ Definition extend_size := DoubleBase.extend (WW (W0:dom_t Size)).
+
+ Lemma spec_extend_size : forall n x, [mk_t Size x] = [Nn n (extend_size n x)].
+ Proof.
+ intros. rewrite spec_eval_size. apply (spec_extend Size n).
+ Qed.
+
+ (** Misc results about extensions *)
+
+ Let spec_extend_WW : forall n x,
+  [Nn (S n) (WW W0 x)] = [Nn n x].
+ Proof.
+ intros n x.
+ set (N:=SizePlus (S n)).
+ change ([Nn (S n) (extend N 0 x)]=[mk_t N x]).
+ rewrite (spec_extend N 0).
+ solve_eval.
+ Qed.
+
+ Let spec_extend_tr: forall m n w,
+ [Nn (m + n) (extend_tr w m)] = [Nn n w].
+ Proof.
+ induction m; auto.
+ intros n x; simpl extend_tr.
+ simpl plus; rewrite spec_extend_WW; auto.
+ Qed.
+
+ Let spec_cast_l: forall n m x1,
+ [Nn n x1] =
+ [Nn (Max.max n m) (castm (diff_r n m) (extend_tr x1 (snd (diff n m))))].
+ Proof.
+ intros n m x1; case (diff_r n m); simpl castm.
+ rewrite spec_extend_tr; auto.
+ Qed.
+
+ Let spec_cast_r: forall n m x1,
+ [Nn m x1] =
+ [Nn (Max.max n m) (castm (diff_l n m) (extend_tr x1 (fst (diff n m))))].
+ Proof.
+ intros n m x1; case (diff_l n m); simpl castm.
+ rewrite spec_extend_tr; auto.
+ Qed.
+
+ Ltac unfold_lets :=
+  match goal with
+   | h : _ |- _ => unfold h; clear h; unfold_lets
+   | _ => idtac
+  end.
+
+ (** * [same_level]
+
+     Generic binary operator construction, by extending the smaller
+     argument to the level of the other.
+ *)
+
+ Section SameLevel.
+
+  Variable res: Type.
+  Variable P : Z -> Z -> res -> Prop.
+  Variable f : forall n, dom_t n -> dom_t n -> res.
+  Variable Pf : forall n x y, P (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y).
+";
+
+for i = 0 to size do
+pr "  Let f%i : w%i -> w%i -> res := f %i." i i i i
+done;
+pr
+"  Let fn n := f (SizePlus (S n)).
+
+  Let Pf' :
+   forall n x y u v, u = [mk_t n x] -> v = [mk_t n y] -> P u v (f n x y).
+  Proof.
+  intros. subst. rewrite 2 spec_mk_t. apply Pf.
+  Qed.
+";
+
+let ext i j s =
+  if j <= i then s else Printf.sprintf "(extend %i %i %s)" i (j-i-1) s
+in
+
+pr "  Notation same_level_folded := (fun x y => match x, y with";
+for i = 0 to size do
+  for j = 0 to size do
+    pr "  | N%i wx, N%i wy => f%i %s %s" i j (max i j) (ext i j "wx") (ext j i "wy")
   done;
-  pp "    intros m y; rewrite <- (spec_cast_l n m x);";
-  pp "          rewrite <- (spec_cast_r n m y); apply (Pfn (Max.max n m)).";
-  pp "  Qed.";
-  pp "";
+  pr "  | N%i wx, Nn m wy => fn m (extend_size m %s) wy" i (ext i size "wx")
+done;
+for i = 0 to size do
+  pr "  | Nn n wx, N%i wy => fn n wx (extend_size n %s)" i (ext i size "wy")
+done;
+pr
+"  | Nn n wx, Nn m wy =>
+    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).
+";
 
-  pr " End SameLevel.";
-  pr "";
-  pr " Implicit Arguments same_level [res].";
+pr
+"  Definition same_level := Eval lazy beta iota delta
+   [ DoubleBase.extend DoubleBase.extend_aux extend zeron ]
+  in same_level_folded.
+
+  Lemma spec_same_level_0: forall x y, P [x] [y] (same_level x y).
+  Proof.
+  change same_level with same_level_folded. unfold_lets.
+  destruct x, y; apply Pf'; simpl mk_t; rewrite <- ?spec_extend_size;
+  match goal with
+   | |- context [ extend ?n ?m _ ] => apply (spec_extend n m)
+   | |- context [ castm _ _ ] => apply spec_cast_l || apply spec_cast_r
+   | _ => reflexivity
+  end.
+  Qed.
+
+ End SameLevel.
+
+ Implicit Arguments same_level [res].
 
-pr "
  Theorem spec_same_level_dep :
   forall res
    (P : nat -> Z -> Z -> res -> Prop)
-   (Pantimon : forall n m z z' r, (n <= m)%%nat -> P m z z' r -> P n z z' r)
+   (Pantimon : forall n m z z' r, n <= m -> P m z z' r -> P n z z' r)
    (f : forall n, dom_t n -> dom_t n -> res)
    (Pf: forall n x y, P n (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y)),
    forall x y, P (level y) [x] [y] (same_level f x y).
@@ -708,828 +716,292 @@ pr "
  intros res P Pantimon f Pf.
  set (f' := fun n x y => (n, f n x y)).
  set (P' := fun z z' r => P (fst r) z z' (snd r)).
- assert (FST : forall x y, (level y <= fst (same_level f' x y))%%nat)
+ assert (FST : forall x y, level y <= fst (same_level f' x y))
   by (destruct x, y; simpl; omega with * ).
  assert (SND : forall x y, same_level f x y = snd (same_level f' x y))
   by (destruct x, y; reflexivity).
  intros. eapply Pantimon; [eapply FST|].
  rewrite SND. eapply (@spec_same_level_0 _ P' f'); eauto.
  Qed.
-";
 
-  pr "";
-  pr " Section Iter.";
-  pr "";
-  pr "  Variable res: Type.";
-  pr "  Variable P: Z -> Z -> res -> Prop.";
-  pr "  (* Abstraction function for each level *)";
-  for i = 0 to size do
-    pr "  Variable f%i: w%i -> w%i -> res." i i i;
-    pr "  Variable f%in: forall n, w%i -> word w%i (S n) -> res." i i i;
-    pr "  Variable fn%i: forall n, word w%i (S n) -> w%i -> res." i i i;
-    pp "  Variable Pf%i: forall x y, P [%s%i x] [%s%i y] (f%i x y)." i c i c i i;
-    if i == size then
-      begin
-        pp "  Variable Pf%in: forall n x y, P [%s%i x] (eval%in (S n) y) (f%in n x y)." i c i i i;
-        pp "  Variable Pfn%i: forall n x y, P (eval%in (S n) x) [%s%i y] (fn%i n x y)." i i c i i;
-      end
-    else
-      begin
-        pp "  Variable Pf%in: forall n x y, Z_of_nat n <= %i -> P [%s%i x] (eval%in (S n) y) (f%in n x y)." i (size - i) c i i i;
-        pp "  Variable Pfn%i: forall n x y, Z_of_nat n <= %i -> P (eval%in (S n) x) [%s%i y] (fn%i n x y)." i (size - i) i c i i;
-      end;
-    pr "";
-  done;
-  pr "  Variable fnn: forall n, word w%i (S n) -> word w%i (S n) -> res." size size;
-  pp "  Variable Pfnn: forall n x y, P [%sn n x] [%sn n y] (fnn n x y)." c c;
-  pr "  Variable fnm: forall n m, word w%i (S n) -> word w%i (S m) -> res." size size;
-  pp "  Variable Pfnm: forall n m x y, P [%sn n x] [%sn m y] (fnm n m x y)." c c;
-  pr "";
+ (** * [iter]
 
-  pr "  (* We iter the smaller argument with the bigger  *)";
-  pr "";
-  pr "  Definition iter (x y: t_): res :=";
-  pr0 "    Eval lazy zeta beta iota delta [";
-  for i = 0 to size do
-    pr0 "extend%i " i;
-  done;
-  pr "";
-  pr "                                         DoubleBase.extend DoubleBase.extend_aux";
-  pr "                                         ] in";
-  pr "  match x, y with";
-  for i = 0 to size do
-    for j = 0 to i - 1 do
-      pr "  | %s%i wx, %s%i wy => fn%i %i wx wy" c i c j j (i - j - 1);
-    done;
-    pr "  | %s%i wx, %s%i wy => f%i wx wy" c i c i i;
-    for j = i + 1 to size do
-      pr "  | %s%i wx, %s%i wy => f%in %i wx wy" c i c j i (j - i - 1);
-    done;
-    if i == size then
-      pr "  | %s%i wx, %sn m wy => f%in m wx wy" c size c size
-    else
-      pr "  | %s%i wx, %sn m wy => f%in m (extend%i %i wx) wy" c i c size i (size - i - 1);
-  done;
-  for i = 0 to size do
-    if i == size then
-      pr "  | %sn n wx, %s%i wy => fn%i n wx wy" c c size size
-    else
-      pr "  | %sn n wx, %s%i wy => fn%i n wx (extend%i %i wy)" c c i size i (size - i - 1);
-  done;
-  pr "  | %sn n wx, %sn m wy => fnm n m wx wy" c c;
-  pr "  end.";
-  pr "";
-  let break_eq0 v =
-    pp "    generalize (ZnZ.spec_eq0 %s); case ZnZ.eq0; intros H." v;
-    pp "      intros; simpl [N0 %s]; rewrite H; trivial." v;
-    pp "    clear H."
-  in
-  pp "  Ltac zg_tac := try";
-  pp "    (red; simpl Zcompare; auto;";
-  pp "     let t := fresh \"H\" in (intros t; discriminate t)).";
-  pp "";
-  pp "  Lemma spec_iter: forall x y, P [x] [y] (iter x y).";
-  pp "  Proof.";
-  pp "  intros x; case x; clear x; unfold iter.";
-  for i = 0 to size do
-    pp "    intros x y; case y; clear y.";
-    for j = 0 to i - 1 do
-      pp "     intros y; rewrite spec_eval%in%i;  apply (Pfn%i %i); zg_tac." j (i - j) j (i - j - 1);
-    done;
-    pp "     intros y; apply Pf%i." i;
-    for j = i + 1 to size do
-      pp "     intros y; rewrite spec_eval%in%i; apply (Pf%in %i); zg_tac." i (j - i) i (j - i - 1);
-    done;
-    if i == size then
-      pp "     intros m y; rewrite spec_eval%in; apply Pf%in." size size
-    else
-      pp "     intros m y; rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pf%in." i size size size;
-  done;
-  pp "    intros n x y; case y; clear y.";
-  for i = 0 to size do
-    if i == size then
-      pp "     intros y; rewrite spec_eval%in; apply Pfn%i." size size
-    else
-      pp "      intros y; rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pfn%i." i size size size;
-  done;
-  pp "  intros m y; apply Pfnm.";
-  pp "  Qed.";
-  pp "";
+     Generic binary operator construction, by splitting the larger
+     argument in blocks and applying the smaller argument to them.
+ *)
 
+ Section Iter.
 
-  pr "  (* We iter the smaller argument with the bigger *)";
-  pr "  (* with special zero functions *)";
-  pr "";
-  pr "  Variable f0t:  t_ -> res.";
-  pp "  Variable Pf0t: forall x, P 0 [x] (f0t x).";
-  pr "  Variable ft0:  t_ -> res.";
-  pp "  Variable Pft0: forall x, P [x] 0 (ft0 x).";
-  pr "";
-  pr "  Definition iter0 (x y: t_): res :=";
-  pr0 "    Eval lazy zeta beta iota delta [";
-  for i = 0 to size do
-    pr0 "extend%i " i;
-  done;
-  pr "";
-  pr "                                         DoubleBase.extend DoubleBase.extend_aux";
-  pr "                                         ] in";
-  pr "  match x with";
-  for i = 0 to size do
-    pr "  | %s%i wx =>" c i;
-    if i == 0 then
-      pr "    if ZnZ.eq0 wx then f0t y else";
-    pr "    match y with";
-    for j = 0 to i - 1 do
-      pr "    | %s%i wy =>" c j;
-      if j == 0 then
-        pr "       if ZnZ.eq0 wy then ft0 x else";
-      pr "       fn%i %i wx wy" j (i - j - 1);
-    done;
-    pr "    | %s%i wy => f%i wx wy" c i i;
-    for j = i + 1 to size do
-      pr "    | %s%i wy => f%in %i wx wy" c j i (j - i - 1);
-    done;
-    if i == size then
-      pr "    | %sn m wy => f%in m wx wy" c size
-    else
-      pr "    | %sn m wy => f%in m (extend%i %i wx) wy" c size i (size - i - 1);
-    pr "    end";
-  done;
-  pr "  | %sn n wx =>" c;
-  pr "    match y with";
-  for i = 0 to size do
-    pr "    | %s%i wy =>" c i;
-    if i == 0 then
-      pr "      if ZnZ.eq0 wy then ft0 x else";
-    if i == size then
-      pr "      fn%i n wx wy" size
-    else
-      pr "      fn%i n wx (extend%i %i wy)" size i (size - i - 1);
-  done;
-  pr "    | %sn m wy => fnm n m wx wy" c;
-  pr "    end";
-  pr "  end.";
-  pr "";
-
-  pp "  Lemma spec_iter0: forall x y, P [x] [y] (iter0 x y).";
-  pp "  Proof.";
-  pp "  intros x; case x; clear x; unfold iter0.";
-  for i = 0 to size do
-    pp "    intros x.";
-    if i == 0 then break_eq0 "x";
-    pp "    intros y; case y; clear y.";
-    for j = 0 to i - 1 do
-      pp "     intros y.";
-      if j == 0 then break_eq0 "y";
-      pp "     rewrite spec_eval%in%i;  apply (Pfn%i %i); zg_tac." j (i - j) j (i - j - 1);
-    done;
-    pp "     intros y; apply Pf%i." i;
-    for j = i + 1 to size do
-      pp "     intros y; rewrite spec_eval%in%i; apply (Pf%in %i); zg_tac." i (j - i) i (j - i - 1);
-    done;
-    if i == size then
-      pp "     intros m y; rewrite spec_eval%in; apply Pf%in." size size
-    else
-      pp "     intros m y; rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pf%in." i size size size;
-  done;
-  pp "    intros n x y; case y; clear y.";
-  for i = 0 to size do
-    pp "    intros y.";
-    if i = 0 then break_eq0 "y";
-    if i == size then
-      pp "     rewrite spec_eval%in; apply Pfn%i." size size
-    else
-      pp "      rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pfn%i." i size size size;
-  done;
-  pp "  intros m y; apply Pfnm.";
-  pp "  Qed.";
-  pp "";
+  Variable res: Type.
+  Variable P: Z -> Z -> res -> Prop.
 
+  Variable f : forall n, dom_t n -> dom_t n -> res.
+  Variable Pf : forall n x y, P (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y).
 
-  pr "  End Iter.";
-  pr "";
+  Variable fd : forall n m, dom_t n -> word (dom_t n) (S m) -> res.
+  Variable fg : forall n m, word (dom_t n) (S m) -> dom_t n -> res.
+  Variable Pfd : forall n m x y, P (ZnZ.to_Z x) (eval n (S m) y) (fd n m x y).
+  Variable Pfg : forall n m x y, P (eval n (S m) x) (ZnZ.to_Z y) (fg n m x y).
 
+  Variable fnm: forall n m, word (dom_t Size) (S n) -> word (dom_t Size) (S m) -> res.
+  Variable Pfnm: forall n m x y, P [Nn n x] [Nn m y] (fnm n m x y).
 
-  pr " (***************************************************************)";
-  pr " (*                                                             *)";
-  pr " (** *                        Reduction                         *)";
-  pr " (*                                                             *)";
-  pr " (***************************************************************)";
-  pr "";
+  Let Pf' :
+   forall n x y u v, u = [mk_t n x] -> v = [mk_t n y] -> P u v (f n x y).
+  Proof.
+  intros. subst. rewrite 2 spec_mk_t. apply Pf.
+  Qed.
 
-  pr " Definition reduce_0 (x:w0) := %s0 x." c;
-  for i = 1 to size do
-   pr " Definition reduce_%i :=" i;
-   pr "  Eval lazy beta iota delta[reduce_n1] in";
-   pr "   reduce_n1 _ _ (N0 ZnZ.zero) (ZnZ.eq0 (Ops:=w%i_op)) %s%i %s%i."
-      (i-1) (if i = 1 then c else "reduce_") (i-1) c i
-  done;
-  pr " Definition reduce_%i :=" (size+1);
-  pr "  Eval lazy beta iota delta[reduce_n1] in";
-  pr "   reduce_n1 _ _ (N0 ZnZ.zero) (ZnZ.eq0 (Ops:=w%i_op)) reduce_%i (%sn 0)."
-    size size c;
+  Let Pfd' : forall n m x y u v, u = [mk_t n x] -> v = eval n (S m) y ->
+   P u v (fd n m x y).
+  Proof.
+  intros. subst. rewrite spec_mk_t. apply Pfd.
+  Qed.
 
-  pr " Definition reduce_n n :=";
-  pr "  Eval lazy beta iota delta[reduce_n] in";
-  pr "   reduce_n _ _ (N0 ZnZ.zero) reduce_%i %sn n." (size + 1) c;
-  pr "";
-
-  pp " Let spec_reduce_0: forall x, [reduce_0 x] = [%s0 x]." c;
-  pp " Proof.";
-  pp " intros x; unfold to_Z, reduce_0.";
-  pp " auto.";
-  pp " Qed.";
-  pp "";
-
-  for i = 1 to size + 1 do
-    if i == size + 1 then
-      pp " Let spec_reduce_%i: forall x, [reduce_%i x] = [%sn 0 x]." i i c
-    else
-      pp " Let spec_reduce_%i: forall x, [reduce_%i x] = [%s%i x]." i i c i;
-    pp " Proof.";
-    pp " intros x; case x; unfold reduce_%i." i;
-    pp " exact ZnZ.spec_0.";
-    pp " intros x1 y1.";
-    pp " generalize (ZnZ.spec_eq0 x1);";
-    pp "   case ZnZ.eq0; intros H1; auto.";
-    if i <> 1 then
-      pp " rewrite spec_reduce_%i." (i - 1);
-    pp " unfold to_Z; rewrite to_Z_%i." i;
-    pp " unfold to_Z in H1; rewrite H1; auto.";
-    pp " Qed.";
-    pp "";
-  done;
-
-  pp " Let spec_reduce_n: forall n x, [reduce_n n x] = [%sn n x]." c;
-  pp " Proof.";
-  pp " intros n; elim n; simpl reduce_n.";
-  pp "   intros x; rewrite <- spec_reduce_%i; auto." (size + 1);
-  pp " intros n1 Hrec x; case x.";
-  pp " unfold to_Z; rewrite make_op_S; auto.";
-  pp " exact ZnZ.spec_0.";
-  pp " intros x1 y1; case x1; auto.";
-  pp " rewrite Hrec.";
-  pp " rewrite spec_extendn0_0; auto.";
-  pp " Qed.";
-  pp "";
+  Let Pfg' : forall n m x y u v, u = eval n (S m) x -> v = [mk_t n y] ->
+   P u v (fg n m x y).
+  Proof.
+  intros. subst. rewrite spec_mk_t. apply Pfg.
+  Qed.
+";
 
-pr " Definition reduce n : dom_t n -> t :=";
-pr "  match n with";
 for i = 0 to size do
-pr "   | %i => reduce_%i" i i;
- done;
-pr "   | %s(S n) => reduce_n n" (if size=0 then "" else "SizePlus ");
-pr "  end%%nat.";
-pr "";
+pr "  Let f%i := f %i." i i
+done;
 
-pr " Lemma spec_reduce : forall n (x:dom_t n), [reduce n x] = ZnZ.to_Z x.";
-pa " Admitted";
-pp " Proof.";
 for i = 0 to size do
-pp "  destruct n. apply spec_reduce_%i." i;
+pr "  Let f%in := fd %i." i i;
+pr "  Let fn%i := fg %i." i i;
 done;
-pp "  apply spec_reduce_n.";
-pp " Qed.";
-pr "";
-
-  pr " (***************************************************************)";
-  pr " (*                                                             *)";
-  pr " (** *                        Comparison                        *)";
-  pr " (*                                                             *)";
-  pr " (***************************************************************)";
-  pr "";
-
-  for i = 0 to size do
-    pr " Definition compare_%i := ZnZ.compare (Ops:=w%i_op)." i i;
-    pr " Definition comparen_%i :=" i;
-    pr "  compare_mn_1 w%i w%i %s compare_%i (compare_%i %s) compare_%i." i i (pz i) i i (pz i) i
-  done;
-  pr "";
-
-  pr " Definition comparenm n m wx wy :=";
-  pr "    let mn := Max.max n m in";
-  pr "    let d := diff n m in";
-  pr "    let op := make_op mn in";
-  pr "    ZnZ.compare";
-  pr "       (castm (diff_r n m) (extend_tr wx (snd d)))";
-  pr "       (castm (diff_l n m) (extend_tr wy (fst d))).";
-  pr "";
-
-  pr " Local Notation compare_folded :=";
-  pr "   (iter _";
-  for i = 0 to size do
-    pr "      compare_%i" i;
-    pr "      (fun n x y => CompOpp (comparen_%i (S n) y x))" i;
-    pr "      (fun n => comparen_%i (S n))" i;
-  done;
-  pr "      comparenm).";
-  pr " Definition compare : t -> t -> comparison :=";
-  pr "  Eval lazy beta delta [iter] in compare_folded.";
-  pr "";
 
-  for i = 0 to size do
-    pp " Let spec_compare_%i: forall x y," i;
-    pp "  compare_%i x y = Zcompare [%s%i x] [%s%i y]." i c i c i;
-    pp " Proof.";
-    pp "  unfold compare_%i, to_Z; exact ZnZ.spec_compare." i;
-    pp " Qed.";
-    pp "";
-
-    pp "  Let spec_comparen_%i:" i;
-    pp "  forall (n : nat) (x : word w%i n) (y : w%i)," i i;
-    pp "   comparen_%i n x y = Zcompare (eval%in n x) [%s%i y]." i i c i;
-    pp "  Proof.";
-    pp "  intros n x y.";
-    pp "  unfold comparen_%i, to_Z; rewrite spec_double_eval%in." i i;
-    pp "  apply spec_compare_mn_1.";
-    pp "  exact ZnZ.spec_0.";
-    pp "  intros x1; exact (ZnZ.spec_compare %s x1)." (pz i);
-    pp "  exact ZnZ.spec_to_Z.";
-    pp "  exact ZnZ.spec_compare.";
-    pp "  exact ZnZ.spec_compare.";
-    pp "  exact ZnZ.spec_to_Z.";
-    pp "  Qed.";
-    pp "";
+pr "  Notation iter_folded := (fun x y => match x, y with";
+for i = 0 to size do
+  for j = 0 to size do
+    pr "  | N%i wx, N%i wy => f%s wx wy" i j
+      (if i = j then string_of_int i
+       else if i < j then string_of_int i ^ "n " ^ string_of_int (j-i-1)
+       else "n" ^ string_of_int j ^ " " ^ string_of_int (i-j-1))
   done;
+  pr "  | N%i wx, Nn m wy => f%in m %s wy" i size (ext i size "wx")
+done;
+for i = 0 to size do
+  pr "  | Nn n wx, N%i wy => fn%i n wx %s" i size (ext i size "wy")
+done;
+pr
+"  | Nn n wx, Nn m wy => fnm n m wx wy
+  end).
+";
 
-  pr " Theorem spec_compare : forall x y,";
-  pr "   compare x y = Zcompare [x] [y].";
-  pa " Admitted.";
-  pp " Proof.";
-  pp "  intros x y. change compare with compare_folded. apply spec_iter; clear x y.";
-  for i = 0 to size - 1 do
-    pp "  exact spec_compare_%i." i;
-    pp "  intros n x y H; rewrite spec_comparen_%i; apply Zcompare_antisym." i;
-    pp "  intros n x y H; exact (spec_comparen_%i (S n) x y)." i;
-  done;
-  pp "  exact spec_compare_%i." size;
-  pp "  intros n x y; rewrite spec_comparen_%i; apply Zcompare_antisym." size;
-  pp "  intros n; exact (spec_comparen_%i (S n))." size;
-  pp "  intros n m x y; unfold comparenm.";
-  pp "  rewrite <- (spec_cast_l n m x); rewrite <- (spec_cast_r n m y).";
-  pp "  unfold to_Z; apply ZnZ.spec_compare.";
-  pp " Qed.";
-  pr "";
+pr
+"  Definition iter := Eval lazy beta iota delta
+   [extend DoubleBase.extend DoubleBase.extend_aux zeron]
+   in iter_folded.
+
+  Lemma spec_iter: forall x y, P [x] [y] (iter x y).
+  Proof.
+  change iter with iter_folded; unfold_lets.
+  destruct x; destruct y; apply Pf' || apply Pfd' || apply Pfg' || apply Pfnm;
+  simpl mk_t;
+  match goal with
+   | |- ?x = ?x => reflexivity
+   | |- [Nn _ _] = _ => apply spec_eval_size
+   | |- context [extend ?n ?m _] => apply (spec_extend n m)
+   | _ => idtac
+  end;
+  unfold to_Z; rewrite <- spec_plus_t'; simpl dom_op; reflexivity.
+  Qed.
+
+  End Iter.
+";
 
-  pr " (***************************************************************)";
-  pr " (*                                                             *)";
-  pr " (** *                        Multiplication                    *)";
-  pr " (*                                                             *)";
-  pr " (***************************************************************)";
-  pr "";
+pr
+"  Definition switch
+  (P:nat->Type)%s
+  (fn:forall n, P n) n :=
+  match n return P n with"
+  (iter_str_gen size (fun i -> Printf.sprintf "(f%i:P %i)" i i));
+for i = 0 to size do pr "   | %i => f%i" i i done;
+pr
+"   | n => fn n
+  end.
+";
 
-  for i = 0 to size do
-    pr " Definition w%i_mul_add :=" i;
-    pr "   Eval lazy beta delta [w_mul_add] in";
-    pr "     @w_mul_add w%i %s ZnZ.succ ZnZ.add_c ZnZ.mul_c." i (pz i)
-  done;
-  pr "";
+pr
+"  Lemma spec_switch : forall P (f:forall n, P n) n,
+   switch P %sf n = f n.
+  Proof.
+  repeat (destruct n; try reflexivity).
+  Qed.
+" (iter_str_gen size (fun i -> Printf.sprintf "(f %i) " i));
 
-  for i = 0 to size do
-    pr " Definition w%i_0W := ZnZ.OW (ops:=w%i_op)." i i
-  done;
-  pr "";
+pr
+"  (** * [iter_sym]
 
-  for i = 0 to size do
-    pr " Definition w%i_WW := ZnZ.WW (ops:=w%i_op)." i i
-  done;
-  pr "";
+    A variant of [iter] for symmetric functions, or pseudo-symmetric
+    functions (when f y x can be deduced from f x y).
+  *)
 
-  for i = 0 to size do
-    pr " Definition w%i_mul_add_n1 :=" i;
-    pr "  @double_mul_add_n1 w%i %s w%i_WW w%i_0W w%i_mul_add."  i (pz i) i i i
-  done;
-  pr "";
+  Section IterSym.
 
-  for i = 0 to size - 1 do
-    pr "  Let to_Z%i n :=" i;
-    pr "  match n return word w%i (S n) -> t_ with" i;
-    for j = 0 to size - i do
-      if (i + j) == size then
-        begin
-          pr "  | %i%s => fun x => %sn 0 x" j "%nat" c;
-          pr "  | %i%s => fun x => %sn 1 x" (j + 1) "%nat" c
-        end
-      else
-        pr "  | %i%s => fun x => %s%i x" j "%nat" c (i + j + 1)
-    done;
-    pr   "  | _   => fun _ => N0 ZnZ.zero";
-    pr "  end.";
-    pr "";
-  done;
+  Variable res: Type.
+  Variable P: Z -> Z -> res -> Prop.
 
+  Variable f : forall n, dom_t n -> dom_t n -> res.
+  Variable Pf : forall n x y, P (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y).
 
-  for i = 0 to size - 1 do
-    pp "Theorem to_Z%i_spec:" i;
-    pp "  forall n x, Z_of_nat n <= %i -> [to_Z%i n x] = ZnZ.to_Z (Ops:=nmake_op _ w%i_op (S n)) x." (size + 1 - i) i i;
-    for j = 1 to size + 2 - i do
-      pp " intros n; case n; clear n.";
-      pp "   unfold to_Z%i." i;
-      pp "   intros x H; rewrite spec_eval%in%i; auto." i j;
-    done;
-    pp " intros n x.";
-    pp " repeat rewrite inj_S; unfold Zsucc; auto with zarith.";
-    pp " Qed.";
-    pp "";
-  done;
+  Variable fg : forall n m, word (dom_t n) (S m) -> dom_t n -> res.
+  Variable Pfg : forall n m x y, P (eval n (S m) x) (ZnZ.to_Z y) (fg n m x y).
 
+  Variable fnm: forall n m, word (dom_t Size) (S n) -> word (dom_t Size) (S m) -> res.
+  Variable Pfnm: forall n m x y, P [Nn n x] [Nn m y] (fnm n m x y).
 
-  for i = 0 to size do
-    pr " Definition w%i_mul n x y :=" i;
-    pr " let (w,r) := w%i_mul_add_n1 (S n) x y %s in" i (pz i);
-    if i == size then
-      begin
-        pr " if ZnZ.eq0 w then %sn n r" c;
-        pr " else %sn (S n) (WW (extend%i n w) r)." c i;
-      end
-    else
-      begin
-        pr " if ZnZ.eq0 w then to_Z%i n r" i;
-        pr " else to_Z%i (S n) (WW (extend%i n w) r)." i i;
-      end;
-    pr "";
-  done;
+  Variable opp: res -> res.
+  Variable Popp : forall u v r, P u v r -> P v u (opp r).
+";
 
-  pr " Definition mulnm n m x y :=";
-  pr "    let mn := Max.max n m in";
-  pr "    let d := diff n m in";
-  pr "    let op := make_op mn in";
-  pr "     reduce_n (S mn) (ZnZ.mul_c";
-  pr "       (castm (diff_r n m) (extend_tr x (snd d)))";
-  pr "       (castm (diff_l n m) (extend_tr y (fst d)))).";
-  pr "";
+for i = 0 to size do
+pr "  Let f%i := f %i." i i
+done;
 
-  pr " Local Notation mul_folded :=";
-  pr "  (iter0 t_";
-  for i = 0 to size do
-    pr "    (fun x y => reduce_%i (ZnZ.mul_c x y))" (i + 1);
-    pr "    (fun n x y => w%i_mul n y x)" i;
-    pr "    w%i_mul" i;
-  done;
-  pr "    mulnm";
-  pr "    (fun _ => N0 ZnZ.zero)";
-  pr "    (fun _ => N0 ZnZ.zero)";
-  pr "  ).";
-  pr " Definition mul : t -> t -> t :=";
-  pr "  Eval lazy beta delta [iter0] in mul_folded.";
-  pr "";
-  for i = 0 to size do
-    pp " Let spec_w%i_mul_add: forall x y z," i;
-    pp "  let (q,r) := w%i_mul_add x y z in" i;
-    pp "  ZnZ.to_Z (Ops:=w%i_op) q * (base (ZnZ.digits w%i_op))  +  ZnZ.to_Z (Ops:=w%i_op) r =" i i i;
-    pp "  ZnZ.to_Z (Ops:=w%i_op) x * ZnZ.to_Z (Ops:=w%i_op) y + ZnZ.to_Z (Ops:=w%i_op) z :=" i i i ;
-    pp "   spec_mul_add.";
-    pp "";
-  done;
+for i = 0 to size do
+pr "  Let fn%i := fg %i." i i;
+done;
 
-  for i = 0 to size do
-    pp " Theorem spec_w%i_mul_add_n1: forall n x y z," i;
-    pp "  let (q,r) := w%i_mul_add_n1 n x y z in" i;
-    pp "  ZnZ.to_Z (Ops:=w%i_op) q * (base (ZnZ.digits (nmake_op _ w%i_op n)))  +" i i;
-    pp "  ZnZ.to_Z (Ops:=nmake_op _ w%i_op n) r =" i;
-    pp "  ZnZ.to_Z (Ops:=nmake_op _ w%i_op n) x * ZnZ.to_Z (Ops:=w%i_op) y +" i i;
-    pp "  ZnZ.to_Z (Ops:=w%i_op) z." i;
-    pp " Proof.";
-    pp " intros n x y z; unfold w%i_mul_add_n1." i;
-    pp " rewrite nmake_double.";
-    pp " rewrite digits_doubled.";
-    pp " change (base (DoubleBase.double_digits (ZnZ.digits w%i_op) n)) with" i;
-    pp "        (DoubleBase.double_wB (ZnZ.digits w%i_op) n)." i;
-    pp " apply spec_double_mul_add_n1; auto.";
-    if i == 0 then pp " exact ZnZ.spec_0.";
-    pp " exact ZnZ.spec_WW.";
-    pp " exact ZnZ.spec_OW.";
-    pp " exact spec_mul_add.";
-    pp " Qed.";
-    pp "";
-  done;
+pr "  Let f' := switch _ %s f." (iter_name 0 size "f" "");
+pr "  Let fg' := switch _ %s fg." (iter_name 0 size "fn" "");
 
-  pp "  Lemma nmake_op_WW: forall ww ww1 n x y,";
-  pp "    ZnZ.to_Z (Ops:=nmake_op ww ww1 (S n)) (WW x y) =";
-  pp "    ZnZ.to_Z (Ops:=nmake_op ww ww1 n) x * base (ZnZ.digits (nmake_op ww ww1 n)) +";
-  pp "    ZnZ.to_Z (Ops:=nmake_op ww ww1 n) y.";
-  pp "  Proof.";
-  pp "    auto.";
-  pp "  Qed.";
-  pp "";
+pr
+"  Local Notation iter_sym_folded :=
+   (iter res f' (fun n m x y => opp (fg' n m y x)) fg' fnm).
 
-  for i = 0 to size do
-    pp "  Lemma extend%in_spec: forall n x1," i;
-    pp "  ZnZ.to_Z (Ops:=nmake_op _ w%i_op (S n)) (extend%i n x1) =" i i;
-    pp "  ZnZ.to_Z (Ops:=w%i_op) x1." i;
-    pp "  Proof.";
-    pp "    intros n1 x2; rewrite nmake_double.";
-    pp "    unfold extend%i." i;
-    pp "    rewrite DoubleBase.spec_extend; auto.";
-    if i == 0 then
-      pp "    intros l; simpl; rewrite ZnZ.spec_0; ring.";
-    pp "  Qed.";
-    pp "";
-  done;
+  Definition iter_sym :=
+   Eval lazy beta zeta iota delta [iter f' fg' switch] in iter_sym_folded.
 
-  pp "  Lemma spec_muln:";
-  pp "    forall n (x: word _ (S n)) y,";
-  pp "     [%sn (S n) (ZnZ.mul_c (Ops:=make_op n) x y)] = [%sn n x] * [%sn n y]." c c c;
-  pp "  Proof.";
-  pp "    intros n x y; unfold to_Z.";
-  pp "    rewrite <- ZnZ.spec_mul_c.";
-  pp "    rewrite make_op_S.";
-  pp "    case ZnZ.mul_c; auto.";
-  pp "  Qed.";
-  pr "";
+  Lemma spec_iter_sym: forall x y, P [x] [y] (iter_sym x y).
+  Proof.
+  intros. change iter_sym with iter_sym_folded. apply spec_iter; clear x y.
+  unfold_lets.
+  intros. rewrite spec_switch. auto.
+  intros. apply Popp. unfold_lets. rewrite spec_switch; auto.
+  intros. unfold_lets. rewrite spec_switch; auto.
+  auto.
+  Qed.
 
-  pr "  Theorem spec_mul: forall x y, [mul x y] = [x] * [y].";
-  pa "  Admitted.";
-  pp "  Proof.";
-  for i = 0 to size do
-    pp "    assert(F%i:" i;
-    pp "    forall n x y,";
-    if i <> size then
-      pp0 "    Z_of_nat n <= %i -> "   (size - i);
-    pp "    [w%i_mul n x y] = eval%in (S n) x * [%s%i y])." i i c i;
-    if i == size then
-      pp "    intros n x y; unfold w%i_mul." i
-    else
-      pp "    intros n x y H; unfold w%i_mul." i;
-    pp "    generalize (spec_w%i_mul_add_n1 (S n) x y %s)." i (pz i);
-    pp "    case w%i_mul_add_n1; intros x1 y1." i;
-    pp "    change (ZnZ.to_Z x) with (eval%in (S n) x)." i;
-    pp "    change (ZnZ.to_Z y) with ([%s%i y])." c i;
-    if i == 0 then
-      pp "    rewrite ZnZ.spec_0; rewrite Zplus_0_r."
-    else
-      pp "    change (ZnZ.to_Z W0) with 0; rewrite Zplus_0_r.";
-    pp "    intros H1; rewrite <- H1; clear H1.";
-    pp "    generalize (ZnZ.spec_eq0 x1); case ZnZ.eq0; intros HH.";
-    pp "    unfold to_Z in HH; rewrite HH by trivial.";
-    if i == size then
-      begin
-        pp "    rewrite spec_eval%in; unfold eval%in, nmake_op%i; auto." i i i;
-        pp "    rewrite spec_eval%in; unfold eval%in, nmake_op%i." i i i
-      end
-    else
-      begin
-        pp "    rewrite to_Z%i_spec; auto with zarith." i;
-        pp "    rewrite to_Z%i_spec; try (rewrite inj_S; auto with zarith)." i
-      end;
-    pp "    rewrite nmake_op_WW; rewrite extend%in_spec; auto." i;
-  done;
-  pp "    intros x y. change mul with mul_folded. apply spec_iter0; clear x y.";
-  for i = 0 to size do
-    pp "    intros x y; rewrite spec_reduce_%i." (i + 1);
-    pp "    unfold to_Z.";
-    pp "    generalize (ZnZ.spec_mul_c x y).";
-    pp "    intros HH; rewrite <- HH; clear HH; auto.";
-    if i == size then
-      begin
-        pp "    intros n x y; rewrite F%i; auto with zarith." i;
-        pp "    intros n x y; rewrite F%i; auto with zarith." i;
-      end
-    else
-      begin
-        pp "    intros n x y H; rewrite F%i; auto with zarith." i;
-        pp "    intros n x y H; rewrite F%i; auto with zarith." i;
-      end;
-  done;
-  pp "    intros n m x y; unfold mulnm.";
-  pp "    rewrite spec_reduce_n.";
-  pp "    rewrite <- (spec_cast_l n m x).";
-  pp "    rewrite <- (spec_cast_r n m y).";
-  pp "    rewrite spec_muln; rewrite spec_cast_l; rewrite spec_cast_r; auto.";
-  pp "    intros x; simpl; rewrite ZnZ.spec_0; ring.";
-  pp "    intros x; simpl; rewrite ZnZ.spec_0; ring.";
-  pp "  Qed.";
-  pr "";
+  End IterSym.
 
-  pr " (***************************************************************)";
-  pr " (*                                                             *)";
-  pr " (** *                        Division                          *)";
-  pr " (*                                                             *)";
-  pr " (***************************************************************)";
-  pr "";
+ (** * Reduction
 
-  pp " Let spec_divn1 ww (ww_op: ZnZ.Ops ww) (ww_spec: ZnZ.Specs ww_op) :=";
-  pp "   (spec_double_divn1";
-  pp "    (ZnZ.zdigits ww_op) ZnZ.zero";
-  pp "    ZnZ.WW ZnZ.head0";
-  pp "    ZnZ.add_mul_div ZnZ.div21";
-  pp "    ZnZ.compare ZnZ.sub ZnZ.to_Z";
-  pp "    ZnZ.spec_to_Z";
-  pp "    ZnZ.spec_zdigits";
-  pp "    ZnZ.spec_0 ZnZ.spec_WW ZnZ.spec_head0";
-  pp "    ZnZ.spec_add_mul_div ZnZ.spec_div21";
-  pp "    ZnZ.spec_compare ZnZ.spec_sub).";
-  pp "";
+     [reduce] can be used instead of [mk_t], it will choose the
+     lowest possible level. NB: We only search and remove leftmost
+     W0's via ZnZ.eq0, any non-W0 block ends the process, even
+     if its value is 0.
+ *)
 
-  for i = 0 to size do
-    pr " Definition w%i_divn1 n x y :="  i;
-    pr "  let (u, v) :=";
-    pr "  double_divn1 (ZnZ.zdigits w%i_op) ZnZ.zero" i;
-    pr "    ZnZ.WW ZnZ.head0";
-    pr "    ZnZ.add_mul_div ZnZ.div21";
-    pr "    ZnZ.compare ZnZ.sub (S n) x y in";
-    if i == size then
-      pr "   (%sn _ u, %s%i v)." c c i
-    else
-      pr "   (to_Z%i _ u, %s%i v)." i c i;
-    pr "";
-  done;
+ (** First, a direct version ... *)
 
-  for i = 0 to size do
-    pp " Lemma spec_get_end%i: forall n x y," i;
-    pp "    eval%in n x  <= [%s%i y] ->" i c i;
-    pp "     [%s%i (DoubleBase.get_low %s n x)] = eval%in n x." c i (pz i) i;
-    pp " Proof.";
-    pp " intros n x y H.";
-    pp " rewrite spec_double_eval%in; unfold to_Z." i;
-    pp " apply DoubleBase.spec_get_low.";
-    pp " exact ZnZ.spec_0.";
-    pp " exact ZnZ.spec_to_Z.";
-    pp " apply Zle_lt_trans with [%s%i y]; auto." c i;
-    pp "   rewrite <- spec_double_eval%in; auto." i;
-    pp " unfold to_Z; case (ZnZ.spec_to_Z y); auto.";
-    pp " Qed.";
-    pp "";
-  done;
+ Fixpoint red_t n : dom_t n -> t :=
+  match n return dom_t n -> t with
+   | O => N0
+   | S n => fun x =>
+     let x' := pred_t n x in
+     reduce_n1 _ _ (N0 zero0) ZnZ.eq0 (red_t n) (mk_t_S n) x'
+  end.
 
-  for i = 0 to size do
-    pr " Let div_gt%i (x y:w%i) := let (u,v) := ZnZ.div_gt x y in (reduce_%i u, reduce_%i v)." i i i i;
-  done;
-  pr "";
+ Lemma spec_red_t : forall n x, [red_t n x] = [mk_t n x].
+ Proof.
+ induction n.
+ reflexivity.
+ intros.
+ simpl red_t. unfold reduce_n1.
+ rewrite <- (succ_pred_t n x) at 2.
+ remember (pred_t n x) as x'.
+ rewrite spec_mk_t, spec_succ_t.
+ destruct x' as [ | xh xl]. simpl. apply ZnZ.spec_0.
+ generalize (ZnZ.spec_eq0 xh); case ZnZ.eq0; intros H.
+ rewrite IHn, spec_mk_t. simpl. rewrite H; auto.
+ apply spec_mk_t_S.
+ Qed.
 
+ (** ... then a specialized one *)
+";
 
-  pr " Let div_gtnm n m wx wy :=";
-  pr "    let mn := Max.max n m in";
-  pr "    let d := diff n m in";
-  pr "    let op := make_op mn in";
-  pr "    let (q, r):= ZnZ.div_gt";
-  pr "         (castm (diff_r n m) (extend_tr wx (snd d)))";
-  pr "         (castm (diff_l n m) (extend_tr wy (fst d))) in";
-  pr "    (reduce_n mn q, reduce_n mn r).";
-  pr "";
+for i = 0 to size do
+pr " Definition eq0%i := @ZnZ.eq0 _ w%i_op." i i;
+done;
 
-  pr " Local Notation div_gt_folded :=";
-  pr "   (iter _";
-  for i = 0 to size do
-    pr "      div_gt%i" i;
-    pr "      (fun n x y => div_gt%i x (DoubleBase.get_low %s (S n) y))" i (pz i);
-    pr "      w%i_divn1" i;
-  done;
-  pr "      div_gtnm).";
-  pr " Definition div_gt := Eval lazy beta delta [iter] in div_gt_folded.";
-  pr "";
+pr "
+ Definition reduce_0 := N0.";
+for i = 1 to size do
+  pr " Definition reduce_%i :=" i;
+  pr "  Eval lazy beta iota delta [reduce_n1] in";
+  pr "   reduce_n1 _ _ (N0 zero0) eq0%i reduce_%i N%i." (i-1) (i-1) i
+done;
 
-  pr " Theorem spec_div_gt: forall x y,";
-  pr "       [x] > [y] -> 0 < [y] ->";
-  pr "      let (q,r) := div_gt x y in";
-  pr "      [q] = [x] / [y] /\\ [r] = [x] mod [y].";
-  pa " Admitted.";
-  pp " Proof.";
-  pp " assert (FO:";
-  pp "   forall x y, [x] > [y] -> 0 < [y] ->";
-  pp "      let (q,r) := div_gt x y in";
-  pp "      [x] = [q] * [y] + [r] /\\ 0 <= [r] < [y]).";
-  pp "   intros x y. change div_gt with div_gt_folded. apply spec_iter; clear x y.";
-  for i = 0 to size do
-    pp "   (* %i *)" i;
-    pp "   intros x y H1 H2; unfold div_gt%i." i;
-    pp "    generalize (ZnZ.spec_div_gt x y H1 H2); case ZnZ.div_gt.";
-    pp "    intros xx yy; repeat rewrite spec_reduce_%i; auto." i;
-    if i == size then
-     pp "   intros n x y H2 H3; unfold div_gt%i." i
-    else
-     pp "   intros n x y H1 H2 H3; unfold div_gt%i." i;
-    pp "    generalize (ZnZ.spec_div_gt x";
-    pp "                (DoubleBase.get_low %s (S n) y))." (pz i);
-    pp "    case ZnZ.div_gt.";
-    pp "    intros xx yy H4; repeat rewrite spec_reduce_%i." i;
-    pp "    generalize (spec_get_end%i (S n) y x); unfold to_Z; intros H5." i;
-    pp "    unfold to_Z in H2; rewrite H5 in H4; auto with zarith.";
-    if i == size then
-     pp "   intros n x y H2 H3."
-    else
-     pp "   intros n x y H1 H2 H3.";
-    pp "    generalize";
-    pp "     (spec_divn1 w%i w%i_op w%i_spec (S n) x y H3)." i i i;
-    pp "    unfold w%i_divn1; case double_divn1." i;
-    pp "    intros xx yy H4.";
-    if i == size then
-      begin
-        pp "    repeat rewrite <- spec_double_eval%in in H4; auto." i;
-        pp "    rewrite spec_eval%in; auto." i;
-      end
-    else
-      begin
-        pp "    rewrite to_Z%i_spec; auto with zarith." i;
-        pp "    repeat rewrite <- spec_double_eval%in in H4; auto." i;
-      end;
-  done;
-  pp "    intros n m x y H1 H2; unfold div_gtnm.";
-  pp "    generalize (ZnZ.spec_div_gt";
-  pp "                   (castm (diff_r n m)";
-  pp "                     (extend_tr x (snd (diff n m))))";
-  pp "                   (castm (diff_l n m)";
-  pp "                     (extend_tr y (fst (diff n m))))).";
-  pp "    case ZnZ.div_gt.";
-  pp "    intros xx yy HH.";
-  pp "    repeat rewrite spec_reduce_n.";
-  pp "    rewrite <- (spec_cast_l n m x).";
-  pp "    rewrite <- (spec_cast_r n m y).";
-  pp "    unfold to_Z; apply HH.";
-  pp "    rewrite <- (spec_cast_l n m x) in H1; auto.";
-  pp "    rewrite <- (spec_cast_r n m y) in H1; auto.";
-  pp "    rewrite <- (spec_cast_r n m y) in H2; auto.";
-  pp "  intros x y H1 H2; generalize (FO x y H1 H2); case div_gt.";
-  pp "  intros q r (H3, H4); split.";
-  pp "  apply (Zdiv_unique [x] [y] [q] [r]); auto.";
-  pp "  rewrite Zmult_comm; auto.";
-  pp "  apply (Zmod_unique [x] [y] [q] [r]); auto.";
-  pp "  rewrite Zmult_comm; auto.";
-  pp "  Qed.";
-  pr "";
+  pr " Definition reduce_%i :=" (size+1);
+  pr "  Eval lazy beta iota delta [reduce_n1] in";
+  pr "   reduce_n1 _ _ (N0 zero0) eq0%i reduce_%i (Nn 0)." size size;
 
-  pr " (***************************************************************)";
-  pr " (*                                                             *)";
-  pr " (** *                        Modulo                            *)";
-  pr " (*                                                             *)";
-  pr " (***************************************************************)";
+  pr " Definition reduce_n n :=";
+  pr "  Eval lazy beta iota delta [reduce_n] in";
+  pr "   reduce_n _ _ (N0 zero0) reduce_%i Nn n." (size + 1);
   pr "";
 
-  for i = 0 to size do
-    pr " Definition w%i_modn1 :=" i;
-    pr "  double_modn1 (ZnZ.zdigits w%i_op) (ZnZ.zero (Ops:=w%i_op))" i i;
-    pr "    ZnZ.head0 ZnZ.add_mul_div ZnZ.div21";
-    pr "    ZnZ.compare ZnZ.sub.";
-  done;
-  pr "";
+pr " Definition reduce n : dom_t n -> t :=";
+pr "  match n with";
+for i = 0 to size do
+pr "   | %i => reduce_%i" i i;
+done;
+pr "   | %s(S n) => reduce_n n" (if size=0 then "" else "SizePlus ");
+pr "  end.";
+pr "";
 
-  pr " Let mod_gtnm n m wx wy :=";
-  pr "    let mn := Max.max n m in";
-  pr "    let d := diff n m in";
-  pr "    let op := make_op mn in";
-  pr "    reduce_n mn (ZnZ.modulo_gt";
-  pr "         (castm (diff_r n m) (extend_tr wx (snd d)))";
-  pr "         (castm (diff_l n m) (extend_tr wy (fst d)))).";
-  pr "";
+pr " Ltac unfold_red := unfold reduce, %s." (iter_name 1 size "reduce_" ",");
 
-  pr " Local Notation mod_gt_folded :=";
-  pr "   (iter _";
-  for i = 0 to size do
-    pr "      (fun x y => reduce_%i (ZnZ.modulo_gt x y))" i;
-    pr "      (fun n x y => reduce_%i (ZnZ.modulo_gt x (DoubleBase.get_low %s (S n) y)))" i (pz i);
-    pr "      (fun n x y => reduce_%i (w%i_modn1 (S n) x y))" i i;
-  done;
-  pr "      mod_gtnm).";
-  pr " Definition mod_gt := Eval lazy beta delta[iter] in mod_gt_folded.";
-  pr "";
+pr "
+ Ltac solve_red :=
+ let H := fresh in let G := fresh in
+ match goal with
+  | |- ?P (S ?n) => assert (H:P n) by solve_red
+  | _ => idtac
+ end;
+ intros n G x; destruct (le_lt_eq_dec _ _ G) as [LT|EQ];
+ solve [
+  apply (H _ (lt_n_Sm_le _ _ LT)) |
+  inversion LT |
+  subst; change (reduce 0 x = red_t 0 x); reflexivity |
+  specialize (H (pred n)); subst; destruct x;
+   [|unfold_red; rewrite H; auto]; reflexivity
+ ].
+
+ Lemma reduce_equiv : forall n x, n <= Size -> reduce n x = red_t n x.
+ Proof.
+ set (P N := forall n, n <= N -> forall x, reduce n x = red_t n x).
+ intros n x H. revert n H x. change (P Size). solve_red.
+ Qed.
 
-  pp " Let spec_modn1 ww (ww_op: ZnZ.Ops ww) (ww_spec: ZnZ.Specs ww_op) :=";
-  pp "   spec_double_modn1";
-  pp "    (ZnZ.zdigits ww_op) ZnZ.zero";
-  pp "    ZnZ.WW ZnZ.head0";
-  pp "    ZnZ.add_mul_div ZnZ.div21";
-  pp "    ZnZ.compare ZnZ.sub ZnZ.to_Z";
-  pp "    ZnZ.spec_to_Z";
-  pp "    ZnZ.spec_zdigits";
-  pp "    ZnZ.spec_0 ZnZ.spec_WW ZnZ.spec_head0";
-  pp "    ZnZ.spec_add_mul_div ZnZ.spec_div21";
-  pp "    ZnZ.spec_compare ZnZ.spec_sub.";
-  pp "";
-
-  pr " Theorem spec_mod_gt:";
-  pr "   forall x y, [x] > [y] -> 0 < [y] -> [mod_gt x y] = [x] mod [y].";
-  pa " Admitted.";
-  pp " Proof.";
-  pp " intros x y. change mod_gt with mod_gt_folded. apply spec_iter; clear x y.";
-  for i = 0 to size do
-    pp " intros x y H1 H2; rewrite spec_reduce_%i." i;
-    pp "   exact (ZnZ.spec_modulo_gt x y H1 H2).";
-    if i == size then
-      pp " intros n x y H2 H3; rewrite spec_reduce_%i." i
-    else
-      pp " intros n x y H1 H2 H3; rewrite spec_reduce_%i." i;
-    pp " rewrite <- (spec_get_end%i (S n) y x); auto with zarith." i;
-    pp " unfold to_Z; apply ZnZ.spec_modulo_gt; auto.";
-    pp " rewrite <- (spec_get_end%i (S n) y x) in H2; auto with zarith." i;
-    pp " rewrite <- (spec_get_end%i (S n) y x) in H3; auto with zarith." i;
-    if i == size then
-      pp " intros n x y H2 H3; rewrite spec_reduce_%i." i
-    else
-      pp " intros n x y H1 H2 H3; rewrite spec_reduce_%i." i;
-    pp " unfold w%i_modn1, to_Z; rewrite spec_double_eval%in." i i;
-    pp " apply (spec_modn1 _ _ w%i_spec); auto." i;
-  done;
-  pp " intros n m x y H1 H2; unfold mod_gtnm.";
-  pp "    repeat rewrite spec_reduce_n.";
-  pp "    rewrite <- (spec_cast_l n m x).";
-  pp "    rewrite <- (spec_cast_r n m y).";
-  pp "    unfold to_Z; apply ZnZ.spec_modulo_gt.";
-  pp "    rewrite <- (spec_cast_l n m x) in H1; auto.";
-  pp "    rewrite <- (spec_cast_r n m y) in H1; auto.";
-  pp "    rewrite <- (spec_cast_r n m y) in H2; auto.";
-  pp " Qed.";
-  pr "";
+ Lemma spec_reduce_n : forall n x, [reduce_n n x] = [Nn n x].
+ Proof.
+ assert (H : forall x, reduce_%i x = red_t (SizePlus 1) x).
+  destruct x; [|unfold reduce_%i; rewrite (reduce_equiv Size)]; auto.
+ induction n.
+   intros. rewrite H. apply spec_red_t.
+ destruct x as [|xh xl].
+ simpl. rewrite make_op_S. exact ZnZ.spec_0.
+ fold word in *.
+ destruct xh; auto.
+ simpl reduce_n.
+ rewrite IHn.
+ rewrite spec_extend_WW; auto.
+ Qed.
+" (size+1) (size+1);
 
-  pr "End Make.";
-  pr "";
+pr
+" Lemma spec_reduce : forall n x, [reduce n x] = ZnZ.to_Z x.
+ Proof.
+ do_size (destruct n;
+       [intros; rewrite reduce_equiv;[apply spec_red_t|auto with arith]|]).
+ apply spec_reduce_n.
+ Qed.
 
+End Make.
+";
diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index 5eb317c682..56dd9c8c56 100644
--- a/theories/Numbers/Natural/BigN/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.v
@@ -480,13 +480,35 @@ End AddS.
 
  End SimplOp.
 
+(** TODO : to migrate in NArith *)
+
+ Notation Pshiftl := DoubleBase.double_digits.
+
+ Lemma Pshiftl_plus : forall n m p,
+  Pshiftl p (m + n) = Pshiftl (Pshiftl p n) m.
+ Proof.
+ induction m; simpl; congruence.
+ Qed.
+
+ Lemma Pshiftl_Zpower : forall n d,
+  Zpos (Pshiftl d n) = (Zpos d * 2 ^ Z_of_nat n)%Z.
+ Proof.
+ intros.
+ rewrite Zmult_comm.
+ induction n. simpl; auto.
+ transitivity (2 * (2 ^ Z_of_nat n * Zpos d))%Z.
+ rewrite <- IHn. auto.
+ rewrite Zmult_assoc.
+ rewrite <- Zpower_Zsucc, inj_S; auto with zarith.
+ Qed.
+
+(** END TODO *)
 
 (** Abstract vision of a datatype of arbitrary-large numbers.
     Concrete operations can be derived from these generic
     fonctions, in particular from [iter_t] and [same_level].
 *)
 
-
 Module Type NAbstract.
 
 (** The domains: a sequence of [Z/nZ] structures *)
@@ -496,7 +518,7 @@ Declare Instance dom_op n : ZnZ.Ops (dom_t n).
 Declare Instance dom_spec n : ZnZ.Specs (dom_op n).
 
 Axiom digits_dom_op : forall n,
-  Zpos (ZnZ.digits (dom_op n)) = Zpos (ZnZ.digits (dom_op 0)) * 2 ^ Z_of_nat n.
+  ZnZ.digits (dom_op n) = Pshiftl (ZnZ.digits (dom_op 0)) n.
 
 (** The type [t] of arbitrary-large numbers, with abstract constructor [mk_t]
     and destructor [destr_t] and iterator [iter_t] *)
@@ -554,22 +576,4 @@ Axiom spec_mk_t_S : forall n (x:zn2z (dom_t n)),
 
 Axiom mk_t_S_level : forall n x, level (mk_t_S n x) = S n.
 
-(** Not generalized yet : *)
-
-Parameter compare : t -> t -> comparison.
-Axiom spec_compare : forall x y, compare x y = Zcompare [x] [y].
-
-Parameter mul : t -> t -> t.
-Axiom spec_mul : forall x y, [mul x y] = [x] * [y].
-
-Parameter div_gt : t -> t -> t*t.
-Axiom spec_div_gt: forall x y,
-       [x] > [y] -> 0 < [y] ->
-      let (q,r) := div_gt x y in
-      [q] = [x] / [y] /\ [r] = [x] mod [y].
-
-Parameter mod_gt : t -> t -> t.
-Axiom spec_mod_gt :
- forall x y, [x] > [y] -> 0 < [y] -> [mod_gt x y] = [x] mod [y].
-
 End NAbstract.