Import coqprime; use it to prove Euler's criterion.

6 files changed, 4788 insertions, 0 deletions

diff --git a/coqprime/num/Lucas.v b/coqprime/num/Lucas.v
new file mode 100644
index 000000000..f969dc106
--- /dev/null
+++ b/coqprime/num/Lucas.v
@@ -0,0 +1,213 @@
+
+(*************************************************************)
+(*      This file is distributed under the terms of the      *)
+(*      GNU Lesser General Public License Version 2.1        *)
+(*************************************************************)
+(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
+(*************************************************************)
+
+Set Implicit Arguments.
+
+Require Import ZArith Znumtheory Zpow_facts.
+Require Import CyclicAxioms DoubleCyclic BigN Cyclic31 Int31.
+Require Import ZCAux.
+Require Import W.
+Require Import Mod_op.
+Require Import LucasLehmer.
+Require Import Bits.
+Import CyclicAxioms DoubleType DoubleBase.
+
+Open Scope Z_scope. 
+
+Section test.
+
+Variable w: Type.
+Variable w_op: ZnZ.Ops w.
+Variable op_spec: ZnZ.Specs w_op.
+Variable p: positive.
+Variable b: w.
+
+Notation "[| x |]" :=
+   (ZnZ.to_Z x)  (at level 0, x at level 99).
+
+
+Hypothesis p_more_1: 2 < Zpos p.
+Hypothesis b_p: [|b|] = 2 ^ Zpos p - 1.
+
+Lemma b_pos: 0 < [|b|].
+rewrite b_p; auto with zarith.
+assert (2 ^ 0 < 2 ^ Zpos p); auto with zarith.
+apply Zpower_lt_monotone; auto with zarith.
+rewrite Zpower_0_r in H; auto with zarith.
+Qed.
+
+Hint Resolve b_pos.
+
+Variable m_op: mod_op w.
+Variable m_op_spec: mod_spec w_op b m_op.
+
+Let w2 := m_op.(add_mod) ZnZ.one ZnZ.one.
+
+Lemma w1_b: [|ZnZ.one|] = 1 mod [|b|].
+rewrite ZnZ.spec_1; simpl; auto.
+rewrite Zmod_small; auto with zarith.
+split; auto with zarith.
+rewrite b_p.
+assert (2 ^ 1 < 2 ^ Zpos p); auto with zarith.
+apply Zpower_lt_monotone; auto with zarith.
+rewrite Zpower_1_r in H; auto with zarith.
+Qed.
+
+Lemma w2_b: [|w2|] = 2 mod [|b|].
+unfold w2; rewrite (add_mod_spec m_op_spec _ _ _ _ w1_b w1_b).
+rewrite w1_b; rewrite <- Zplus_mod; auto with zarith.
+Qed.
+
+Let w4 := m_op.(add_mod) w2 w2.
+
+Lemma w4_b: [|w4|] = 4 mod [|b|].
+unfold w4; rewrite (add_mod_spec m_op_spec _ _ _ _ w2_b w2_b).
+rewrite w2_b; rewrite <- Zplus_mod; auto with zarith.
+Qed.
+
+Let square_m2 :=
+   let square := m_op.(square_mod) in
+   let sub := m_op.(sub_mod) in
+   fun x => sub (square x) w2.
+
+Definition lucastest :=
+ ZnZ.to_Z (iter_pos (Pminus p 2) _ square_m2 w4).
+
+Theorem lucastest_aux_correct:
+ forall p1 z n, 0 <= n -> [|z|] = fst (s n) mod (2 ^ Zpos p - 1) ->
+       [|iter_pos p1 _ square_m2 z|] = fst (s (n + Zpos p1)) mod (2 ^ Zpos p - 1).
+intros p1; pattern p1; apply Pind; simpl iter_pos; simpl s; clear p1.
+intros z p1 Hp1 H.
+unfold square_m2.
+rewrite <- b_p in H.
+generalize (square_mod_spec m_op_spec _ _ H); intros H1.
+rewrite (sub_mod_spec m_op_spec _ _ _ _ H1 w2_b).
+rewrite H1; rewrite w2_b; auto with zarith.
+rewrite H; rewrite <- Zmult_mod; auto with zarith.
+rewrite <- Zminus_mod; auto with zarith.
+rewrite sn; simpl; auto with zarith.
+rewrite b_p; auto.
+intros p1 Rec w1 z Hz Hw1.
+rewrite Pplus_one_succ_l; rewrite iter_pos_plus;
+ simpl iter_pos.
+match goal with |- context[square_m2 ?X] =>
+  set (tmp := X); unfold square_m2; unfold tmp; clear tmp
+end.
+generalize (Rec _ _ Hz Hw1); intros H1.
+rewrite <- b_p in H1.
+generalize (square_mod_spec m_op_spec _ _ H1); intros H2.
+rewrite (sub_mod_spec m_op_spec _ _ _ _ H2 w2_b).
+rewrite H2; rewrite w2_b; auto with zarith.
+rewrite H1; rewrite <- Zmult_mod; auto with zarith.
+rewrite <- Zminus_mod; auto with zarith.
+replace (z + Zpos (1 + p1)) with ((z + Zpos p1) + 1); auto with zarith.
+rewrite sn; simpl fst; try rewrite b_p; auto with zarith.
+rewrite Zpos_plus_distr; auto with zarith.
+Qed.
+
+Theorem lucastest_prop: lucastest = fst(s (Zpos p -2)) mod (2 ^ Zpos p - 1).
+unfold lucastest.
+assert (F: 0 <= 0); auto with zarith.
+generalize (lucastest_aux_correct (p -2) w4 F); simpl Zplus;
+   rewrite Zpos_minus; auto with zarith.
+rewrite Zmax_right; auto with zarith.
+intros tmp; apply tmp; clear tmp.
+rewrite <- b_p; simpl; exact w4_b.
+Qed.
+
+Theorem lucastest_prop_cor: lucastest = 0 -> (2 ^ Zpos p - 1 | fst(s (Zpos p - 2)))%Z.
+intros H.
+apply Zmod_divide.
+assert (H1: 2 ^ 1 < 2 ^ Zpos p); auto with zarith.
+apply Zpower_lt_monotone; auto with zarith.
+rewrite Zpower_1_r in H1; auto with zarith.
+apply trans_equal with (2:= H); apply sym_equal; apply lucastest_prop; auto.
+Qed.
+
+Theorem lucastest_prime:  lucastest = 0 -> prime (2 ^ Zpos p - 1).
+intros H1; case (prime_dec (2 ^ Zpos p - 1)); auto; intros H2.
+case Zdivide_div_prime_le_square with (2 := H2).
+assert (H3: 2 ^ 1 < 2 ^ Zpos p); auto with zarith.
+apply Zpower_lt_monotone; auto with zarith.
+rewrite Zpower_1_r in H3; auto with zarith.
+intros q (H3, (H4, H5)).
+contradict H5; apply Zlt_not_le.
+generalize q_more_than_square; unfold Mp; intros tmp; apply tmp;
+  auto; clear tmp.
+apply lucastest_prop_cor; auto.
+case (Zle_lt_or_eq 2 q); auto.
+apply prime_ge_2; auto.
+intros H5; subst.
+absurd (2 <= 1); auto with arith.
+apply Zdivide_le; auto with zarith.
+case H4; intros x Hx.
+exists (2 ^ (Zpos p -1) - x).
+rewrite Zmult_minus_distr_r; rewrite <- Hx; unfold Mp.
+pattern 2 at 2; rewrite <- Zpower_1_r; rewrite <- Zpower_exp; auto with zarith.
+replace (Zpos p - 1 + 1) with (Zpos p); auto with zarith.
+Qed.
+
+End test.
+
+Definition znz_of_Z (w: Type) (op: ZnZ.Ops w) z :=
+ match z with
+ | Zpos p => snd (ZnZ.of_pos p)
+ | _ => ZnZ.zero
+ end.
+
+Definition lucas p :=
+ let op := cmk_op (Peano.pred (nat_of_P (get_height 31 p))) in
+ let b := znz_of_Z op (Zpower 2 (Zpos p) - 1) in
+ let zp := znz_of_Z op (Zpos p) in
+ let mod_op := mmake_mod_op op b zp in
+  lucastest op p mod_op.
+
+Theorem lucas_prime:
+ forall p, 2 < Zpos p -> lucas p = 0 -> prime (2 ^ Zpos p - 1).
+unfold lucas; intros p Hp H.
+match type of H with lucastest (cmk_op ?x) ?y ?z = _ =>
+   set (w_op := (cmk_op x)); assert(A1: ZnZ.Specs w_op)
+end.
+unfold w_op; apply cmk_spec.
+assert (F0: Zpos p <= Zpos (ZnZ.digits w_op)).
+unfold w_op, base; rewrite (cmk_op_digits (Peano.pred (nat_of_P (get_height 31 p)))).
+generalize (get_height_correct 31 p).
+replace (Z_of_nat (Peano.pred (nat_of_P (get_height 31 p)))) with
+       ((Zpos (get_height 31 p) - 1) ); auto with zarith.
+rewrite pred_of_minus; rewrite inj_minus1; auto with zarith.
+rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto with zarith.
+generalize (lt_O_nat_of_P (get_height 31 p)); auto with zarith.
+assert (F1: ZnZ.to_Z (znz_of_Z w_op (2 ^ (Zpos p) - 1)) = 2 ^ (Zpos p) - 1).
+assert (F1: 0 < 2 ^ (Zpos p) - 1).
+assert (F2: 2 ^ 0 < 2 ^ (Zpos p)); auto with zarith.
+apply Zpower_lt_monotone; auto with zarith.
+rewrite Zpower_0_r in F2; auto with zarith.
+case_eq (2 ^ (Zpos p) - 1); simpl ZnZ.to_Z.
+intros HH; contradict F1; rewrite HH; auto with zarith.
+2: intros p1 HH; contradict F1; rewrite HH; 
+  apply Zle_not_lt; red; simpl; intros; discriminate.
+intros p1 Hp1; apply ZnZ.of_pos_correct; auto.
+rewrite <- Hp1.
+unfold base.
+apply Zlt_le_trans with (2 ^ (Zpos p)); auto with zarith.
+apply Zpower_le_monotone; auto with zarith.
+match type of H with lucastest (cmk_op ?x) ?y ?z = _ =>
+  apply  
+  (@lucastest_prime _ _ (cmk_spec x) p (znz_of_Z w_op (2 ^ Zpos p  -1)) Hp F1 z)
+end; auto with zarith; fold w_op.
+eapply mmake_mod_spec with (p := p); auto with zarith.
+unfold znz_of_Z; unfold znz_of_Z in F1; rewrite F1.
+assert (F2: 2 ^ 1 < 2 ^ (Zpos p)); auto with zarith.
+apply Zpower_lt_monotone; auto with zarith.
+rewrite Zpower_1_r in F2; auto with zarith.
+rewrite ZnZ.of_Z_correct; auto with zarith.
+split; auto with zarith.
+apply Zle_lt_trans with (1 := F0); auto with zarith.
+unfold base; apply Zpower2_lt_lin; auto with zarith.
+Qed.
+
diff --git a/coqprime/num/MEll.v b/coqprime/num/MEll.v
new file mode 100644
index 000000000..afcdf4146
--- /dev/null
+++ b/coqprime/num/MEll.v
@@ -0,0 +1,1228 @@
+
+(*************************************************************)
+(*      This file is distributed under the terms of the      *)
+(*      GNU Lesser General Public License Version 2.1        *)
+(*************************************************************)
+(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
+(*************************************************************)
+
+
+Require Import ZArith Znumtheory Zpow_facts.
+Require Import Int31 ZEll montgomery.
+
+Set Implicit Arguments.
+
+Open Scope Z_scope.
+
+
+Record ex: Set := mkEx {
+  vN : positive;
+  vS : positive;
+  vR:  List.list (positive * positive);
+  vA:  Z;
+  vB:  Z;
+  vx:  Z;
+  vy:  Z
+}.
+
+Coercion Local Zpos : positive >-> Z.
+
+Record ex_spec (exx: ex): Prop := mkExS {
+  n2_div: ~(2 | exx.(vN));
+  n_pos: 2 < exx.(vN);
+ lprime: 
+  forall p : positive * positive, List.In p (vR exx) -> prime (fst p);
+   lbig:
+    4 * vN exx < (Zmullp (vR exx) - 1) ^ 2;
+   inC:
+    vy exx ^ 2 mod vN exx = (vx exx ^ 3 + vA exx * vx exx + vB exx) mod vN exx
+}.
+
+(*
+Let is_even m := 
+Fixpoint invM_aux (n : nat) (m v: int31) : int31 :=
+  match n with 0%nat => 0%int31 | S n =>
+    if (iszero (Cyclic31.nshiftl 30 m)) then
+      lsl (invM_aux n (lsr m 1) v) 1
+    else (1 lor (lsl (invM_aux n (lsr (m - v) 1) v) 1))
+  end.
+
+Definition invM := invM_aux 31.
+
+Lemma invM_spec m v : 
+  is_even v = false -> (v * (invM m v) = m)%int31.
+Proof. admit. Qed.
+
+Inductive melt: Type :=
+  mzero | mtriple: number -> number -> number  -> melt.
+
+(* Montgomery version *)
+Section MEll.
+
+Variable add_mod sub_mod mult_mod : number -> number -> number.
+
+Notation "x ++ y " := (add_mod x y).
+Notation "x -- y" := (sub_mod x y) (at level 50, left associativity).
+Notation "x ** y" := 
+  (mult_mod x y) (at level 40, left associativity).
+Notation "x ?= y" := (eq_num x y).
+
+Variable A c0 c2 c3 : number.
+
+Definition mdouble : number -> melt -> (melt * number):= 
+  fun (sc: number) (p1: melt) =>
+ match p1 with
+  mzero => (p1, sc)
+ | (mtriple x1 y1 z1) =>
+    if (y1 ?= c0) then (mzero, z1 ** sc) else
+     (* we do 2p *)
+    let m' := c3 ** x1 ** x1 ++ A ** z1 ** z1 in
+    let l' := c2 ** y1 ** z1 in
+    let m'2 := m' ** m' in
+    let l'2 := l' ** l' in
+    let l'3 := l'2 ** l' in
+    let x3 := m'2 ** z1 -- c2 ** x1 ** l'2 in
+    (mtriple
+          (l' ** x3)
+          (l'2 ** (m' ** x1 -- y1 ** l') -- m' ** x3)
+          (z1 ** l'3), sc)
+  end.
+
+Definition madd := fun (sc : number) (p1 p2 : melt) =>
+ match p1, p2 with
+  mzero, _ => (p2, sc)
+ | _ , mzero => (p1, sc)
+ | (mtriple x1 y1 z1), (mtriple x2 y2 z2) =>
+  let d1 := x2 ** z1 in
+  let d2 := x1 ** z2 in
+  let l := d1 -- d2 in
+  let dl := d1 ++ d2 in
+  let m := y2 ** z1 -- y1 ** z2 in
+  if (l ?= c0) then
+   (* we have p1 = p2 o p1 = -p2 *)
+   if (m ?= c0) then
+    if (y1 ?= c0) then (mzero, z1 ** z2 ** sc) else
+     (* we do 2p *)
+    let m' := c3 ** x1 ** x1 ++ A ** z1 ** z1 in
+    let l' := c2 ** y1 ** z1 in
+    let m'2 := m' ** m' in
+    let l'2 := l' ** l' in
+    let l'3 := l'2 ** l' in
+    let x3 := m'2 ** z1 -- c2 ** x1 ** l'2 in
+    (mtriple
+          (l' ** x3)
+          (l'2 ** (m' ** x1 -- y1 ** l') -- m' ** x3)
+          (z1 ** l'3), z2 ** sc)
+    else (* p - p *)  (mzero, m ** z1 ** z2 ** sc)
+  else
+     let l2 := l ** l in
+     let l3 := l2 ** l in
+     let m2 := m ** m in
+     let x3 := z1 ** z2 ** m2 -- l2 ** dl in
+      (mtriple (l ** x3)
+             (z2 ** l2 ** (m ** x1 -- y1 ** l) -- m ** x3)
+             (z1 ** z2 ** l3), sc)
+  end.
+
+Definition mopp p := 
+  match p with mzero => p | (mtriple x1 y1 z1) => (mtriple x1 (c0 -- y1) z1) end.
+
+End MEll.
+
+*)
+
+(* 
+
+Section Scal.
+
+Variable mdouble : number -> melt -> melt * number.
+Variable madd : number -> melt -> melt -> melt * number.
+Variable mopp : melt -> melt.
+
+
+Fixpoint scalb (sc: number) (b:bool) (a: melt) (p: positive) {struct p}:
+ melt * number :=
+ match p with
+   xH => if b then mdouble sc a else (a,sc)
+ | xO p1 => let (a1, sc1) := scalb sc false a p1 in
+              if b then 
+                let (a2, sc2) := mdouble sc1 a1 in
+                madd sc2 a a2
+              else mdouble sc1 a1
+ | xI p1 => let (a1, sc1) := scalb sc true a p1 in
+              if b then  mdouble sc1 a1
+              else
+              let (a2, sc2) := mdouble sc1 a1 in 
+              madd sc2 (mopp a) a2
+ end.
+
+Definition scal sc a p := scalb sc false a p.
+
+Definition scal_list sc a l :=
+  List.fold_left 
+  (fun (asc: melt * number) p1 => let (a,sc) := asc in scal sc a p1) l (a,sc).
+
+Variable mult_mod : number -> number -> number.
+Notation "x ** y" := 
+  (mult_mod x y) (at level 40, left associativity).
+
+Variable c0 : number.
+
+Fixpoint scalL (sc : number) (a: melt) (l: List.list positive) {struct l} : 
+    (melt * number) :=
+   match l with
+     List.nil => (a,sc)
+   | List.cons n l1 =>
+        let (a1, sc1) := scal sc a n in
+        let (a2, sc2) := scal_list sc1 a l1 in
+          match a2 with
+             mzero => (mzero, c0)
+          |  mtriple _ _ z => scalL (sc2 ** z) a1 l1
+          end
+   end.
+
+End Scal.
+
+Definition isM2 p := 
+  match p with
+    xH   => false
+|    xO _ => false
+|     _ => true
+end.
+
+Definition ell_test (N S: positive) (l: List.list (positive * positive))
+                      (A B x y: Z) :=
+    if isM2 N then
+    match (4 * N) ?= (ZEll.Zmullp l - 1) ^ 2  with
+      Lt => 
+       match y ^ 2 mod N ?= (x ^ 3 + A * x + B) mod N with
+       Eq => 
+          let M := positive_to_num N in
+          let m' := invM (0 - 1) (nhead M) in
+          let n := length M in
+          let e := encode M m' n in
+          let d := decode M m' n in
+          let add_mod := add_mod M in
+          let sub_mod := sub_mod M in
+          let mult_mod := reduce_mult_num M m' n in
+          let mA := e A in
+          let mB := e B in
+          let c0 := e 0 in
+          let c1 := e 1 in
+          let c2 := e 2 in
+          let c3 := e 3 in
+          let c4 := e 4 in
+          let c27 := e 27 in
+          let mdouble := mdouble add_mod sub_mod mult_mod mA c0 c2 c3 in
+          let madd := madd add_mod sub_mod mult_mod mA c0 c2 c3 in
+          let mopp := mopp sub_mod c0 in
+          let scal := scal mdouble madd mopp in
+          let scalL := scalL mdouble madd mopp mult_mod c0 in
+          let da := add_mod in
+          let dm := mult_mod in
+          let isc := (da (dm (dm  (dm c4 mA) mA) mA) (dm (dm c27 mB) mB)) in
+          let a := mtriple (e x) (e y) c1  in
+          let (a1, sc1) := scal isc a S in
+          let (S1,R1) := ZEll.psplit l in
+          let (a2, sc2) := scal sc1 a1 S1 in
+          let (a3, sc3) := scalL sc2 a2 R1 in
+          match a3 with
+           mzero => if (Zeq_bool (Zgcd (d sc3) N) 1) then true
+                    else false
+          | _ => false
+          end
+      | _  => false
+       end
+    | _  => false
+    end 
+    else false.
+
+Time Eval vm_compute in (ell_test
+  329719147332060395689499
+  8209062
+  (List.cons (40165264598163841%positive,1%positive) List.nil)
+  (-94080)
+  9834496
+  0
+  3136).
+
+Time Eval vm_compute in (ell_test
+  1384435372850622112932804334308326689651568940268408537
+  13077052794
+  (List.cons (105867537178241517538435987563198410444088809%positive, 1%positive) List.nil)
+  (-677530058123796416781392907869501000001421915645008494)
+  0
+  (- 169382514530949104195348226967375250000355478911252124)
+  1045670343788723904542107880373576189650857982445904291
+).
+
+*)
+
+(*
+Variable M : number.
+Variable m' : int.
+
+Definition n := length M.
+Definition e z := encode M m' n z.
+Definition d z := decode M m' n z.
+
+Variable exx: ex.
+Variable exxs: ex_spec exx.
+
+Definition S := exx.(vS).
+Definition R := exx.(vR).
+Definition A := e exx.(vA).
+Definition B := e exx.(vB).
+Definition xx := e exx.(vx).
+Definition yy := e exx.(vy).
+Definition c3 := e 3.
+Definition c2 := e 2.
+Definition c1 := e 1.
+Definition c0 := e 0.
+
+Definition pp := mtriple xx yy c1.
+
+Notation "x ++ y " := (add_mod M x y).
+Notation "x -- y" := (sub_mod M x y) (at level 50, left associativity).
+Notation "x ** y" := 
+  (reduce_mult_num M m' n x y) (at level 40, left associativity).
+Notation "x ?= y" := (eq_num x y).
+
+Definition mdouble : number -> melt -> (melt * number):= 
+  fun (sc: number) (p1: melt) =>
+ match p1 with
+  mzero => (p1, sc)
+ | (mtriple x1 y1 z1) =>
+    if (y1 ?= c0) then (mzero, z1 ** sc) else
+     (* we do 2p *)
+    let m' := c3 ** x1 ** x1 ++ A ** z1 ** z1 in
+    let l' := c2 ** y1 ** z1 in
+    let m'2 := m' ** m' in
+    let l'2 := l' ** l' in
+    let l'3 := l'2 ** l' in
+    let x3 := m'2 ** z1 -- c2 ** x1 ** l'2 in
+    (mtriple
+          (l' ** x3)
+          (l'2 ** (m' ** x1 -- y1 ** l') -- m' ** x3)
+          (z1 ** l'3), sc)
+  end.
+
+End MEll.
+
+Print mdouble.
+
+Definition Ex := mkEx 101 99 nil 10 3 4 5.
+
+Check (
+  let v := Eval lazy compute in mdouble 
+ in
+
+Check (fun exx: ex => nN (mkMOp exx)).
+
+
+Definition e z := encode nn nn' nT ll z.
+Definition d z := decode nn nn' nT ll z.
+
+}
+
+Lemma nEx : to_Z nN = to_Z (cons nn nT).
+Proof. unfold nn, nT; case nN; auto. Qed.
+
+Definition nn' := invM (0 - 1) nn.
+
+Notation phi := Int31Op.to_Z.
+
+Lemma nn'_spec : phi (nn * nn') = wB - 1.
+Proof.
+unfold nn'; rewrite invM_spec.
+rewrite sub_spec, to_Z_0, to_Z_1; simpl; auto.
+admit.
+Qed.
+
+Definition ll := length nN.
+
+
+Inductive melt: Type :=
+  mzero | mtriple: number -> number -> number  -> melt.
+
+Definition pp := mtriple xx yy c1.
+
+Definition mplus x y : number := add_mod x y nN.
+Definition msub x y : number := sub_mod x y nN.
+Definition mmult x y : number := reduce_mult_num nn nn' nT x y ll.
+Definition meq x y : bool := eq_num x y.
+
+Notation "x ++ y " := (mplus x y).
+Notation "x -- y" := (msub x y) (at level 50, left associativity).
+Notation "x ** y" := (mmult x y) (at level 40, left associativity).
+Notation "x ?= y" := (meq x y).
+
+Definition mdouble: number -> melt -> (melt * number):= 
+  fun (sc: number) (p1: melt) =>
+ match p1 with
+  mzero => (p1, sc)
+ | (mtriple x1 y1 z1) =>
+    if (y1 ?= c0) then (mzero, z1 ** sc) else
+     (* we do 2p *)
+    let m' := c3 ** x1 ** x1 ++ A ** z1 ** z1 in
+    let l' := c2 ** y1 ** z1 in
+    let m'2 := m' ** m' in
+    let l'2 := l' ** l' in
+    let l'3 := l'2 ** l' in
+    let x3 := m'2 ** z1 -- c2 ** x1 ** l'2 in
+    (mtriple
+          (l' ** x3)
+          (l'2 ** (m' ** x1 -- y1 ** l') -- m' ** x3)
+          (z1 ** l'3), sc)
+  end.
+
+Definition madd := fun (sc : number) (p1 p2 : melt) =>
+ match p1, p2 with
+  mzero, _ => (p2, sc)
+ | _ , mzero => (p1, sc)
+ | (mtriple x1 y1 z1), (mtriple x2 y2 z2) =>
+  let d1 := x2 ** z1 in
+  let d2 := x1 ** z2 in
+  let l := d1 -- d2 in
+  let dl := d1 ++ d2 in
+  let m := y2 ** z1 -- y1 ** z2 in
+  if (l ?= c0) then
+   (* we have p1 = p2 o p1 = -p2 *)
+   if (m ?= c0) then
+    if (y1 ?= c0) then (mzero, z1 ** z2 ** sc) else
+     (* we do 2p *)
+    let m' := c3 ** x1 ** x1 ++ A ** z1 ** z1 in
+    let l' := c2 ** y1 ** z1 in
+    let m'2 := m' ** m' in
+    let l'2 := l' ** l' in
+    let l'3 := l'2 ** l' in
+    let x3 := m'2 ** z1 -- c2 ** x1 ** l'2 in
+    (mtriple
+          (l' ** x3)
+          (l'2 ** (m' ** x1 -- y1 ** l') -- m' ** x3)
+          (z1 ** l'3), z2 ** sc)
+    else (* p - p *)  (mzero, m ** z1 ** z2 ** sc)
+  else
+     let l2 := l ** l in
+     let l3 := l2 ** l in
+     let m2 := m ** m in
+     let x3 := z1 ** z2 ** m2 -- l2 ** dl in
+      (mtriple (l ** x3)
+             (z2 ** l2 ** (m ** x1 -- y1 ** l) -- m ** x3)
+             (z1 ** z2 ** l3), sc)
+  end.
+
+Definition mopp p := 
+  match p with mzero => p | (mtriple x1 y1 z1) => (mtriple x1 (c0 -- y1) z1) end.
+
+Fixpoint scalb (sc: number) (b:bool) (a: melt) (p: positive) {struct p}:
+ melt * number :=
+ match p with
+   xH => if b then mdouble sc a else (a,sc)
+ | xO p1 => let (a1, sc1) := scalb sc false a p1 in
+              if b then 
+                let (a2, sc2) := mdouble sc1 a1 in
+                madd sc2 a a2
+              else mdouble sc1 a1
+ | xI p1 => let (a1, sc1) := scalb sc true a p1 in
+              if b then  mdouble sc1 a1
+              else
+              let (a2, sc2) := mdouble sc1 a1 in 
+              madd sc2 (mopp a) a2
+ end.
+
+Definition scal sc a p := scalb sc false a p.
+
+Definition scal_list sc a l :=
+  List.fold_left 
+  (fun (asc: melt * number) p1 => let (a,sc) := asc in scal sc a p1) l (a,sc).
+
+Fixpoint scalL (sc : number) (a: melt) (l: List.list positive) {struct l} : 
+    (melt * number) :=
+   match l with
+     List.nil => (a,sc)
+   | List.cons n l1 =>
+        let (a1, sc1) := scal sc a n in
+        let (a2, sc2) := scal_list sc1 a l1 in
+          match a2 with
+             mzero => (mzero, c0)
+          |  mtriple _ _ z => scalL (sc2 ** z) a1 l1
+          end
+   end.
+
+Definition zpow sc p n :=
+  let (p,sc') := scal sc p n in
+  (p, Zgcd (d sc') (exx.(vN))).
+
+Definition e2E n := 
+  match n with 
+    mzero => ZEll.nzero
+  | mtriple x1 y1 z1 => ntriple (d x1) (d y1) (d z1)
+  end.
+
+Definition wft t :=  d t = (d t) mod (to_Z nN).
+
+Lemma vN_pos : 0 < exx.(vN).
+Proof. red; simpl; auto. Qed.
+
+Hint Resolve vN_pos.
+
+Lemma mplusz x y : wft x -> wft y -> 
+      d (x ++ y) = nplus (exx.(vN)) (d x) (d y).
+Proof.
+intros Hx Hy.
+unfold d, mplus, nplus.
+(*
+rewrite decode_encode_add.
+rewrite (mop_spec.(add_mod_spec) _ _ _ _ Hx Hy); auto.
+rewrite <- z2ZN; auto.
+*)
+admit.
+Qed.
+
+Lemma mplusw x y : wft x -> wft y ->  wft (x ++ y).
+Proof.
+intros Hx Hy.
+unfold wft.
+(*
+pattern (z2Z (x ++ y)) at 2; rewrite (nplusz Hx Hy).
+unfold ZEll.nplus; rewrite z2ZN.
+rewrite Zmod_mod; auto.
+apply (nplusz Hx Hy).
+*)
+admit.
+Qed.
+
+Lemma msubz x y : wft x -> wft y -> 
+      d (x -- y) = ZEll.nsub (vN exx) (d x) (d y).
+Proof.
+intros Hx Hy.
+(*
+unfold z2Z, nsub.
+rewrite (mop_spec.(sub_mod_spec) _ _ _ _ Hx Hy); auto.
+rewrite <- z2ZN; auto.
+*)
+admit.
+Qed.
+
+Lemma msubw x y : wft x -> wft y ->  wft (x -- y).
+Proof.
+intros Hx Hy.
+unfold wft.
+(*
+pattern (z2Z (x -- y)) at 2; rewrite (nsubz Hx Hy).
+unfold ZEll.nsub; rewrite z2ZN.
+rewrite Zmod_mod; auto.
+apply (nsubz Hx Hy).
+*)
+admit.
+Qed.
+
+Lemma mmulz x y : wft x -> wft y -> 
+      d (x ** y) = ZEll.nmul (vN exx) (d x) (d y).
+Proof.
+intros Hx Hy.
+(*
+unfold z2Z, nmul.
+rewrite (mop_spec.(mul_mod_spec) _ _ _ _ Hx Hy); auto.
+rewrite <- z2ZN; auto.
+*)
+admit.
+Qed.
+
+Lemma mmulw x y : wft x -> wft y ->  wft (x ** y).
+Proof.
+intros Hx Hy.
+unfold wft.
+(*
+pattern (z2Z (x ** y)) at 2; rewrite (nmulz Hx Hy).
+unfold ZEll.nmul; rewrite z2ZN.
+rewrite Zmod_mod; auto.
+apply (nmulz Hx Hy).
+*)
+admit.
+Qed.
+
+Hint Resolve mmulw mplusw msubw.
+
+
+Definition wfe p := match p with
+  mtriple x y z => wft x /\ wft y /\ wft z
+| _ => True
+end.
+
+Lemma dx x : d (e x) = x mod exx.(vN).
+Proof.
+(*
+unfold Z2z; intros x.
+generalize (Z_mod_lt x exx.(vN)).
+case_eq (x mod exx.(vN)).
+intros _ _.
+simpl; unfold z2Z; rewrite ZnZ.spec_0; auto.
+intros p Hp HH; case HH; auto with zarith; clear HH.
+intros _ HH1.
+case (ZnZ.spec_to_Z zN).
+generalize  z2ZN; unfold z2Z; intros HH; rewrite HH; auto.
+intros _ H0.
+set (v := ZnZ.of_pos p); generalize HH1.
+rewrite (ZnZ.spec_of_pos p); fold v.
+case (fst v).
+  simpl; auto.
+intros p1 H1.
+contradict H0; apply Zle_not_lt.
+apply Zlt_le_weak; apply Zle_lt_trans with (2:= H1).
+apply Zle_trans with (1 * base (ZnZ.digits op) + 0); auto with zarith.
+apply Zplus_le_compat; auto.
+apply Zmult_gt_0_le_compat_r; auto with zarith.
+  case (ZnZ.spec_to_Z (snd v)); auto with zarith.
+  case p1; red; simpl; intros; discriminate.
+  case (ZnZ.spec_to_Z (snd v)); auto with zarith.
+intros p Hp; case (Z_mod_lt x exx.(vN)); auto with zarith.
+rewrite Hp; intros HH; case HH; auto.
+*)
+admit.
+Qed.
+
+Lemma dx1 x : d (e x) = d (e x) mod [nN].
+Proof.
+(*
+unfold Z2z; intros x.
+generalize (Z_mod_lt x exx.(vN)).
+case_eq (x mod exx.(vN)).
+intros _ _.
+simpl; unfold z2Z; rewrite ZnZ.spec_0; auto.
+intros p H1 H2.
+case (ZnZ.spec_to_Z zN).
+generalize  z2ZN; unfold z2Z; intros HH; rewrite HH; auto.
+intros _ H0.
+case H2; auto with zarith; clear H2; intros _ H2.
+rewrite Zmod_small; auto.
+set (v := ZnZ.of_pos p).
+split.
+  case (ZnZ.spec_to_Z (snd v)); auto.
+generalize H2; rewrite (ZnZ.spec_of_pos p); fold v.
+case (fst v).
+  simpl; auto.
+intros p1 H.
+contradict H0; apply Zle_not_lt.
+apply Zlt_le_weak; apply Zle_lt_trans with (2:= H).
+apply Zle_trans with (1 * base (ZnZ.digits op) + 0); auto with zarith.
+apply Zplus_le_compat; auto.
+apply Zmult_gt_0_le_compat_r; auto with zarith.
+  case (ZnZ.spec_to_Z (snd v)); auto with zarith.
+  case p1; red; simpl; intros; discriminate.
+  case (ZnZ.spec_to_Z (snd v)); auto with zarith.
+intros p Hp; case (Z_mod_lt x exx.(vN)); auto with zarith.
+rewrite Hp; intros HH; case HH; auto.
+*)
+admit.
+Qed.
+
+Lemma c0w : wft c0.
+Proof. apply dx1. Qed.
+
+Lemma c2w : wft c2.
+Proof. apply dx1. Qed.
+
+Lemma c3w : wft c3.
+Proof. apply dx1. Qed.
+
+Lemma Aw : wft A.
+Proof. apply dx1. Qed.
+
+Hint Resolve c0w c2w c3w Aw.
+
+Ltac nw :=
+  repeat (apply mplusw || apply msubw || apply mmulw || apply c2w ||
+          apply c3w || apply Aw); auto.
+
+Lemma madd_wf x y sc :
+  wfe x -> wfe y -> wft sc ->
+  wfe (fst (madd sc x y)) /\  wft (snd (madd sc x y)).
+Proof.
+destruct x as [ | x1 y1 z1]; auto.
+destruct y as [ | x2 y2 z2]; auto.
+(*
+  intros (wfx1,(wfy1, wfz1)) (wfx2,(wfy2, wfz2)) wfsc; 
+    simpl; auto.
+   case meq.
+    2: repeat split; simpl; nw.
+   case meq.
+    2: repeat split; simpl; nw.
+   case meq.
+   repeat split; simpl; nw; auto.
+   repeat split; simpl; nw; auto.
+*)
+admit.
+Qed.
+
+(*
+
+ Lemma ztest: forall x y,
+     x ?= y =Zeq_bool (z2Z x) (z2Z y).
+ Proof.
+ intros x y.
+ unfold neq.
+ rewrite (ZnZ.spec_compare x y); case Zcompare_spec; intros HH;
+ match goal with H: context[x] |- _ =>
+   generalize H; clear H; intros HH1
+ end.
+ symmetry; apply GZnZ.Zeq_iok; auto.
+ case_eq (Zeq_bool (z2Z x) (z2Z y)); intros H1; auto;
+   generalize HH1; generalize (Zeq_bool_eq _ _ H1); unfold z2Z;
+   intros HH; rewrite HH; auto with zarith.
+ case_eq (Zeq_bool (z2Z x) (z2Z y)); intros H1; auto;
+   generalize HH1; generalize (Zeq_bool_eq _ _ H1); unfold z2Z;
+   intros HH; rewrite HH; auto with zarith.
+ Qed.
+
+ Lemma zc0: z2Z c0 = 0.
+ Proof.
+ unfold z2Z, c0, z2Z; simpl.
+ generalize ZnZ.spec_0; auto.
+ Qed.
+
+
+Ltac iftac t := 
+  match t with 
+   context[if ?x ?= ?y then _ else _] =>
+      case_eq (x ?= y)
+  end.
+
+Ltac ftac := match goal with
+  |- context[?x = ?y] => (iftac x); 
+    let H := fresh "tmp" in 
+     (try rewrite ztest; try rewrite zc0; intros H;
+      repeat ((rewrite nmulz in H || rewrite nplusz in H || rewrite nsubz in H); auto);
+      try (rewrite H; clear H))
+    end.
+
+Require Import Zmod.
+
+Lemma c2ww: forall x, ZEll.nmul (vN exx) 2 x = ZEll.nmul (vN exx) (z2Z c2) x.
+intros x; unfold ZEll.nmul.
+unfold c2; rewrite z2Zx; rewrite Zmodml; auto.
+Qed.
+Lemma c3ww: forall x, ZEll.nmul (vN exx) 3 x = ZEll.nmul (vN exx) (z2Z c3) x.
+intros x; unfold ZEll.nmul.
+unfold c3; rewrite z2Zx; rewrite Zmodml; auto.
+Qed.
+
+Lemma Aww: forall x, ZEll.nmul (vN exx) exx.(vA) x = ZEll.nmul (vN exx) (z2Z A) x.
+intros x; unfold ZEll.nmul.
+unfold A; rewrite z2Zx; rewrite Zmodml; auto.
+Qed.
+
+Lemma nadd_correct: forall x y sc,
+  wfe x -> wfe y -> wft sc ->
+  e2E (fst (nadd sc x y)) = fst (ZEll.nadd exx.(vN) exx.(vA) (z2Z sc) (e2E x) (e2E y) )/\
+  z2Z (snd (nadd sc x y)) = snd (ZEll.nadd exx.(vN) exx.(vA) (z2Z sc) (e2E x) (e2E y)).
+Proof.
+intros x; case x; clear; auto.
+intros x1 y1 z1 y; case y; clear; auto.
+  intros x2 y2 z2 sc (wfx1,(wfy1, wfz1)) (wfx2,(wfy2, wfz2)) wfsc; simpl.
+  ftac.
+  ftac.
+  ftac.
+  simpl; split; auto.
+  repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz); auto).
+  simpl; split; auto.
+  repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz||
+           rewrite c2ww || rewrite c3ww || rewrite Aww); try nw; auto).
+  rewrite nmulz; auto.
+  simpl; split; auto.
+  repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz); auto).
+  simpl; split; auto.
+  repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz ||
+           rewrite c2ww || rewrite c3ww || rewrite Aww); try nw; auto).
+  Qed.
+
+ Lemma ndouble_wf: forall x sc,
+  wfe x -> wft sc ->
+  wfe (fst (ndouble sc x)) /\  wft (snd (ndouble sc x)).
+Proof.
+intros x; case x; clear; auto.
+intros x1 y1 z1 sc (wfx1,(wfy1, wfz1)) wfsc; 
+    simpl; auto.
+  repeat (case neq; repeat split; simpl; nw; auto).
+Qed.
+
+
+Lemma ndouble_correct: forall x sc,
+  wfe x -> wft sc ->
+  e2E (fst (ndouble sc x)) = fst (ZEll.ndouble exx.(vN) exx.(vA) (z2Z sc) (e2E x))/\
+  z2Z (snd (ndouble sc x)) = snd (ZEll.ndouble exx.(vN) exx.(vA) (z2Z sc) (e2E x)).
+Proof.
+intros x; case x; clear; auto.
+  intros x1 y1 z1 sc (wfx1,(wfy1, wfz1))  wfsc; simpl.
+  ftac.
+  simpl; split; auto.
+  repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz); auto).
+  simpl; split; auto.
+  repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz ||
+           rewrite c2ww || rewrite c3ww || rewrite Aww); try nw; auto).
+  Qed.
+
+Lemma nopp_wf: forall x, wfe x -> wfe (nopp x).
+Proof.
+intros x; case x; simpl nopp; auto.
+intros x1 y1 z1 [H1 [H2 H3]]; repeat split; auto.
+Qed.
+
+Lemma scalb_wf: forall n b x sc,
+  wfe x -> wft sc ->
+  wfe (fst (scalb sc b x n)) /\  wft (snd (scalb sc b x n)).
+Proof.
+intros n; elim n; unfold scalb; fold scalb; auto.
+  intros n1 Hrec b x sc H H1.
+    case (Hrec true x sc H H1).
+    case scalb; simpl fst; simpl snd.
+    intros a1 sc1 H2 H3.
+    case (ndouble_wf _ H2 H3); auto;
+    case ndouble; simpl fst; simpl snd; intros x2 sc2 H4 H5.
+    case b; auto.
+    case (nadd_wf _ _ (nopp_wf _ H) H4 H5); auto;
+    case ndouble; simpl fst; simpl snd; intros x2 sc2 H4 H5.
+  intros n1 Hrec b x sc H H1.
+    case (Hrec false x sc H H1).
+    case scalb; simpl fst; simpl snd.
+    intros a1 sc1 H2 H3.
+    case (ndouble_wf _ H2 H3); auto;
+    case ndouble; simpl fst; simpl snd; intros x2 sc2 H4 H5.
+    case b; auto.
+    case (nadd_wf _ _ H H4 H5); auto;
+    case ndouble; simpl fst; simpl snd; intros x2 sc2 H4 H5.
+intros b x sc H H1; case b; auto.
+case (ndouble_wf _ H H1); auto.
+Qed.
+
+
+Lemma scal_wf: forall n x sc,
+  wfe x -> wft sc ->
+  wfe (fst (scal sc x n)) /\  wft (snd (scal sc x n)).
+Proof.
+intros n; exact (scalb_wf n false).
+Qed.
+
+Lemma nopp_correct: forall x,
+  wfe x -> e2E x = ZEll.nopp exx.(vN) (e2E (nopp x)).
+Proof.
+intros x; case x; simpl; auto.
+intros x1 y1 z1 [H1 [H2 H3]]; apply f_equal3 with (f := ZEll.ntriple); auto.
+rewrite nsubz; auto.
+rewrite zc0.
+unfold ZEll.nsub, ninv; simpl.
+apply sym_equal.
+rewrite <- (Z_mod_plus) with (b := -(-z2Z y1 /exx.(vN))); auto with zarith.
+rewrite <- Zopp_mult_distr_l.
+rewrite <- Zopp_plus_distr.
+rewrite Zmult_comm; rewrite Zplus_comm.
+rewrite <- Z_div_mod_eq; auto with zarith.
+rewrite Zopp_involutive; rewrite <- z2ZN.
+apply sym_equal; auto.
+Qed.
+
+Lemma scalb_correct: forall n b x sc,
+  wfe x -> wft sc ->
+  e2E (fst (scalb sc b x n)) = fst (ZEll.scalb exx.(vN) exx.(vA) (z2Z sc) b (e2E x) n)/\
+  z2Z (snd (scalb sc b x n)) = snd (ZEll.scalb exx.(vN) exx.(vA) (z2Z sc) b (e2E x) n).
+Proof.
+intros n; elim n; clear; auto.
+intros p Hrec b x sc H1 H2.
+  case b; unfold scalb; fold scalb.
+    generalize (scalb_wf p true x H1 H2);
+    generalize (Hrec true _ _ H1 H2); case scalb; simpl.
+    case ZEll.scalb; intros r1 rc1; simpl.
+    intros a2 sc2 (H3, H4) (H5, H6); subst r1 rc1.
+    apply ndouble_correct; auto.
+    generalize (scalb_wf p true x H1 H2);
+    generalize (Hrec true _ _ H1 H2); case scalb; simpl.
+    case ZEll.scalb; intros r1 rc1; simpl.
+    intros a2 sc2 (H3, H4) (H5, H6); subst r1 rc1.
+    generalize (ndouble_wf _ H5 H6); 
+      generalize (ndouble_correct _ H5 H6); case ndouble; simpl.
+    case ZEll.ndouble; intros r1 rc1; simpl.
+    intros a3 sc3 (H7,H8) (H9,H10); subst r1 rc1.
+    replace (ZEll.nopp (vN exx) (e2E x)) with
+      (e2E (nopp x)).
+    apply nadd_correct; auto. 
+    generalize H1; case x; auto.
+    intros x1 y1 z1 [HH1 [HH2 HH3]]; split; auto.
+    rewrite nopp_correct; auto.
+    apply f_equal2 with (f := ZEll.nopp); auto.
+    generalize H1; case x; simpl; auto; clear x H1.
+    intros x1 y1 z1 [HH1 [HH2 HH3]]; 
+      apply f_equal3 with (f := ZEll.ntriple); auto.
+    repeat rewrite nsubz; auto.
+    rewrite zc0.
+    unfold ZEll.nsub; simpl.
+    rewrite <- (Z_mod_plus) with (b := -(-z2Z y1 /exx.(vN))); auto with zarith.
+    rewrite <- Zopp_mult_distr_l.
+    rewrite <- Zopp_plus_distr.
+    rewrite Zmult_comm; rewrite Zplus_comm.
+    rewrite <- Z_div_mod_eq; auto with zarith.
+    rewrite Zopp_involutive; rewrite <- z2ZN.
+    apply sym_equal; auto.
+    generalize H1; case x; auto.
+    intros x1 y1 z1 [HH1 [HH2 HH3]]; split; auto.
+intros p Hrec b x sc H1 H2.
+  case b; unfold scalb; fold scalb.
+    generalize (scalb_wf p false x H1 H2);
+    generalize (Hrec false _ _ H1 H2); case scalb; simpl.
+    case ZEll.scalb; intros r1 rc1; simpl.
+    intros a2 sc2 (H3, H4) (H5, H6); subst r1 rc1.
+    generalize (ndouble_wf _ H5 H6); 
+      generalize (ndouble_correct _ H5 H6); case ndouble; simpl.
+    case ZEll.ndouble; intros r1 rc1; simpl.
+    intros a3 sc3 (H7,H8) (H9,H10); subst r1 rc1.
+    replace (ZEll.nopp (vN exx) (e2E x)) with
+      (e2E (nopp x)).
+    apply nadd_correct; auto.
+    rewrite nopp_correct; auto.
+    apply f_equal2 with (f := ZEll.nopp); auto.
+    generalize H1; case x; simpl; auto; clear x H1.
+    intros x1 y1 z1 [HH1 [HH2 HH3]]; 
+      apply f_equal3 with (f := ZEll.ntriple); auto.
+    repeat rewrite nsubz; auto.
+    rewrite zc0.
+    unfold ZEll.nsub; simpl.
+    rewrite <- (Z_mod_plus) with (b := -(-z2Z y1 /exx.(vN))); auto with zarith.
+    rewrite <- Zopp_mult_distr_l.
+    rewrite <- Zopp_plus_distr.
+    rewrite Zmult_comm; rewrite Zplus_comm.
+    rewrite <- Z_div_mod_eq; auto with zarith.
+    rewrite Zopp_involutive; rewrite <- z2ZN.
+    apply sym_equal; auto.
+    generalize H1; case x; auto.
+    intros x1 y1 z1 [HH1 [HH2 HH3]]; split; auto.
+    generalize (scalb_wf p false x H1 H2);
+    generalize (Hrec false _ _ H1 H2); case scalb; simpl.
+    case ZEll.scalb; intros r1 rc1; simpl.
+    intros a2 sc2 (H3, H4) (H5, H6); subst r1 rc1.
+    apply ndouble_correct; auto.
+intros b x sc H H1.
+case b; simpl; auto.
+apply ndouble_correct; auto.
+Qed.
+
+
+Lemma scal_correct: forall n x sc,
+  wfe x -> wft sc ->
+  e2E (fst (scal sc x n)) = fst (ZEll.scal exx.(vN) exx.(vA) (z2Z sc) (e2E x) n)/\
+  z2Z (snd (scal sc x n)) = snd (ZEll.scal exx.(vN) exx.(vA) (z2Z sc) (e2E x) n).
+Proof.
+intros n; exact (scalb_correct n false).
+Qed. 
+
+Lemma scal_list_correct: forall l x sc,
+  wfe x -> wft sc ->
+  e2E (fst (scal_list sc x l)) = fst (ZEll.scal_list exx.(vN) exx.(vA) (z2Z sc) (e2E x) l)/\
+  z2Z (snd (scal_list sc x l)) = snd (ZEll.scal_list exx.(vN) exx.(vA) (z2Z sc) (e2E x) l).
+Proof.
+intros l1; elim l1; simpl; auto.
+unfold scal_list, ZEll.scal_list; simpl; intros a l2 Hrec x sc H1 H2.
+generalize (scal_correct a _ H1 H2) (scal_wf a _ H1 H2); case scal.
+case ZEll.scal; intros r1 rsc1; simpl.
+simpl; intros a1 sc1 (H3, H4) (H5, H6); subst r1 rsc1; auto.
+Qed.
+
+Lemma scal_list_wf: forall l x sc,
+  wfe x -> wft sc ->
+  wfe (fst (scal_list sc x l)) /\  wft (snd (scal_list sc x l)).
+Proof.
+intros l1; elim l1; simpl; auto.
+unfold scal_list; intros a l Hrec x sc H1 H2; simpl.
+generalize (@scal_wf a _ _ H1 H2); 
+  case (scal sc x a); simpl; intros x1 sc1 [H3 H4]; auto.
+Qed.
+
+Lemma scalL_wf: forall l x sc,
+  wfe x -> wft sc ->
+  wfe (fst (scalL sc x l)) /\  wft (snd (scalL sc x l)).
+Proof.
+intros l1; elim l1; simpl; auto.
+intros a l2 Hrec x sc H1 H2.
+generalize (scal_wf a _ H1 H2); case scal; simpl.
+intros a1 sc1 (H3, H4); auto.
+generalize (scal_list_wf l2 _ H1 H4); case scal_list; simpl.
+intros a2 sc2; case a2; simpl; auto.
+intros x1 y1 z1 ((V1, (V2, V3)), V4); apply Hrec; auto.
+Qed. 
+
+Lemma scalL_correct: forall l x sc,
+  wfe x -> wft sc ->
+  e2E (fst (scalL sc x l)) = fst (ZEll.scalL exx.(vN) exx.(vA) (z2Z sc) (e2E x) l)/\
+  z2Z (snd (scalL sc x l)) = snd (ZEll.scalL exx.(vN) exx.(vA) (z2Z sc) (e2E x) l).
+Proof.
+intros l1; elim l1; simpl; auto.
+intros a l2 Hrec x sc H1 H2.
+generalize (scal_wf a _ H1 H2) (scal_correct a _ H1 H2); case scal; simpl.
+case ZEll.scal; intros r1 rsc1; simpl.
+intros a1 sc1 (H3, H4) (H5, H6); subst r1 rsc1.
+generalize (scal_list_wf l2 _ H1 H4) (scal_list_correct l2 _ H1 H4); case scal_list; simpl.
+case ZEll.scal_list; intros r1 rsc1; simpl.
+intros a2 sc2 (H7, H8) (H9, H10); subst r1 rsc1.
+generalize H7; clear H7; case a2; simpl; auto.
+rewrite zc0; auto.
+intros x1 y1 z1 (V1, (V2, V3)); auto.
+generalize (nmulw H8 V3) (nmulz H8 V3); intros V4 V5; rewrite <- V5.
+apply Hrec; auto.
+Qed.
+
+Lemma f4 : wft (Z2z 4).
+Proof.
+red; apply z2Zx1.
+Qed.
+
+Lemma f27 : wft (Z2z 27).
+Proof.
+red; apply z2Zx1.
+Qed.
+
+Lemma Bw : wft B.
+Proof.
+red; unfold B; apply z2Zx1.
+Qed.
+
+Hint Resolve f4 f27 Bw.
+
+Lemma mww: forall x y, ZEll.nmul (vN exx) (x mod (vN exx) ) y = ZEll.nmul (vN exx) x y.
+intros x  y; unfold ZEll.nmul; rewrite Zmodml; auto.
+Qed.
+
+Lemma wwA: forall x, ZEll.nmul (vN exx) x exx.(vA) = ZEll.nmul (vN exx) x (z2Z A).
+intros x; unfold ZEll.nmul.
+unfold A; rewrite z2Zx; rewrite Zmodmr; auto.
+Qed.
+
+Lemma wwB: forall x, ZEll.nmul (vN exx) x exx.(vB) = ZEll.nmul (vN exx) x (z2Z B).
+intros x; unfold ZEll.nmul.
+unfold B; rewrite z2Zx; rewrite Zmodmr; auto.
+Qed.
+
+ Lemma  scalL_prime: 
+  let a := ntriple (Z2z (exx.(vx))) (Z2z (exx.(vy))) c1 in
+  let isc := (Z2z 4) ** A ** A ** A  ++ (Z2z 27) ** B ** B in
+  let (a1, sc1) := scal isc a exx.(vS) in
+  let (S1,R1) := psplit exx.(vR) in
+  let (a2, sc2) := scal sc1 a1 S1 in
+  let (a3, sc3) := scalL sc2 a2 R1 in
+    match a3 with
+     nzero => if (Zeq_bool (Zgcd (z2Z sc3) exx.(vN)) 1) then prime exx.(vN)
+              else True
+   | _ => True
+   end.
+  Proof.
+  intros a isc.
+  case_eq (scal isc a (vS exx)); intros a1 sc1 Ha1.
+  case_eq (psplit (vR exx)); intros S1 R1 HS1.
+  case_eq (scal sc1 a1 S1); intros a2 sc2 Ha2.
+  case_eq (scalL sc2 a2 R1); intros a3 sc3; case a3; auto.
+  intros Ha3; case_eq (Zeq_bool (Zgcd (z2Z sc3) (vN exx)) 1); auto.
+  intros H1.
+  assert (F0: 
+     (vy exx mod vN exx) ^ 2 mod vN exx =
+       ((vx exx mod vN exx) ^ 3 + vA exx * (vx exx mod vN exx) +
+        vB exx) mod vN exx).
+      generalize exxs.(inC).
+      simpl; unfold Zpower_pos; simpl.
+      repeat rewrite Zmult_1_r.
+      intros HH.
+      match goal with |- ?t1 = ?t2 => rmod t1; auto end.
+      rewrite HH.
+      rewrite Zplus_mod; auto; symmetry; rewrite Zplus_mod; auto; symmetry.
+      apply f_equal2 with (f := Zmod); auto.
+      apply f_equal2 with (f := Zplus); auto.
+      rewrite Zplus_mod; auto; symmetry; rewrite Zplus_mod; auto; symmetry.
+      apply f_equal2 with (f := Zmod); auto.
+      apply f_equal2 with (f := Zplus); auto.
+      rewrite Zmult_mod; auto; symmetry; rewrite Zmult_mod; auto; symmetry.
+      apply f_equal2 with (f := Zmod); auto.
+      apply f_equal2 with (f := Zmult); auto.
+      rewrite Zmod_mod; auto.
+      match goal with |- ?t1 = ?t2 => rmod t2; auto end.
+      rewrite Zmult_mod; auto; symmetry; rewrite Zmult_mod; auto; symmetry.
+      apply f_equal2 with (f := Zmod); auto.
+      rewrite Zmod_mod; auto.
+   generalize (@ZEll.scalL_prime exx.(vN) 
+               (exx.(vx) mod exx.(vN))
+               (exx.(vy) mod exx.(vN))
+               exx.(vA)
+               exx.(vB) 
+               exxs.(n_pos) exxs.(n2_div) exx.(vR) 
+               exxs.(lprime) exx.(vS) exxs.(lbig) F0); simpl.
+generalize (@scal_wf (vS exx) a isc) (@scal_correct (vS exx) a isc).
+unfold isc.
+rewrite nplusz; auto; try nw; auto.
+repeat rewrite nmulz; auto; try nw; auto.
+  repeat rewrite z2Zx.
+repeat rewrite wwA || rewrite wwB|| rewrite mww.
+replace (e2E a) with (ZEll.ntriple (vx exx mod vN exx) (vy exx mod vN exx) 1).
+case ZEll.scal.
+fold isc; rewrite HS1; rewrite Ha1; simpl; auto.
+intros r1 rsc1 HH1 HH2.
+case HH1; clear HH1.
+  unfold c1; repeat split; red; try apply z2Zx1.
+  unfold isc; nw.
+case HH2; clear HH2.
+  unfold c1; repeat split; red; try apply z2Zx1.
+  unfold isc; nw.
+intros U1 U2 W1 W2; subst r1 rsc1.
+generalize (@scal_wf S1 a1 sc1) (@scal_correct S1 a1 sc1).
+case ZEll.scal.
+intros r1 rsc1 HH1 HH2.
+case HH1; clear HH1; auto.
+case HH2; clear HH2; auto.
+rewrite Ha2; simpl.
+intros U1 U2 W3 W4; subst r1 rsc1.
+generalize (@scalL_wf R1 a2 sc2) (@scalL_correct R1 a2 sc2).
+case ZEll.scalL.
+intros n; case n; auto.
+rewrite Ha3; simpl.
+intros rsc1 HH1 HH2.
+case HH1; clear HH1; auto.
+case HH2; clear HH2; auto.
+intros _ U2 _ W5; subst rsc1.
+rewrite H1; auto.
+intros x1 y1 z1 sc4; rewrite Ha3; simpl; auto.
+intros _ HH; case HH; auto.
+intros; discriminate.
+unfold a; simpl.
+unfold c1; repeat rewrite z2Zx.
+rewrite (Zmod_small 1); auto.
+generalize exxs.(n_pos).
+auto with zarith.
+Qed.
+*)
+
+End NEll.
+
+Definition isM2 p := 
+  match p with
+    xH   => false
+|    xO _ => false
+|     _ => true
+end.
+
+Lemma isM2_correct: forall p,
+  if isM2 p then ~(Zdivide 2 p) /\ 2 < p else True.
+Proof.
+intros p; case p; simpl; auto; clear p.
+intros p1; split; auto.
+intros HH; inversion_clear HH.
+generalize H; rewrite Zmult_comm.
+case x; simpl; intros; discriminate.
+case p1; red; simpl; auto.
+Qed.
+
+Definition ell_test (N S: positive) (l: List.list (positive * positive))
+                      (A B x y: Z) :=
+    if isM2 N then
+    match (4 * N) ?= (ZEll.Zmullp l - 1) ^ 2  with
+      Lt => 
+       match y ^ 2 mod N ?= (x ^ 3 + A * x + B) mod N with
+       Eq => 
+          let ex := mkEx N S l A B x y in
+          let e2n := e ex in
+          let a := mtriple (e2n x) (e2n y) (e2n 1)  in
+          let A := (e2n A) in
+          let B := (e2n B) in
+          let d4 := (e2n 4) in
+          let d27 := (e2n 27) in
+          let dN := nN ex in
+          let n := nn ex in
+          let n' := nn' ex in
+          let da := mplus ex in
+          let dm := mmult ex in
+          let isc := (da (dm (dm  (dm d4 A) A) A) (dm (dm d27 B) B)) in
+          let (a1, sc1) := scal ex isc a S in
+          let (S1,R1) := ZEll.psplit l in
+          let (a2, sc2) := scal ex sc1 a1 S1 in
+          let (a3, sc3) := scalL ex sc2 a2 R1 in
+          match a3 with
+           mzero => if (Zeq_bool (Zgcd (d ex sc3) N) 1) then true
+                    else false
+          | _ => false
+          end
+      | _  => false
+       end
+    | _  => false
+    end 
+    else false.
+
+(*
+Lemma Zcompare_correct: forall x y,
+  match x ?= y with Eq => x = y | Gt => x > y | Lt => x < y end.
+Proof.
+intros x y; unfold Zlt, Zgt; generalize (Zcompare_Eq_eq x y); case Zcompare; auto.
+Qed.
+
+Lemma ell_test_correct: forall (N S: positive) (l: List.list (positive * positive))
+                      (A B x y: Z),
+  (forall p, List.In p l -> prime (fst p)) -> 
+  if ell_test N S l A B x y then prime N else True.
+intros N S1 l A1 B1 x y H; unfold ell_test.
+generalize (isM2_correct N); case isM2; auto.
+intros (H1, H2).
+match goal with |- context[?x ?= ?y] =>
+  generalize (Zcompare_correct x y); case Zcompare; auto
+end; intros H3.
+match goal with |- context[?x ?= ?y] =>
+  generalize (Zcompare_correct x y); case Zcompare; auto
+end; intros H4.
+set (n := Peano.pred (nat_of_P (get_height 31 (plength N)))).
+set (op := cmk_op n).
+set (mop := make_mod_op op (ZnZ.of_Z N)).
+set (exx := mkEx N S1 l A1 B1 x y).
+set (op_spec := cmk_spec n).
+assert (exxs: ex_spec exx).
+  constructor; auto.
+assert (H0: N < base (ZnZ.digits op)).
+  apply Zlt_le_trans with (1 := plength_correct N).
+  unfold op, base.
+  rewrite cmk_op_digits.
+  apply Zpower_le_monotone; split; auto with zarith.
+  generalize (get_height_correct 31 (plength N)); unfold n.
+  set (p := plength N).
+  replace (Z_of_nat (Peano.pred (nat_of_P (get_height 31 p)))) with
+       ((Zpos (get_height 31 p) - 1) ); auto with zarith.
+  rewrite pred_of_minus; rewrite inj_minus1; auto with zarith.
+  rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto with zarith.
+  generalize (lt_O_nat_of_P (get_height 31 p)); auto with zarith.
+assert (mspec: mod_spec op (zN exx op) mop).
+  unfold mop; apply make_mod_spec; auto.
+  rewrite ZnZ.of_Z_correct; auto with zarith.
+generalize (@scalL_prime exx exxs _ op (cmk_spec n) mop mspec H0).
+lazy zeta.
+unfold c1, A, B,  nplus, nmul; 
+  simpl exx.(vA); simpl exx.(vB); simpl exx.(vx); simpl exx.(vy);
+  simpl exx.(vS); simpl exx.(vR); simpl exx.(vN).
+case scal; intros a1 sc1.
+case ZEll.psplit; intros S2 R2.
+case scal; intros a2 sc2.
+case scalL; intros a3 sc3.
+case a3; auto.
+case Zeq_bool; auto.
+Qed.
+*)
+
+Time Eval vm_compute in (ell_test
+  329719147332060395689499
+  8209062
+  (List.cons (40165264598163841%positive,1%positive) List.nil)
+  (-94080)
+  9834496
+  0
+  3136).
+
+
+Time Eval vm_compute in (ell_test
+  1384435372850622112932804334308326689651568940268408537
+  13077052794
+  (List.cons (105867537178241517538435987563198410444088809%positive, 1%positive) List.nil)
+  (-677530058123796416781392907869501000001421915645008494)
+  0
+  (- 169382514530949104195348226967375250000355478911252124)
+  1045670343788723904542107880373576189650857982445904291
+).
+*)
\ No newline at end of file
diff --git a/coqprime/num/Mod_op.v b/coqprime/num/Mod_op.v
new file mode 100644
index 000000000..a8f25bd2d
--- /dev/null
+++ b/coqprime/num/Mod_op.v
@@ -0,0 +1,1200 @@
+
+(*************************************************************)
+(*      This file is distributed under the terms of the      *)
+(*      GNU Lesser General Public License Version 2.1        *)
+(*************************************************************)
+(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
+(*************************************************************)
+
+Set Implicit Arguments.
+
+Require Import DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv. 
+Require Import CyclicAxioms DoubleCyclic BigN Cyclic31.
+Require Import ZArith ZCAux.
+Import CyclicAxioms DoubleType DoubleBase.
+
+Theorem Zpos_pos: forall x, 0 < Zpos x.
+red; simpl; auto.
+Qed.
+Hint Resolve Zpos_pos: zarith.
+
+Section Mod_op.
+
+ Variable w : Type.
+ 
+ Record mod_op : Type := mk_mod_op {    
+   succ_mod   : w -> w;
+   add_mod    : w -> w -> w;
+   pred_mod   : w -> w;
+   sub_mod    : w -> w -> w;
+   mul_mod    : w -> w -> w;
+   square_mod : w -> w;
+   power_mod  : w -> positive -> w
+ }.
+
+ Variable w_op : ZnZ.Ops w.
+ 
+ Let w_digits      := w_op.(ZnZ.digits).
+ Let w_zdigits     := w_op.(ZnZ.zdigits).
+ Let w_to_Z        := (@ZnZ.to_Z _ w_op).
+ Let w_of_pos      := (@ZnZ.of_pos _ w_op).
+ Let w_head0       := (@ZnZ.head0 _ w_op).
+ Let w0            := (@ZnZ.zero _ w_op).
+ Let w1            := (@ZnZ.one _ w_op).
+ Let wBm1          := (@ZnZ.minus_one _ w_op).
+
+ Let wWW           := (@ZnZ.WW _ w_op).
+ Let wW0           := (@ZnZ.WO _ w_op).
+ Let w0W           := (@ZnZ.OW _ w_op).
+
+ Let w_compare     := (@ZnZ.compare _ w_op).
+ Let w_opp_c       := (@ZnZ.opp_c _ w_op).
+ Let w_opp         := (@ZnZ.opp _ w_op).
+ Let w_opp_carry   := (@ZnZ.opp_carry _ w_op).
+
+ Let w_succ        := (@ZnZ.succ _ w_op).
+ Let w_succ_c      := (@ZnZ.succ_c _ w_op).
+ Let w_add_c       := (@ZnZ.add_c _ w_op).
+ Let w_add_carry_c := (@ZnZ.add_carry_c _ w_op).
+ Let w_add         := (@ZnZ.add _ w_op).
+
+
+ Let w_pred_c      := (@ZnZ.pred_c _ w_op).
+ Let w_sub_c       := (@ZnZ.sub_c _ w_op).
+ Let w_sub_carry   := (@ZnZ.sub_carry _ w_op).
+ Let w_sub_carry_c := (@ZnZ.sub_carry_c _ w_op).
+ Let w_sub         := (@ZnZ.sub _ w_op).
+ Let w_pred        := (@ZnZ.pred _ w_op).
+
+ Let w_mul_c       := (@ZnZ.mul_c _ w_op).
+ Let w_mul         := (@ZnZ.mul _ w_op).
+ Let w_square_c    := (@ZnZ.square_c _ w_op).
+
+ Let w_div21       := (@ZnZ.div21 _ w_op).
+ Let w_add_mul_div := (@ZnZ.add_mul_div _ w_op).
+
+ Variable b : w.
+    (* b should be > 1 *)
+ Let n := w_head0 b.
+
+ Let b2n := w_add_mul_div n b w0.
+
+ Let bm1 := w_sub b w1.
+
+ Let mb := w_opp b.
+
+ Let wwb := WW w0 b.
+
+ Let low x := match x with WW _ x => x | W0 => w0 end.
+
+ Let w_add2 x y := match w_add_c x y with
+                     C0 n => WW w0 n
+                    |C1 n => WW w1 n
+                    end.
+ Let ww_zdigits := w_add2 w_zdigits w_zdigits.
+ 
+ Let ww_compare := 
+  Eval lazy beta delta [ww_compare] in ww_compare w0 w_compare.
+
+ Let ww_sub := 
+ Eval lazy beta delta [ww_sub] in 
+   ww_sub w0 wWW w_opp_c w_opp_carry w_sub_c w_opp w_sub w_sub_carry.
+
+ Let ww_add_mul_div :=
+ Eval lazy beta delta [ww_add_mul_div] in 
+   ww_add_mul_div w0 wWW wW0 w0W 
+              ww_compare w_add_mul_div 
+              ww_sub w_zdigits low (w0W n).
+
+ Let ww_lsl_n :=
+   Eval lazy beta delta [ww_add_mul_div] in
+    fun ww => ww_add_mul_div  ww W0.
+
+ Let w_lsr_n w :=
+     w_add_mul_div (w_sub w_zdigits n) w0 w.
+
+ Open Scope Z_scope. 
+ Notation "[| x |]" :=
+   (@ZnZ.to_Z _ w_op x)  (at level 0, x at level 99).
+
+Notation "[[ x ]]" :=
+   (@ww_to_Z _ w_digits w_to_Z x)  (at level 0, x at level 99).
+
+ Section Mod_spec.
+ 
+   Variable m_op : mod_op.
+
+   Record mod_spec : Prop := mk_mod_spec {
+      succ_mod_spec     : 
+                forall w t, [|w|]= t mod [|b|] ->
+                          [|succ_mod m_op w|] = ([|w|] + 1) mod [|b|];
+      add_mod_spec      :
+            forall w1 w2 t1 t2, [|w1|]= t1 mod [|b|] -> [|w2|]= t2 mod [|b|] ->
+                          [|add_mod m_op w1 w2|] = ([|w1|] + [|w2|]) mod [|b|];
+      pred_mod_spec     :
+                forall w t, [|w|]= t mod [|b|] ->
+                          [|pred_mod m_op w|] = ([|w|] - 1) mod [|b|];
+      sub_mod_spec      :
+            forall w1 w2 t1 t2, [|w1|]= t1 mod [|b|] -> [|w2|]= t2 mod [|b|] ->
+                          [|sub_mod m_op w1 w2|] = ([|w1|] - [|w2|]) mod [|b|];
+      mul_mod_spec      :
+            forall w1 w2 t1 t2, [|w1|]= t1 mod [|b|] -> [|w2|]= t2 mod [|b|] ->
+                          [|mul_mod m_op w1 w2|] = ([|w1|] * [|w2|]) mod [|b|];
+      square_mod_spec   :
+                forall w t, [|w|]= t mod [|b|] ->
+                          [|square_mod m_op w|] = ([|w|] * [|w|]) mod [|b|];
+      power_mod_spec    :
+              forall w t p, [|w|]= t mod [|b|] ->
+                          [|power_mod m_op w p|] = (Zpower_pos [|w|] p) mod [|b|]
+(*
+      shift_spec        :
+              forall w p, wf w -> 
+                          [|shift m_op w p|] = ([|w|] / (Zpower_pos 2 p)) mod [|b|];
+      trunc_spec        :
+              forall w p, wf w ->
+                          [|power_mod m_op w p|] = ([|w1|] mod (Zpower_pos 2 p)) mod [|b|]
+*)
+    }.
+
+  End Mod_spec.
+
+ Hypothesis b_pos: 1 < [|b|].
+ Variable op_spec: ZnZ.Specs w_op.
+
+
+ Lemma Zpower_n: 0 < 2 ^ [|n|].
+ apply Zpower_gt_0; auto with zarith.
+ case (ZnZ.spec_to_Z n); auto with zarith.
+ Qed.
+
+ Hint Resolve Zpower_n Zmult_lt_0_compat Zpower_gt_0.
+
+ Variable m_op : mod_op.
+
+ Hint Rewrite 
+    ZnZ.spec_0
+    ZnZ.spec_1
+    ZnZ.spec_m1
+    ZnZ.spec_WW
+    ZnZ.spec_opp_c
+    ZnZ.spec_opp	
+    ZnZ.spec_opp_carry 
+    ZnZ.spec_succ_c
+    ZnZ.spec_add_c
+    ZnZ.spec_add_carry_c 
+    ZnZ.spec_add
+    ZnZ.spec_pred_c
+    ZnZ.spec_sub_c
+    ZnZ.spec_sub_carry_c
+    ZnZ.spec_sub
+    ZnZ.spec_mul_c
+    ZnZ.spec_mul
+    : w_rewrite.
+
+ Let _succ_mod x :=
+  let res :=w_succ x in
+  match w_compare res b with 
+  | Lt => res
+  | _ => w0
+  end.
+
+ Let split x := 
+  match x with
+  | W0 => (w0,w0)
+  | WW h l => (h,l)
+  end. 
+
+ Let _w0_is_0: [|w0|] = 0.
+ unfold ZnZ.to_Z; rewrite <- ZnZ.spec_0; auto.
+ Qed.
+
+ Let _w1_is_1: [|w1|] = 1.
+ unfold ZnZ.to_Z; rewrite <-ZnZ.spec_1; simpl; auto.
+ Qed.
+
+ Theorem Zmod_plus_one: forall a1 b1, 0 < b1 -> (a1 + b1) mod b1 = a1 mod b1.
+ intros a1 b1 H; rewrite Zplus_mod; auto with zarith.
+ rewrite Z_mod_same; try rewrite Zplus_0_r; auto with zarith.
+ apply Zmod_mod; auto.
+ Qed.
+
+ Theorem Zmod_minus_one: forall a1 b1, 0 < b1 -> (a1 - b1) mod b1 = a1 mod b1.
+ intros a1 b1 H; rewrite Zminus_mod; auto with zarith.
+ rewrite Z_mod_same; try rewrite Zminus_0_r; auto with zarith.
+ apply Zmod_mod; auto.
+ Qed.
+
+ Lemma without_c_b: forall w2, [|w2|] < [|b|] -> 
+    [|w_succ w2|] = [|w2|] + 1.
+ intros w2 H.
+ unfold w_succ;rewrite ZnZ.spec_succ.
+ rewrite Zmod_small;auto.
+ assert (HH := ZnZ.spec_to_Z w2).
+ assert (HH' := ZnZ.spec_to_Z b);auto with zarith.
+ Qed.
+
+ Lemma _succ_mod_spec: forall w t, [|w|]= t mod [|b|] ->
+    [|_succ_mod w|] = ([|w|] + 1) mod [|b|].
+ intros w2 t H; unfold _succ_mod, w_compare; simpl.
+ assert (F: [|w2|] < [|b|]).
+ case (Z_mod_lt t [|b|]); auto with zarith.
+ rewrite ZnZ.spec_compare; case Zcompare_spec; intros H1;
+ match goal with H: context[w_succ _] |- _ =>
+   generalize H; clear H; rewrite (without_c_b _ F); intros H1;
+   auto with zarith
+ end.
+ rewrite H1, Z_mod_same, _w0_is_0; auto with zarith.
+ rewrite Zmod_small; auto with zarith.
+ case (ZnZ.spec_to_Z w2); auto with zarith.
+ Qed.
+
+ Let _add_mod x y :=
+  match w_add_c x y with
+  | C0 z =>
+    match w_compare z b with
+    | Lt => z
+    | Eq => w0
+    | Gt => w_sub z b
+    end
+  | C1 z => w_add mb z
+  end.
+
+ Lemma _add_mod_correct: forall w1 w2, [|w1|] + [|w2|] < 2 * [|b|] ->
+     [|_add_mod w1 w2|] = ([|w1|] + [|w2|]) mod [|b|].
+ intros w2 w3; unfold _add_mod, w_compare, w_add_c; intros H.
+ match goal with |- context[ZnZ.add_c ?x ?y] =>
+   generalize (ZnZ.spec_add_c x y); unfold interp_carry;
+   case (ZnZ.add_c x y); autorewrite with w_rewrite
+ end; auto with zarith.
+ intros w4 H2.
+ rewrite ZnZ.spec_compare; case Zcompare_spec; intros H1;
+ match goal with H: context[b] |- _ =>
+   generalize H; clear H; intros H1; rewrite <-H2;
+   auto with zarith
+ end.
+ rewrite H1, Z_mod_same; auto with zarith.
+ rewrite Zmod_small; auto with zarith.
+ case (ZnZ.spec_to_Z w4); auto with zarith.
+ assert (F1: 0 < [|w4|] - [|b|]); auto with zarith.
+ assert (F2: [|w4|] < [|b|] + [|b|]); auto with zarith.
+ autorewrite with w_rewrite; auto.
+ rewrite (fun x y => Zmod_small (x - y)); auto with zarith.
+ rewrite <- (Zmod_minus_one [|w4|]); auto with zarith.
+ apply sym_equal; apply Zmod_small; auto with zarith.
+ split; auto with zarith.
+ apply Zlt_trans with [|b|]; auto with zarith.
+ case (ZnZ.spec_to_Z b); unfold base; auto with zarith.
+ rewrite Zmult_1_l; intros w4 H2; rewrite <- H2.
+ unfold mb, w_add; rewrite ZnZ.spec_add; auto with zarith.
+ assert (F1: [|w4|] < [|b|]).
+ assert (F2: base (ZnZ.digits w_op) + [|w4|] < base (ZnZ.digits w_op) + [|b|]);
+   auto with zarith.
+ rewrite H2.
+ apply Zlt_trans with ([|b|] +[|b|]); auto with zarith.
+ apply Zplus_lt_compat_r; auto with zarith.
+ case (ZnZ.spec_to_Z b); auto with zarith.
+ assert (F2: [|b|] < base (ZnZ.digits w_op) + [|w4|]); auto with zarith.
+ apply Zlt_le_trans with (base (ZnZ.digits w_op)); auto with zarith.
+ case (ZnZ.spec_to_Z b); auto with zarith.
+ case (ZnZ.spec_to_Z w4); auto with zarith.
+ assert (F3: base (ZnZ.digits w_op) + [|w4|] < [|b|] + [|b|]); auto with zarith.
+ rewrite <- (fun x => Zmod_minus_one (base x + [|w4|])); auto with zarith.
+ rewrite (fun x y => Zmod_small (x - y)); auto with zarith.
+ unfold w_opp;rewrite (ZnZ.spec_opp b).
+ rewrite <- (fun x => Zmod_plus_one (-x)); auto with zarith.
+ rewrite (Zmod_small (- [|b|] + base (ZnZ.digits w_op)));auto with zarith.
+ 2 : assert (HHH := ZnZ.spec_to_Z b);auto with zarith.
+ repeat rewrite Zmod_small; auto with zarith.
+ Qed.
+
+ Lemma _add_mod_spec: forall w1 w2 t1 t2, [|w1|] = t1 mod [|b|] -> [|w2|] = t2 mod [|b|] ->
+     [|_add_mod w1 w2|] = ([|w1|] + [|w2|]) mod [|b|].
+ intros w2 w3 t1 t2 H H1.
+ apply _add_mod_correct; auto with zarith.
+ assert (F: [|w2|] < [|b|]).
+ case (Z_mod_lt t1 [|b|]); auto with zarith.
+ assert (F': [|w3|] < [|b|]).
+ case (Z_mod_lt t2 [|b|]); auto with zarith.
+ assert (tmp: forall x, 2 * x = x + x); auto with zarith.
+ Qed.
+
+ Let _pred_mod x :=
+  match w_compare w0 x with
+  | Eq => bm1
+  | _ => w_pred x
+  end.
+
+ Lemma _pred_mod_spec: forall w t, [|w|] = t mod [|b|] ->
+   [|_pred_mod w|] = ([|w|] - 1) mod [|b|].
+ intros w2 t H; unfold _pred_mod, w_compare, bm1; simpl.
+ assert (F: [|w2|] < [|b|]).
+ case (Z_mod_lt t [|b|]); auto with zarith.
+ rewrite ZnZ.spec_compare; case Zcompare_spec; intros H1;
+ match goal with H: context[w2] |- _ =>
+   generalize H; clear H; intros H1; autorewrite with w_rewrite;
+   auto with zarith
+ end; try rewrite _w0_is_0; try rewrite _w1_is_1; auto with zarith.
+ rewrite <- H1, _w0_is_0; simpl.
+ rewrite <- (Zmod_plus_one (-1)); auto with zarith.
+ repeat rewrite Zmod_small; auto with zarith.
+ case (ZnZ.spec_to_Z b); auto with zarith.
+ unfold w_pred;rewrite ZnZ.spec_pred; auto.
+ assert (HHH := ZnZ.spec_to_Z b);repeat rewrite Zmod_small;auto with
+ zarith.
+ intros;assert (HHH := ZnZ.spec_to_Z w2);auto with zarith.
+ Qed.
+
+ Let _sub_mod x y :=
+  match w_sub_c x y with
+  | C0 z => z
+  | C1 z => w_add z b
+  end.
+
+ Lemma _sub_mod_spec: forall w1 w2 t1 t2, [|w1|] = t1 mod [|b|] -> [|w2|] = t2 mod [|b|] ->
+   [|_sub_mod w1 w2|] = ([|w1|] - [|w2|]) mod [|b|].
+ intros w2 w3 t1 t2; unfold _sub_mod, w_compare, w_sub_c; intros H H1.
+ assert (F: [|w2|] < [|b|]).
+ case (Z_mod_lt t1 [|b|]); auto with zarith.
+ assert (F': [|w3|] < [|b|]).
+ case (Z_mod_lt t2 [|b|]); auto with zarith.
+ match goal with |- context[ZnZ.sub_c ?x ?y] =>
+   generalize (ZnZ.spec_sub_c x y); unfold interp_carry;
+   case (ZnZ.sub_c x y); autorewrite with w_rewrite
+ end; auto with zarith.
+ intros w4 H2.
+ rewrite Zmod_small; auto with zarith.
+ split; auto with zarith.
+ rewrite <- H2; case (ZnZ.spec_to_Z w4); auto with zarith.
+ apply Zle_lt_trans with [|w2|]; auto with zarith.
+ case (ZnZ.spec_to_Z w3); auto with zarith.
+ intros w4 H2; rewrite <- H2.
+ unfold w_add; rewrite ZnZ.spec_add; auto with zarith.
+ case (ZnZ.spec_to_Z w4); intros F1 F2.
+ assert (F3: 0 <= - 1 *  base (ZnZ.digits w_op) + [|w4|] + [|b|]); auto with zarith.
+ rewrite H2.
+ case (ZnZ.spec_to_Z w3); case (ZnZ.spec_to_Z w2); auto with zarith.
+ rewrite <- (fun x => Zmod_minus_one ([|w4|] + x)); auto with zarith.
+ rewrite <- (fun x y => Zmod_plus_one (-y + x)); auto with zarith.
+ repeat rewrite Zmod_small; auto with zarith.
+ case (ZnZ.spec_to_Z b); auto with zarith.
+ Qed.
+
+ Let _mul_mod x y :=
+  let xy := w_mul_c x y in
+  match ww_compare xy wwb with
+  | Lt => snd (split xy)
+  | Eq => w0
+  | Gt => 
+    let xy2n := ww_lsl_n xy in
+    let (h,l) := split xy2n in
+    let (q,r) := w_div21 h l b2n in
+    w_lsr_n r 
+  end.
+
+ Theorem high_zero:forall x, [[x]] < base w_digits -> [|fst (split x)|] = 0.
+  intros x; case x; simpl; auto.
+ intros xh xl H; case (Zle_lt_or_eq 0 [|xh|]); auto with zarith.
+ case (ZnZ.spec_to_Z xh); auto with zarith.
+ intros H1; contradict H; apply Zle_not_lt.
+ assert (HHHH := wB_pos w_digits).
+ unfold w_to_Z.
+ match goal with |- ?X <= ?Y + ?Z =>
+  pattern X at 1; rewrite <- (Zmult_1_l X); auto with zarith;
+  apply Zle_trans with Y; auto with zarith
+ end.
+ case (ZnZ.spec_to_Z xl); auto with zarith.
+ Qed.
+
+ Theorem n_spec: base (ZnZ.digits w_op) / 2 <= 2 ^ [|n|] * [|b|] 
+                        < base (ZnZ.digits w_op).
+ unfold n, w_head0; apply (ZnZ.spec_head0); auto with zarith.
+ Qed. 
+
+ Theorem b2n_spec: [|b2n|] = 2 ^ [|n|] * [|b|].
+ unfold b2n, w_add_mul_div; case n_spec; intros Hp Hp1.
+ assert (F1: [|n|] < Zpos (ZnZ.digits w_op)).
+ case (Zle_or_lt (Zpos (ZnZ.digits w_op)) [|n|]); auto with zarith.
+ intros H1; contradict Hp1; apply Zle_not_lt; unfold base.
+ apply Zle_trans with (2 ^ [|n|] * 1); auto with zarith.
+ rewrite Zmult_1_r; apply Zpower_le_monotone; auto with zarith.
+ rewrite ZnZ.spec_add_mul_div; auto with zarith.
+ rewrite _w0_is_0; rewrite Zdiv_0_l; auto with zarith.
+ rewrite Zplus_0_r; rewrite Zmult_comm; apply Zmod_small; auto with zarith.
+ Qed.
+
+ Theorem ww_lsl_n_spec: forall w, [[w]] < [|b|] * [|b|] ->
+   [[ww_lsl_n w]] = 2 ^ [|n|] * [[w]].
+ intros w2 H; unfold ww_lsl_n.
+ case n_spec; intros Hp Hp1.
+ assert (F0: forall x, 2 * x = x + x); auto with zarith.
+ assert (F1: [|n|] < Zpos (ZnZ.digits w_op)).
+ case (Zle_or_lt (Zpos (ZnZ.digits w_op)) [|n|]); auto.
+ intros H1; contradict Hp1; apply Zle_not_lt; unfold base.
+ apply Zle_trans with (2 ^ [|n|] * 1); auto with zarith.
+ rewrite Zmult_1_r; apply Zpower_le_monotone; auto with zarith.
+ assert (F2: [|n|] < Zpos (xO (ZnZ.digits w_op))).
+ rewrite (Zpos_xO (ZnZ.digits w_op)); rewrite F0; auto with zarith.
+ pattern [|n|]; rewrite <- Zplus_0_r; auto with zarith.
+ apply Zplus_lt_compat; auto with zarith.
+ change 
+  ([[DoubleLift.ww_add_mul_div w0 wWW wW0 w0W 
+              ww_compare w_add_mul_div 
+              ww_sub w_zdigits low (w0W n) w2 W0]] = 2 ^ [|n|] * [[w2]]).
+ rewrite (DoubleLift.spec_ww_add_mul_div ); auto with zarith.
+ 2: apply ZnZ.spec_to_Z; auto.
+ 2: refine (spec_ww_to_Z _ _ _); auto.
+ 2: apply ZnZ.spec_to_Z; auto.
+ 2: apply ZnZ.spec_WW; auto.
+ 2: apply ZnZ.spec_WO; auto.
+ 2: apply ZnZ.spec_OW; auto.
+ 2: refine (spec_ww_compare _ _ _ _ _ _ _); auto.
+ 2: apply ZnZ.spec_to_Z; auto.
+ 2: apply ZnZ.spec_compare; auto.
+ 2: apply ZnZ.spec_add_mul_div; auto.
+ 2: refine (spec_ww_sub _ _ _ _ _ _ _ _ _ _
+                _ _ _ _ _ _ _ _ _ _ _); auto.
+ 2: apply ZnZ.spec_to_Z; auto.
+ 2: apply ZnZ.spec_WW; auto.
+ 2: apply ZnZ.spec_opp_c; auto.
+ 2: apply ZnZ.spec_opp; auto.
+ 2: apply ZnZ.spec_opp_carry; auto.
+ 2: apply ZnZ.spec_sub_c; auto.
+ 2: apply ZnZ.spec_sub; auto.
+ 2: apply ZnZ.spec_sub_carry; auto.
+ 2: apply ZnZ.spec_zdigits; auto.
+ replace ([[w0W n]]) with  [|n|]. 
+ change [[W0]] with 0. rewrite Zdiv_0_l; auto with zarith.
+ rewrite Zplus_0_r; rewrite Zmod_small; auto with zarith.
+ split; auto with zarith.
+ case spec_ww_to_Z with (w_digits := w_digits) (w_to_Z := w_to_Z) (x:=w2); auto with zarith. 
+ apply ZnZ.spec_to_Z; auto.
+ apply Zlt_trans with ([|b|] * [|b|] * 2 ^ [|n|]); auto with zarith.
+ apply Zmult_lt_compat_r; auto with zarith.
+ rewrite <- Zmult_assoc.
+ unfold base; unfold base in Hp.
+ unfold ww_digits,w_digits;rewrite (Zpos_xO (ZnZ.digits w_op)); rewrite F0; auto with zarith.
+ rewrite Zpower_exp; auto with zarith.
+ apply Zmult_lt_compat; auto with zarith.
+ case (ZnZ.spec_to_Z b); auto with zarith.
+ split; auto with zarith.
+ rewrite Zmult_comm; auto with zarith.
+ unfold w_digits;auto with zarith.
+ generalize (ZnZ.spec_OW n).
+ unfold ww_to_Z, w_digits; auto.
+ intros x; case x; simpl.
+ unfold w_to_Z, w_digits, w0; rewrite ZnZ.spec_0; auto.
+ intros w3 w4; rewrite Zplus_comm.
+ rewrite Z_mod_plus; auto with zarith.
+ rewrite Zmod_small; auto with zarith.
+ case (ZnZ.spec_to_Z w4); auto with zarith.
+ unfold base; auto with zarith.  
+ unfold ww_to_Z, w_digits, w_to_Z, w0W; auto.
+ rewrite ZnZ.spec_OW; auto with zarith.
+ Qed.
+
+ Theorem w_lsr_n_spec: forall w, [|w|] < 2 ^ [|n|] *  [|b|]->
+   [|w_lsr_n w|] = [|w|] / 2 ^ [|n|].
+ intros w2 H.
+ case (ZnZ.spec_to_Z w2); intros U1 U2.
+ unfold w_lsr_n, w_add_mul_div.
+ rewrite ZnZ.spec_add_mul_div; auto with zarith.
+ rewrite _w0_is_0; rewrite Zmult_0_l; auto with zarith.
+ rewrite Zplus_0_l.
+ autorewrite with w_rewrite; auto.
+ rewrite (fun x y => Zmod_small (x - y)); auto with zarith.
+ unfold w_zdigits; rewrite ZnZ.spec_zdigits; auto.
+ assert (tmp: forall p q, p - (p - q) = q); intros; try ring;
+  rewrite tmp; clear tmp; auto.
+ rewrite Zmod_small; auto with zarith.
+ split; auto with zarith.
+ apply Zle_lt_trans with (2 := U2); auto with zarith.
+ apply Zdiv_le_upper_bound; auto with zarith.
+ apply Zle_trans with ([|w2|] * (2 ^ 0)); auto with zarith.
+ simpl Zpower; rewrite Zmult_1_r; auto with zarith.
+ apply Zmult_le_compat_l; auto with zarith.
+ apply Zpower_le_monotone; auto with zarith.
+ case (ZnZ.spec_to_Z n); auto with zarith.
+ unfold n.
+ assert (HH: 0 < [|b|]); auto with zarith.
+ split.
+   case (Zle_or_lt [|w_head0 b|] [|w_zdigits|]); auto with zarith.
+   unfold w_zdigits; rewrite ZnZ.spec_zdigits; auto; intros H1.
+   case (ZnZ.spec_head0 b HH); intros _ H2; contradict H2.
+   apply Zle_not_lt; unfold base.
+   apply Zle_trans with (2^[|ZnZ.head0 b|] * 1); auto with zarith.
+   rewrite Zmult_1_r; apply Zpower_le_monotone; auto with zarith.
+ unfold w_zdigits; rewrite ZnZ.spec_zdigits; auto.
+ apply Zle_lt_trans with (Zpos (ZnZ.digits w_op)); auto with zarith.
+    case (ZnZ.spec_to_Z (w_head0 b)); auto with zarith.
+ unfold base; apply Zpower2_lt_lin; auto with zarith.
+ autorewrite with w_rewrite; auto.
+ rewrite Zmod_small; auto with zarith.
+ unfold w_zdigits; rewrite ZnZ.spec_zdigits; auto with zarith.
+ case (ZnZ.spec_to_Z n); auto with zarith.
+ unfold w_zdigits; rewrite ZnZ.spec_zdigits; auto.
+ split; auto with zarith.
+ case (Zle_or_lt [|n|] (Zpos (ZnZ.digits w_op))); auto with zarith; intros H1.
+ case (ZnZ.spec_head0 b); auto with zarith; intros _ H2.
+ contradict H2; apply Zle_not_lt; auto with zarith.
+ unfold base; apply Zle_trans with (2 ^ [|ZnZ.head0 b|] * 1);
+   auto with zarith.
+ rewrite Zmult_1_r; unfold base; apply Zpower_le_monotone; auto with zarith.
+ apply Zle_lt_trans with (Zpos (ZnZ.digits w_op)); auto with zarith.
+ case (ZnZ.spec_to_Z n); auto with zarith.
+ unfold base; apply Zpower2_lt_lin; auto with zarith.
+ Qed.
+
+ Lemma split_correct: forall x, let (xh, xl) := split x in [[WW xh xl]] = [[x]].
+ intros x; case x; simpl; unfold w0, w_to_Z;try rewrite ZnZ.spec_0; auto with zarith.
+ Qed. 
+
+ Lemma _mul_mod_spec: forall w1 w2 t1 t2, [|w1|] = t1 mod [|b|] -> [|w2|] = t2 mod [|b|] ->
+   [|_mul_mod w1 w2|] = ([|w1|] * [|w2|]) mod [|b|].
+ intros w2 w3 t1 t2 H H1; unfold _mul_mod, wwb.
+ assert (F: [|w2|] < [|b|]).
+ case (Z_mod_lt t1 [|b|]); auto with zarith.
+ assert (F': [|w3|] < [|b|]).
+ case (Z_mod_lt t2 [|b|]); auto with zarith.
+ match goal with |- context[ww_compare ?x ?y] =>
+   change (ww_compare x y) with (DoubleBase.ww_compare w0 w_compare x y)
+ end.
+ rewrite (@spec_ww_compare w w0 w_digits w_to_Z w_compare
+    ZnZ.spec_0 ZnZ.spec_to_Z ZnZ.spec_compare 
+    (w_mul_c w2 w3) (WW w0 b)); case Zcompare_spec; intros H2;
+ match goal with H: context[w_mul_c] |- _ =>
+   generalize H; clear H
+ end; try rewrite _w0_is_0; try rewrite !_w1_is_1; auto with zarith.
+ unfold w_mul_c, ww_to_Z, w_to_Z, w_digits; rewrite ZnZ.spec_mul_c; auto with zarith.
+ simpl; rewrite _w0_is_0, Zmult_0_l, Zplus_0_l.
+ intros H2; rewrite H2; simpl.
+ rewrite Z_mod_same; auto with zarith.
+ generalize (high_zero (w_mul_c w2 w3)).
+ unfold w_mul_c; generalize (ZnZ.spec_mul_c w2 w3); 
+  case (ZnZ.mul_c w2 w3); simpl; auto with zarith.
+ intros H3 _  _; rewrite <- H3; autorewrite with w_rewrite; auto.
+(*  rewrite Zmod_small; auto with zarith. *)
+ intros w4 w5.
+ change (w_to_Z w0) with [|w0|]; rewrite _w0_is_0.
+ change (w_to_Z w4) with [|w4|].
+ change (w_to_Z w5) with [|w5|].
+ simpl.
+ intros H2 H3 H4.
+ assert (E1: [|w4|] = 0).
+ apply H3; auto with zarith.
+ apply Zlt_trans with (1 := H4).
+ case (ZnZ.spec_to_Z b); auto with zarith.
+ generalize H4 H2; rewrite E1; rewrite Zmult_0_l; rewrite Zplus_0_l;
+   clear H4 H2; intros H4 H2.
+ rewrite <- H2; rewrite Zmod_small; auto with zarith.
+ case (ZnZ.spec_to_Z w5); auto with zarith.
+ intros H2.
+ match goal with |- context[split ?x] =>
+ generalize (split_correct x); 
+  case (split x); auto with zarith
+ end.
+ assert (F1: [[w_mul_c w2 w3]] < [|b|] * [|b|]).
+ unfold w_to_Z, w_mul_c, ww_to_Z,w_digits;
+   rewrite ZnZ.spec_mul_c; auto with zarith.
+ apply Zmult_lt_compat; auto with zarith.
+ case (ZnZ.spec_to_Z w2); auto with zarith.
+ case (ZnZ.spec_to_Z w3); auto with zarith.
+ intros w4 w5; rewrite ww_lsl_n_spec; auto with zarith.
+ intros H3.
+ unfold w_div21; match goal with |- context[ZnZ.div21 ?y ?z ?t] =>
+   generalize (ZnZ.spec_div21 y z t);
+   case (ZnZ.div21 y z t)
+ end.
+ rewrite b2n_spec; case (n_spec); auto.
+ intros H4 H5 w6 w7 H6.
+ case H6; auto with zarith.
+ case (Zle_or_lt (2 ^ [|n|] * [|b|]) [|w4|]); auto; intros H7.
+ match type of H3 with ?X = ?Y =>
+    absurd (Y < X)
+ end.
+ apply Zle_not_lt; rewrite H3; auto with zarith.
+ simpl ww_to_Z.
+ match goal with |- ?X < ?Y + _ =>
+    apply Zlt_le_trans with Y; auto with zarith
+ end.
+ apply Zlt_trans with (2 ^ [|n|] * ([|b|] * [|b|])); 
+   auto with zarith.
+ apply Zmult_lt_compat_l; auto with zarith.
+ rewrite Zmult_assoc.
+ apply Zmult_lt_compat2; auto with zarith.
+ case (ZnZ.spec_to_Z b); auto with zarith.
+ case (ZnZ.spec_to_Z w5); unfold w_to_Z;auto with zarith.
+ clear H6; intros H7 H8.
+ rewrite w_lsr_n_spec; auto with zarith.
+ rewrite <- (Z_div_mult ([|w2|] * [|w3|]) (2 ^ [|n|]));
+  auto with zarith; rewrite Zmult_comm.
+ rewrite <- ZnZ.spec_mul_c; auto with zarith.
+ unfold w_mul_c in H3; unfold ww_to_Z in H3;simpl H3.
+ unfold w_digits,w_to_Z in H3. rewrite <- H3; simpl.
+ rewrite H7; rewrite (fun x => Zmult_comm (2 ^ x));
+   rewrite Zmult_assoc; rewrite  BigNumPrelude.Z_div_plus_l; auto with zarith.
+ rewrite Zplus_mod; auto with zarith.
+ rewrite Z_mod_mult; auto with zarith.
+ rewrite Zplus_0_l; auto with zarith.
+ rewrite Zmod_mod; auto with zarith.
+ rewrite Zmod_small; auto with zarith.
+ split; auto with zarith.
+ apply Zdiv_lt_upper_bound; auto with zarith.
+ rewrite Zmult_comm; auto with zarith.
+ Qed.
+
+ Let _square_mod x :=
+  let x2 := w_square_c x in
+  match ww_compare x2 wwb with
+  | Lt => snd (split x2)
+  | Eq => w0
+  | Gt =>
+    let x2_2n := ww_lsl_n x2 in
+    let (h,l) := split x2_2n in
+    let (q,r) := w_div21 h l b2n in
+    w_lsr_n r
+  end.
+
+ Lemma _square_mod_spec: forall w t, [|w|] = t mod [|b|] ->
+    [|_square_mod w|] = ([|w|] * [|w|]) mod [|b|].
+ intros w2 t2 H; unfold _square_mod, wwb.
+ assert (F: [|w2|] < [|b|]).
+ case (Z_mod_lt t2 [|b|]); auto with zarith.
+ match goal with |- context[ww_compare ?x ?y] =>
+   change (ww_compare x y) with (DoubleBase.ww_compare w0 w_compare x y)
+ end.
+ rewrite (@spec_ww_compare w w0 w_digits w_to_Z w_compare
+    ZnZ.spec_0 ZnZ.spec_to_Z ZnZ.spec_compare); case Zcompare_spec;
+   intros H2;
+ match goal with H: context[w_square_c] |- _ =>
+   generalize H; clear H
+ end; autorewrite with w_rewrite; try rewrite _w0_is_0; try rewrite !_w1_is_1; auto with zarith.
+ unfold w_square_c, ww_to_Z, w_to_Z, w_digits; rewrite ZnZ.spec_square_c; auto with zarith.
+ intros H2;rewrite H2; simpl.
+ rewrite _w0_is_0; simpl.
+ rewrite Z_mod_same; auto with zarith.
+ generalize (high_zero (w_square_c w2)).
+ unfold w_square_c; generalize (ZnZ.spec_square_c w2); 
+  case (ZnZ.square_c w2); simpl; auto with zarith.
+ intros H3 _  _; rewrite <- H3; autorewrite with w_rewrite; auto.
+ intros w4 w5.
+ change (w_to_Z w0) with [|w0|]; rewrite _w0_is_0; simpl.
+ change (w_to_Z w4) with [|w4|].
+ change (w_to_Z w5) with [|w5|].
+ intros H2 H3 H4.
+ assert (E1: [|w4|] = 0).
+ apply H3; auto with zarith.
+ apply Zlt_trans with (1 := H4).
+ case (ZnZ.spec_to_Z b); auto with zarith.
+ generalize H4 H2; rewrite E1; rewrite Zmult_0_l; rewrite Zplus_0_l;
+   clear H4 H2; intros H4 H2.
+ rewrite <- H2; rewrite Zmod_small; auto with zarith.
+ case (ZnZ.spec_to_Z w5); auto with zarith.
+ intros H2.
+ match goal with |- context[split ?x] =>
+ generalize (split_correct x); 
+  case (split x); auto with zarith
+ end.
+ assert (F1: [[w_square_c w2]] < [|b|] * [|b|]).
+ unfold w_square_c, ww_to_Z, w_digits, w_to_Z.
+ rewrite ZnZ.spec_square_c; auto with zarith.
+ apply Zmult_lt_compat; auto with zarith.
+ case (ZnZ.spec_to_Z w2); auto with zarith.
+ case (ZnZ.spec_to_Z w2); auto with zarith.
+ intros w4 w5; rewrite ww_lsl_n_spec; auto with zarith.
+ intros H3.
+ unfold w_div21; match goal with |- context[ZnZ.div21 ?y ?z ?t] =>
+   generalize (ZnZ.spec_div21 y z t);
+   case (ZnZ.div21 y z t)
+ end.
+ rewrite b2n_spec; case (n_spec); auto.
+ intros H4 H5 w6 w7 H6.
+ case H6; auto with zarith.
+ case (Zle_or_lt (2 ^ [|n|] * [|b|]) [|w4|]); auto; intros H7.
+ match type of H3 with ?X = ?Y =>
+    absurd (Y < X)
+ end.
+ apply Zle_not_lt; rewrite H3; auto with zarith.
+ simpl ww_to_Z.
+ match goal with |- ?X < ?Y + _ =>
+    apply Zlt_le_trans with Y; auto with zarith
+ end.
+ apply Zlt_trans with (2 ^ [|n|] * ([|b|] * [|b|])); 
+   auto with zarith.
+ apply Zmult_lt_compat_l; auto with zarith.
+ rewrite Zmult_assoc.
+ apply Zmult_lt_compat2; auto with zarith.
+ case (ZnZ.spec_to_Z b); auto with zarith.
+ unfold w_to_Z,w_digits;case (ZnZ.spec_to_Z w5); auto with zarith.
+ clear H6; intros H7 H8.
+ rewrite w_lsr_n_spec; auto with zarith.
+ rewrite <- (Z_div_mult ([|w2|] * [|w2|]) (2 ^ [|n|]));
+  auto with zarith; rewrite Zmult_comm.
+ rewrite <- ZnZ.spec_square_c; auto with zarith.
+ unfold w_square_c, ww_to_Z in H3;  unfold w_digits,w_to_Z in H3.
+ rewrite <- H3; simpl.
+ rewrite H7; rewrite (fun x => Zmult_comm (2 ^ x));
+   rewrite Zmult_assoc; rewrite BigNumPrelude.Z_div_plus_l; auto with zarith.
+ rewrite Zplus_mod; auto with zarith.
+ rewrite Z_mod_mult; auto with zarith.
+ rewrite Zplus_0_l; auto with zarith.
+ rewrite Zmod_mod; auto with zarith.
+ rewrite Zmod_small; auto with zarith.
+ split; auto with zarith.
+ apply Zdiv_lt_upper_bound; auto with zarith.
+ rewrite Zmult_comm; auto with zarith.
+ Qed.
+
+ Let _power_mod :=
+   fix pow_mod (x:w) (p:positive) {struct p} : w :=
+     match p with
+     | xH => x
+     | xO p' =>
+       let pow := pow_mod x p' in
+       _square_mod pow
+     | xI p' =>
+       let pow := pow_mod x p' in
+       _mul_mod (_square_mod pow) x
+     end.
+
+ Lemma _power_mod_spec: forall w t p, [|w|] = t mod [|b|] ->
+   [|_power_mod w p|] = (Zpower_pos [|w|] p) mod [|b|].
+ intros w2 t p; elim p; simpl; auto with zarith.
+ intros p' Rec H. 
+ assert (F: [|w2|] < [|b|]).
+ case (Z_mod_lt t [|b|]); auto with zarith.
+ replace (xI p') with (p' + p' + 1)%positive.
+ repeat rewrite Zpower_pos_is_exp; auto with zarith.
+ pose (t1 := [|_power_mod w2 p'|]).
+ rewrite _mul_mod_spec with (t1 := t1 * t1)
+                            (t2 := t); auto with zarith.
+ rewrite _square_mod_spec with (t := Zpower_pos [|w2|] p'); auto with zarith.
+ rewrite Rec; auto with zarith.
+ assert (tmp: forall p, Zpower_pos p 1 = p); try (rewrite tmp; clear tmp).
+ intros p1; unfold Zpower_pos; simpl; ring.
+ rewrite <- Zmult_mod; auto with zarith.
+ rewrite Zmult_mod; auto with zarith.
+ rewrite Zmod_mod; auto with zarith.
+ rewrite <- Zmult_mod; auto with zarith.
+ simpl; unfold t1; apply _square_mod_spec with (t := Zpower_pos [|w2|] p'); auto with zarith.
+ rewrite xI_succ_xO; rewrite <- Pplus_diag.
+ rewrite Pplus_one_succ_r; auto.
+ intros p' Rec H. 
+ replace (xO p') with (p' + p')%positive.
+ repeat rewrite Zpower_pos_is_exp; auto with zarith.
+ rewrite _square_mod_spec with (t := Zpower_pos [|w2|] p'); auto with zarith.
+ rewrite Rec; auto with zarith.
+ rewrite <- Zmult_mod; auto with zarith.
+ rewrite <- Pplus_diag; auto.
+ intros H.
+ assert (tmp: forall p, Zpower_pos p 1 = p); try (rewrite tmp; clear tmp).
+ intros p1; unfold Zpower_pos; simpl; ring.
+ rewrite Zmod_small; auto with zarith.
+ assert (F: [|w2|] < [|b|]).
+ case (Z_mod_lt t [|b|]); auto with zarith.
+ case (ZnZ.spec_to_Z w2); auto with zarith.
+ Qed.
+
+ Definition make_mod_op := 
+   mk_mod_op
+     _succ_mod _add_mod 
+     _pred_mod _sub_mod
+     _mul_mod _square_mod _power_mod.
+
+  Definition make_mod_spec: mod_spec make_mod_op.
+  apply mk_mod_spec.
+  exact _succ_mod_spec.
+  exact _add_mod_spec.
+  exact _pred_mod_spec.
+  exact _sub_mod_spec.
+  exact _mul_mod_spec.
+  exact _square_mod_spec.
+  exact _power_mod_spec.
+  Defined.
+
+(*********** Mersenne special **********)
+  
+ Variable p: positive.
+ Variable zp: w.
+
+ Hypothesis zp_b: [|zp|] = Zpos p.
+ Hypothesis p_lt_w_digits: Zpos p <= Zpos w_digits.
+
+ Let p1 := Pminus (xO w_digits) p.
+
+ Theorem p_p1: Zpos p + Zpos p1 = Zpos (xO w_digits).
+ unfold p1.
+ rewrite Zpos_minus; auto with zarith.
+ rewrite Zmax_right; auto with zarith.
+ rewrite Zpos_xO; auto with zarith.
+ assert (0 < Zpos w_digits); auto with zarith.
+ Qed.
+
+ Let zp1 := ww_sub ww_zdigits (WW w0 zp).
+
+ Let spec_add2: forall x y,
+  [[w_add2 x y]] = [|x|] + [|y|].
+  unfold w_add2.
+  intros xh xl; generalize (ZnZ.spec_add_c xh xl).
+  unfold w_add_c; case ZnZ.add_c; unfold interp_carry; simpl ww_to_Z.
+    intros w2 Hw2; simpl; unfold w_to_Z; rewrite Hw2.
+  unfold w0; rewrite ZnZ.spec_0; simpl; auto with zarith.
+  intros w2; rewrite Zmult_1_l; simpl.
+  unfold w_to_Z, w1; rewrite ZnZ.spec_1; auto with zarith.
+  rewrite Zmult_1_l; auto.
+ Qed.
+
+ Let spec_ww_digits:
+  [[ww_zdigits]] = Zpos (xO w_digits).
+ Proof.
+ unfold w_to_Z, ww_zdigits.
+ rewrite spec_add2.
+ unfold w_to_Z, w_zdigits, w_digits.
+ rewrite ZnZ.spec_zdigits; auto.
+ rewrite Zpos_xO; auto with zarith.
+ Qed.
+
+ Let spec_ww_to_Z := (spec_ww_to_Z _ _ ZnZ.spec_to_Z).
+ Let spec_ww_compare := spec_ww_compare _ _ _ _ ZnZ.spec_0  
+      ZnZ.spec_to_Z ZnZ.spec_compare.
+ Let spec_ww_sub := 
+         spec_ww_sub w0 zp wWW zp1 w_opp_c w_opp_carry
+              w_sub_c w_opp w_sub w_sub_carry w_digits w_to_Z
+             ZnZ.spec_0
+             ZnZ.spec_to_Z
+             ZnZ.spec_WW
+             ZnZ.spec_opp_c
+             ZnZ.spec_opp
+             ZnZ.spec_opp_carry
+             ZnZ.spec_sub_c
+             ZnZ.spec_sub
+             ZnZ.spec_sub_carry.
+
+ Theorem zp1_b: [[zp1]] = Zpos p1.
+ change ([[DoubleSub.ww_sub w0 wWW w_opp_c w_opp_carry w_sub_c w_opp w_sub
+            w_sub_carry ww_zdigits (WW w0 zp)]] =
+          Zpos p1).
+ rewrite spec_ww_sub; auto with zarith.
+ rewrite spec_ww_digits; simpl ww_to_Z.
+ change (w_to_Z w0) with [|w0|].
+ unfold w0; rewrite ZnZ.spec_0; autorewrite with rm10; auto.
+ change (w_to_Z zp) with [|zp|].
+ rewrite zp_b.
+ rewrite Zmod_small; auto with zarith.
+ rewrite <- p_p1; auto with zarith.
+ unfold ww_digits; split; auto with zarith.
+ rewrite <- p_p1; auto with zarith.
+ assert (0 < Zpos p1); auto with zarith.
+ apply Zle_lt_trans with (Zpos (xO w_digits)); auto with zarith.
+ assert (0 < Zpos p); auto with zarith.
+ unfold base; apply Zpower2_lt_lin; auto with zarith.
+ Qed.
+
+ Hypothesis p_b: [|b|] = 2 ^ (Zpos p) - 1.
+
+
+ Let w_pos_mod := ZnZ.pos_mod.
+
+ Let add_mul_div := 
+   DoubleLift.ww_add_mul_div w0 wWW wW0 w0W 
+              ww_compare w_add_mul_div 
+              ww_sub w_zdigits low. 
+
+ Let _mmul_mod x y :=
+  let xy := w_mul_c x y in
+  match xy with
+    W0 => w0
+  | WW xh xl =>
+      let xl1 := w_pos_mod zp xl in
+        match add_mul_div zp1 W0 xy with
+          W0 => match w_compare xl1 b with
+                | Lt => xl1
+                | Eq => w0
+                | Gt => w1
+                end
+        | WW _ xl2 => _add_mod xl1 xl2
+        end
+  end.
+
+ Hint Unfold w_digits.
+
+ Lemma WW_0: forall x y, [[WW x y]] = 0 -> [|x|] = 0 /\ [|y|] =0.
+ intros x y; simpl; case (ZnZ.spec_to_Z x); intros H1 H2;
+   case (ZnZ.spec_to_Z y); intros H3 H4 H5.
+ case Zle_lt_or_eq with (1 := H1); clear H1; intros H1; auto with zarith.
+ absurd (0 < [|x|] * base (ZnZ.digits w_op) + [|y|]); auto with zarith.
+ unfold w_to_Z, w_digits in H5;auto with zarith.
+ match goal with |- _ < ?X + _ =>
+  apply Zlt_le_trans with X; auto with zarith
+ end.
+ case Zle_lt_or_eq with (1 := H3); clear H3; intros H3; auto with zarith.
+ absurd (0 < [|x|] * base (ZnZ.digits w_op) + [|y|]); auto with zarith.
+ unfold w_to_Z, w_digits in H5;auto with zarith.
+ rewrite <- H1; rewrite Zmult_0_l; auto with zarith.
+ Qed.
+
+ Theorem WW0_is_0: [[W0]] = 0.
+ simpl; auto.
+ Qed.
+  Hint Rewrite WW0_is_0: w_rewrite.
+
+ Theorem mmul_aux0: Zpos (xO w_digits) - Zpos p1 = Zpos p.
+ unfold w_digits.
+ apply trans_equal with (Zpos p + Zpos p1 - Zpos p1); auto with zarith.
+ rewrite p_p1; auto with zarith.
+ Qed.
+
+ Theorem mmul_aux1: 2 ^ Zpos w_digits = 
+     2 ^ (Zpos w_digits - Zpos p) * 2 ^ Zpos p.
+ rewrite <- Zpower_exp; auto with zarith.
+ eq_tac; auto with zarith.
+ Qed.
+
+ Theorem mmul_aux2:forall x,
+   x mod (2 ^ Zpos p - 1) = 
+    ((x / 2 ^ Zpos p) + (x mod 2 ^ Zpos p)) mod (2 ^ Zpos p - 1).
+ intros x; pattern x at 1; rewrite Z_div_mod_eq with (b := 2 ^ Zpos p); auto with zarith.
+ match goal with |- (?X * ?Y + ?Z) mod (?X - 1) = ?T =>
+  replace (X * Y + Z) with (Y * (X - 1) + (Y + Z)); try ring
+ end.
+ rewrite Zplus_mod; auto with zarith.
+ rewrite Z_mod_mult; auto with zarith.
+ rewrite Zplus_0_l.
+ rewrite Zmod_mod; auto with zarith.
+ Qed.
+
+ Theorem mmul_aux3:forall xh xl,
+   [[WW xh xl]] mod (2 ^ Zpos p) = [|xl|] mod (2 ^ Zpos p).
+ intros xh xl; simpl ww_to_Z; unfold base.
+ rewrite Zplus_mod; auto with zarith.
+ generalize mmul_aux1; unfold w_digits; intros tmp; rewrite tmp;
+   clear tmp. 
+ rewrite Zmult_assoc.
+ rewrite Z_mod_mult; auto with zarith.
+ rewrite Zplus_0_l; apply Zmod_mod; auto with zarith.
+ Qed.
+
+ Let spec_low: forall x,
+  [|low x|] = [[x]] mod base w_digits.
+  intros x; case x; simpl low; auto with zarith.
+  intros xh xl; simpl.
+  rewrite Zplus_comm; rewrite Z_mod_plus; auto with zarith.
+  rewrite Zmod_small; auto with zarith.
+  case (ZnZ.spec_to_Z xl); auto with zarith.
+  unfold base; auto with zarith.
+ Qed.
+
+ Theorem mmul_aux4:forall x,
+  [[x]] < [|b|] * 2 ^  Zpos p ->
+     match add_mul_div zp1 W0 x with
+          W0 => 0
+        | WW _ xl2 => [|xl2|]
+     end = [[x]] / 2 ^ Zpos p.
+ intros x Hx.
+ assert (Hp: [[zp1]] <= Zpos (xO w_digits)); auto with zarith.
+   rewrite zp1_b; rewrite <- p_p1; auto with zarith.
+   assert (0 <= Zpos p); auto with zarith.
+ generalize (@DoubleLift.spec_ww_add_mul_div w w0 wWW wW0 w0W
+    ww_compare w_add_mul_div ww_sub w_digits w_zdigits low w_to_Z
+    ZnZ.spec_0 ZnZ.spec_to_Z spec_ww_to_Z
+    ZnZ.spec_WW ZnZ.spec_WO ZnZ.spec_OW
+    spec_ww_compare ZnZ.spec_add_mul_div spec_ww_sub
+    ZnZ.spec_zdigits spec_low W0 x zp1 Hp).
+  unfold add_mul_div; 
+    case DoubleLift.ww_add_mul_div; autorewrite with w_rewrite; auto.
+ rewrite Zmult_0_l; rewrite Zplus_0_l.
+ rewrite zp1_b.
+ generalize mmul_aux0; unfold w_digits; intros tmp; rewrite tmp.
+ rewrite Zmod_small; auto with zarith.
+ split; auto with zarith.
+ apply Z_div_pos; auto with zarith.
+ case (spec_ww_to_Z x); auto with zarith.
+ unfold base.
+ apply Zdiv_lt_upper_bound; auto with zarith.
+ rewrite <- Zpower_exp; auto with zarith.
+ apply Zlt_le_trans with (base (ww_digits (ZnZ.digits w_op))); auto with zarith.
+   case (spec_ww_to_Z x); auto with zarith.
+ unfold base; apply Zpower_le_monotone; auto with zarith.
+ split; auto with zarith.
+ assert (0 < Zpos p); auto with zarith.
+ intros w2 w3; rewrite Zmult_0_l; rewrite Zplus_0_l.
+ rewrite zp1_b.
+ generalize mmul_aux0; unfold w_digits; intros tmp; rewrite tmp;
+  clear tmp.
+ simpl ww_to_Z; rewrite Zmod_small; auto with zarith.
+ intros H1; 
+   generalize (high_zero (WW w2 w3)); unfold w_digits;intros tmp;
+   simpl fst in tmp; simpl ww_to_Z in tmp;auto with zarith.
+   unfold w_to_Z in *.
+   rewrite tmp in H1; auto with zarith. clear tmp.
+ simpl ww_to_Z; rewrite H1; apply Zdiv_lt_upper_bound; auto with zarith.
+ unfold base; rewrite <- Zpower_exp; auto with zarith.
+ apply Zlt_le_trans with (1 := Hx).
+ apply Zle_trans with (2 ^ Zpos p * 2 ^ Zpos p).
+ rewrite p_b; apply Zmult_le_compat_r; auto with zarith.
+ rewrite <- Zpower_exp; auto with zarith.
+ apply Zpower_le_monotone; auto with zarith.
+ split; auto with zarith.
+ apply Z_div_pos; auto with zarith.
+ case (spec_ww_to_Z  x); auto with zarith.
+ unfold base.
+ apply Zdiv_lt_upper_bound; auto with zarith.
+ rewrite <- Zpower_exp; auto with zarith.
+ apply Zlt_le_trans with (base (ww_digits (ZnZ.digits w_op))); auto with zarith.
+   case (spec_ww_to_Z x); auto with zarith.
+ unfold base; apply Zpower_le_monotone; auto with zarith.
+ split; auto with zarith.
+ assert (0 < Zpos p); auto with zarith.
+ Qed.
+
+ Theorem mmul_aux5:forall xh xl, 
+      [[WW xh xl]] < [|b|] * 2 ^  Zpos p ->
+      let xl1 := w_pos_mod zp xl in
+      let r := 
+        match add_mul_div zp1 W0 (WW xh xl) with
+          W0 => match w_compare xl1 b with
+                | Lt => xl1
+                | Eq => w0
+                | Gt => w1
+                end
+        | WW _ xl2 => _add_mod xl1 xl2
+        end  in
+        [|r|] = [[WW xh xl]] mod [|b|].
+ intros xh xl Hx xl1 r; unfold r; clear r.
+ generalize (mmul_aux4 _ Hx).
+ simpl ww_to_Z; rewrite p_b.
+ rewrite mmul_aux2.
+ assert (Hp: [[zp1]] <= Zpos (xO w_digits)); auto with zarith.
+   rewrite zp1_b; rewrite <- p_p1; auto with zarith.
+   assert (0 <= Zpos p); auto with zarith.
+ generalize (@DoubleLift.spec_ww_add_mul_div w w0 wWW wW0 w0W
+    ww_compare w_add_mul_div ww_sub w_digits w_zdigits low w_to_Z
+    ZnZ.spec_0 ZnZ.spec_to_Z spec_ww_to_Z
+    ZnZ.spec_WW ZnZ.spec_WO ZnZ.spec_OW
+    spec_ww_compare ZnZ.spec_add_mul_div spec_ww_sub
+    ZnZ.spec_zdigits spec_low W0 (WW xh xl) zp1 Hp).
+  unfold add_mul_div; 
+    case DoubleLift.ww_add_mul_div; autorewrite with w_rewrite; auto.
+ rewrite Zmult_0_l; rewrite Zplus_0_l.
+ rewrite zp1_b.
+ generalize mmul_aux0; unfold w_digits; intros tmp; rewrite tmp; clear tmp.
+ intros H1 H2.
+ rewrite <- H2.
+ rewrite Zplus_0_l.
+ generalize mmul_aux3; simpl ww_to_Z; intros tmp; rewrite tmp; clear tmp;
+   auto with zarith.
+ unfold xl1; unfold w_pos_mod.
+  rewrite <- p_b; rewrite <- zp_b. 
+  rewrite <- ZnZ.spec_pos_mod; auto with zarith.
+ unfold w_compare; rewrite ZnZ.spec_compare;
+   case Zcompare_spec; intros Hc;
+ match goal with H: context[b] |- _ =>
+   generalize H; clear H
+ end; try rewrite _w0_is_0.
+ intros H3; rewrite H3.
+ rewrite Z_mod_same; auto with zarith.
+ intros H3; rewrite Zmod_small; auto with zarith.
+ case (ZnZ.spec_to_Z (ZnZ.pos_mod zp xl)); unfold w_to_Z; auto with zarith.
+ rewrite p_b; rewrite ZnZ.spec_pos_mod; auto with zarith.
+ intros H3; assert (HH: [|xl|] mod 2 ^ Zpos p = 2 ^ Zpos p).
+ apply Zle_antisym; auto with zarith.
+ case (Z_mod_lt ([|xl|]) (2 ^ Zpos p)); auto with zarith.
+ rewrite zp_b in H3; auto with zarith.
+ rewrite zp_b; rewrite HH.
+ rewrite <- Zmod_minus_one; auto with zarith.
+ rewrite _w1_is_1; rewrite Zmod_small; auto with zarith.
+ rewrite Zmult_0_l; rewrite Zplus_0_l.
+ rewrite zp1_b.
+ generalize mmul_aux0; unfold w_digits; intros tmp; rewrite tmp; clear tmp.
+ intros w2 w3 H1 H2; rewrite <- H2.
+ generalize mmul_aux3; simpl ww_to_Z; intros tmp; rewrite tmp; clear tmp;
+   auto with zarith.
+ rewrite <- p_b; rewrite <- zp_b. 
+ rewrite <- ZnZ.spec_pos_mod; auto with zarith.
+ unfold xl1; unfold w_pos_mod.
+ rewrite Zplus_comm.
+ apply _add_mod_correct; auto with zarith.
+ assert (tmp: forall x, 2 * x = x + x); auto with zarith;
+   rewrite tmp; apply Zplus_le_lt_compat; clear tmp; auto with zarith.
+ rewrite ZnZ.spec_pos_mod; auto with zarith.
+ rewrite p_b; case (Z_mod_lt [|xl|] (2 ^ Zpos p)); auto with zarith.
+ rewrite zp_b; auto with zarith.
+ rewrite H2; apply Zdiv_lt_upper_bound; auto with zarith.
+ Qed.
+
+ Lemma _mmul_mod_spec: forall w1 w2 t1 t2, [|w1|] = t1 mod [|b|] -> [|w2|] = t2 mod [|b|] ->
+   [|_mmul_mod w1 w2|] = ([|w1|] * [|w2|]) mod [|b|].
+ intros w2 w3 t1 t2; unfold _mmul_mod, w_mul_c; intros H H1.
+ assert (F: [|w2|] < [|b|]).
+ case (Z_mod_lt t1 [|b|]); auto with zarith.
+ assert (F': [|w3|] < [|b|]).
+ case (Z_mod_lt t2 [|b|]); auto with zarith.
+ match goal with |- context[ZnZ.mul_c ?x ?y] =>
+   generalize (ZnZ.spec_mul_c x y); unfold interp_carry;
+   case (ZnZ.mul_c x y); autorewrite with w_rewrite
+ end; auto with zarith.
+ simpl; intros H2; rewrite <- H2; rewrite Zmod_small;
+  auto with zarith.
+ intros w4 w5 H2.
+ rewrite mmul_aux5; auto with zarith.
+ rewrite <- H2; auto.
+ unfold ww_to_Z,w_digits,w_to_Z; rewrite H2.
+ apply Zmult_lt_compat; auto with zarith.
+ case (ZnZ.spec_to_Z w2); auto with zarith.
+ case (ZnZ.spec_to_Z w3); auto with zarith.
+ Qed.
+
+ Let _msquare_mod x :=
+  let xy := w_square_c x in
+  match xy with
+    W0 => w0
+  | WW xh xl =>
+      let xl1 := w_pos_mod zp xl in
+        match add_mul_div zp1 W0 xy with
+          W0 =>  match w_compare xl1 b with
+                | Lt => xl1
+                | Eq => w0
+                | Gt => w1
+                end         
+        | WW _ xl2 => _add_mod xl1 xl2
+        end
+  end.
+
+ Lemma _msquare_mod_spec: forall w1 t1, [|w1|] = t1 mod [|b|] -> 
+   [|_msquare_mod w1|] = ([|w1|] * [|w1|]) mod [|b|].
+ intros w2 t2; unfold _msquare_mod, w_square_c; intros H.
+ assert (F: [|w2|] < [|b|]).
+ case (Z_mod_lt t2 [|b|]); auto with zarith.
+ match goal with |- context[ZnZ.square_c ?x] =>
+   generalize (ZnZ.spec_square_c x); unfold interp_carry;
+   case (ZnZ.square_c x); autorewrite with w_rewrite
+ end; auto with zarith.
+ simpl; intros H2; rewrite <- H2; rewrite Zmod_small;
+  auto with zarith.
+ intros w4 w5 H2.
+ rewrite mmul_aux5; auto with zarith.
+ unfold ww_to_Z, w_to_Z ,w_digits; rewrite <- H2; auto.
+ unfold ww_to_Z,w_to_Z ,w_digits; rewrite H2.
+ apply Zmult_lt_compat; auto with zarith.
+ case (ZnZ.spec_to_Z w2); auto with zarith.
+ case (ZnZ.spec_to_Z w2); auto with zarith.
+ Qed.
+
+ Definition mmake_mod_op := 
+   mk_mod_op
+     _succ_mod _add_mod 
+     _pred_mod _sub_mod
+     _mmul_mod _msquare_mod _power_mod.
+
+ Definition mmake_mod_spec: mod_spec mmake_mod_op.
+  apply mk_mod_spec.
+  exact _succ_mod_spec.
+  exact _add_mod_spec.
+  exact _pred_mod_spec.
+  exact _sub_mod_spec.
+  exact _mmul_mod_spec.
+  exact _msquare_mod_spec.
+  exact _power_mod_spec.
+  Defined.
+ 
+End Mod_op.
+    
diff --git a/coqprime/num/NEll.v b/coqprime/num/NEll.v
new file mode 100644
index 000000000..28dd63181
--- /dev/null
+++ b/coqprime/num/NEll.v
@@ -0,0 +1,983 @@
+
+(*************************************************************)
+(*      This file is distributed under the terms of the      *)
+(*      GNU Lesser General Public License Version 2.1        *)
+(*************************************************************)
+(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
+(*************************************************************)
+
+
+Require Import ZArith Znumtheory Zpow_facts.
+Require Import CyclicAxioms DoubleCyclic BigN Cyclic31 Int31.
+Require Import W.
+Require Import Mod_op.
+Require Import ZEll.
+Require Import Bits.
+Import CyclicAxioms DoubleType DoubleBase.
+
+
+Set Implicit Arguments.
+
+Open Scope Z_scope.
+
+
+Record ex: Set := mkEx {
+  vN : positive;
+  vS : positive;
+  vR:  List.list (positive * positive);
+  vA:  Z;
+  vB:  Z;
+  vx:  Z;
+  vy:  Z
+}.
+
+Coercion Local Zpos : positive >-> Z.
+
+Record ex_spec (exx: ex): Prop := mkExS {
+  n2_div: ~(2 | exx.(vN));
+  n_pos: 2 < exx.(vN);
+ lprime: 
+  forall p : positive * positive, List.In p (vR exx) -> prime (fst p);
+   lbig:
+    4 * vN exx < (Zmullp (vR exx) - 1) ^ 2;
+   inC:
+    vy exx ^ 2 mod vN exx = (vx exx ^ 3 + vA exx * vx exx + vB exx) mod vN exx
+}.
+
+Section NEll.
+
+Variable exx: ex.
+Variable exxs: ex_spec exx.
+
+Variable zZ: Type.
+Variable op: ZnZ.Ops zZ.
+Variable op_spec: ZnZ.Specs op.
+Definition z2Z z :=  ZnZ.to_Z z.
+Definition zN := snd (ZnZ.of_pos exx.(vN)).
+Variable mop: mod_op zZ.
+Variable mop_spec: mod_spec op zN mop.
+Variable N_small:  exx.(vN) < base (ZnZ.digits op).
+
+Lemma z2ZN: z2Z zN = exx.(vN).
+apply (@ZnZ.of_Z_correct _ _ op_spec exx.(vN)); split; auto with zarith.
+Qed.
+
+Definition Z2z z :=
+ match z mod exx.(vN) with
+ | Zpos p => snd (ZnZ.of_pos p)
+ | _ => ZnZ.zero
+ end.
+
+Definition S := exx.(vS).
+Definition R := exx.(vR).
+Definition A := Z2z exx.(vA).
+Definition B := Z2z exx.(vB).
+Definition xx := Z2z exx.(vx).
+Definition yy := Z2z exx.(vy).
+Definition c3 := Z2z 3.
+Definition c2 := Z2z 2.
+Definition c1 := Z2z 1.
+Definition c0 := Z2z 0.
+
+Inductive nelt: Type :=
+  nzero | ntriple: zZ -> zZ -> zZ  -> nelt.
+
+Definition pp := ntriple xx yy c1.
+
+Definition nplus x y := mop.(add_mod) x y.
+Definition nmul x y :=  mop.(mul_mod) x y.
+Definition nsub x y :=  mop.(sub_mod) x y.
+Definition neq x y := match ZnZ.compare x y with Eq => true | _ => false end.
+
+Notation "x ++ y " := (nplus x y).
+Notation "x -- y" := (nsub x y) (at level 50, left associativity).
+Notation "x ** y" := (nmul x y) (at level 40, left associativity).
+Notation "x ?= y" := (neq x y).
+
+Definition ndouble: zZ -> nelt -> (nelt * zZ):= fun (sc: zZ) (p1: nelt) =>
+ match p1 with
+  nzero => (p1, sc)
+ | (ntriple x1 y1 z1) =>
+    if (y1 ?= c0) then (nzero, z1 ** sc) else
+     (* we do 2p *)
+    let m' := c3 ** x1 ** x1 ++ A ** z1 ** z1 in
+    let l' := c2 ** y1 ** z1 in
+    let m'2 := m' ** m' in
+    let l'2 := l' ** l' in
+    let l'3 := l'2 ** l' in
+    let x3 := m'2 ** z1 -- c2 ** x1 ** l'2 in
+    (ntriple
+          (l' ** x3)
+          (l'2 ** (m' ** x1 -- y1 ** l') -- m' ** x3)
+          (z1 ** l'3), sc)
+  end.
+
+
+Definition nadd := fun (sc: zZ) (p1 p2: nelt) =>
+ match p1, p2 with
+  nzero, _ => (p2, sc)
+ | _ , nzero => (p1, sc)
+ | (ntriple x1 y1 z1), (ntriple x2 y2 z2) =>
+  let d1 := x2 ** z1 in
+  let d2 := x1 ** z2 in
+  let l := d1 -- d2 in
+  let dl := d1 ++ d2 in
+  let m := y2 ** z1 -- y1 ** z2 in
+  if (l ?= c0) then
+   (* we have p1 = p2 o p1 = -p2 *)
+   if (m ?= c0) then
+    if (y1 ?= c0) then (nzero, z1 ** z2 ** sc) else
+     (* we do 2p *)
+    let m' := c3 ** x1 ** x1 ++ A ** z1 ** z1 in
+    let l' := c2 ** y1 ** z1 in
+    let m'2 := m' ** m' in
+    let l'2 := l' ** l' in
+    let l'3 := l'2 ** l' in
+    let x3 := m'2 ** z1 -- c2 ** x1 ** l'2 in
+    (ntriple
+          (l' ** x3)
+          (l'2 ** (m' ** x1 -- y1 ** l') -- m' ** x3)
+          (z1 ** l'3), z2 ** sc)
+    else (* p - p *)  (nzero, m ** z1 ** z2 ** sc)
+  else
+     let l2 := l ** l in
+     let l3 := l2 ** l in
+     let m2 := m ** m in
+     let x3 := z1 ** z2 ** m2 -- l2 ** dl in
+      (ntriple (l ** x3)
+             (z2 ** l2 ** (m ** x1 -- y1 ** l) -- m ** x3)
+             (z1 ** z2 ** l3), sc)
+  end.
+
+
+Definition nopp p := 
+  match p with nzero => p | (ntriple x1 y1 z1) => (ntriple x1 (c0 -- y1) z1) end.
+
+Fixpoint scalb (sc: zZ) (b:bool) (a: nelt) (p: positive) {struct p}:
+ nelt * zZ :=
+ match p with
+   xH => if b then ndouble sc a else (a,sc)
+ | xO p1 => let (a1, sc1) := scalb sc false a p1 in
+              if b then 
+                let (a2, sc2) := ndouble sc1 a1 in
+                nadd sc2 a a2
+              else ndouble sc1 a1
+ | xI p1 => let (a1, sc1) := scalb sc true a p1 in
+              if b then  ndouble sc1 a1
+              else
+              let (a2, sc2) := ndouble sc1 a1 in 
+              nadd sc2 (nopp a) a2
+ end.
+
+Definition scal sc a p := scalb sc false a p.
+
+
+Definition scal_list sc a l :=
+  List.fold_left 
+  (fun (asc: nelt * zZ) p1 => let (a,sc) := asc in scal sc a p1) l (a,sc).
+
+Fixpoint scalL (sc:zZ) (a: nelt) (l: List.list positive) {struct l}: (nelt * zZ) :=
+   match l with
+     List.nil => (a,sc)
+   | List.cons n l1 =>
+        let (a1, sc1) := scal sc a n in
+        let (a2, sc2) := scal_list sc1 a l1 in
+          match a2 with
+             nzero => (nzero, c0)
+          |  ntriple _ _ z => scalL (sc2 ** z) a1 l1
+          end
+   end.
+
+Definition zpow sc p n :=
+  let (p,sc') := scal sc p n in
+  (p, ZnZ.to_Z (ZnZ.gcd sc' zN)).
+
+Definition e2E n := 
+  match n with 
+    nzero => ZEll.nzero
+  | ntriple x1 y1 z1 => ZEll.ntriple (z2Z x1) (z2Z y1) (z2Z z1)
+  end.
+
+
+Definition wft t :=  z2Z t = (z2Z t) mod (z2Z zN).
+
+Lemma vN_pos: 0 < exx.(vN).
+red; simpl; auto.
+Qed.
+
+Hint Resolve vN_pos.
+
+Lemma nplusz: forall x y, wft x -> wft y -> 
+      z2Z (x ++ y) = ZEll.nplus (vN exx) (z2Z x) (z2Z y).
+Proof.
+intros x y Hx Hy.
+unfold z2Z, nplus.
+rewrite (mop_spec.(add_mod_spec) _ _ _ _ Hx Hy); auto.
+rewrite <- z2ZN; auto.
+Qed.
+
+Lemma nplusw: forall x y, wft x -> wft y ->  wft (x ++ y).
+Proof.
+intros x y Hx Hy.
+unfold wft.
+pattern (z2Z (x ++ y)) at 2; rewrite (nplusz Hx Hy).
+unfold ZEll.nplus; rewrite z2ZN.
+rewrite Zmod_mod; auto.
+apply (nplusz Hx Hy).
+Qed.
+
+Lemma nsubz: forall x y, wft x -> wft y -> 
+      z2Z (x -- y) = ZEll.nsub (vN exx) (z2Z x) (z2Z y).
+Proof.
+intros x y Hx Hy.
+unfold z2Z, nsub.
+rewrite (mop_spec.(sub_mod_spec) _ _ _ _ Hx Hy); auto.
+rewrite <- z2ZN; auto.
+Qed.
+
+Lemma nsubw: forall x y, wft x -> wft y ->  wft (x -- y).
+Proof.
+intros x y Hx Hy.
+unfold wft.
+pattern (z2Z (x -- y)) at 2; rewrite (nsubz Hx Hy).
+unfold ZEll.nsub; rewrite z2ZN.
+rewrite Zmod_mod; auto.
+apply (nsubz Hx Hy).
+Qed.
+
+Lemma nmulz: forall x y, wft x -> wft y -> 
+      z2Z (x ** y) = ZEll.nmul (vN exx) (z2Z x) (z2Z y).
+Proof.
+intros x y Hx Hy.
+unfold z2Z, nmul.
+rewrite (mop_spec.(mul_mod_spec) _ _ _ _ Hx Hy); auto.
+rewrite <- z2ZN; auto.
+Qed.
+
+Lemma nmulw: forall x y, wft x -> wft y ->  wft (x ** y).
+Proof.
+intros x y Hx Hy.
+unfold wft.
+pattern (z2Z (x ** y)) at 2; rewrite (nmulz Hx Hy).
+unfold ZEll.nmul; rewrite z2ZN.
+rewrite Zmod_mod; auto.
+apply (nmulz Hx Hy).
+Qed.
+
+Hint Resolve nmulw nplusw nsubw.
+
+
+Definition wfe p := match p with
+  ntriple x y z => wft x /\ wft y /\ wft z
+| _ => True
+end.
+
+Lemma z2Zx: forall x, z2Z (Z2z x) = x mod exx.(vN).
+unfold Z2z; intros x.
+generalize (Z_mod_lt x exx.(vN)).
+case_eq (x mod exx.(vN)).
+intros _ _.
+simpl; unfold z2Z; rewrite ZnZ.spec_0; auto.
+intros p Hp HH; case HH; auto with zarith; clear HH.
+intros _ HH1.
+case (ZnZ.spec_to_Z zN).
+generalize  z2ZN; unfold z2Z; intros HH; rewrite HH; auto.
+intros _ H0.
+set (v := ZnZ.of_pos p); generalize HH1.
+rewrite (ZnZ.spec_of_pos p); fold v.
+case (fst v).
+  simpl; auto.
+intros p1 H1.
+contradict H0; apply Zle_not_lt.
+apply Zlt_le_weak; apply Zle_lt_trans with (2:= H1).
+apply Zle_trans with (1 * base (ZnZ.digits op) + 0); auto with zarith.
+apply Zplus_le_compat; auto.
+apply Zmult_gt_0_le_compat_r; auto with zarith.
+  case (ZnZ.spec_to_Z (snd v)); auto with zarith.
+  case p1; red; simpl; intros; discriminate.
+  case (ZnZ.spec_to_Z (snd v)); auto with zarith.
+intros p Hp; case (Z_mod_lt x exx.(vN)); auto with zarith.
+rewrite Hp; intros HH; case HH; auto.
+Qed.
+
+
+Lemma z2Zx1: forall x, z2Z (Z2z x) = z2Z (Z2z x) mod z2Z zN.
+Proof.
+unfold Z2z; intros x.
+generalize (Z_mod_lt x exx.(vN)).
+case_eq (x mod exx.(vN)).
+intros _ _.
+simpl; unfold z2Z; rewrite ZnZ.spec_0; auto.
+intros p H1 H2.
+case (ZnZ.spec_to_Z zN).
+generalize  z2ZN; unfold z2Z; intros HH; rewrite HH; auto.
+intros _ H0.
+case H2; auto with zarith; clear H2; intros _ H2.
+rewrite Zmod_small; auto.
+set (v := ZnZ.of_pos p).
+split.
+  case (ZnZ.spec_to_Z (snd v)); auto.
+generalize H2; rewrite (ZnZ.spec_of_pos p); fold v.
+case (fst v).
+  simpl; auto.
+intros p1 H.
+contradict H0; apply Zle_not_lt.
+apply Zlt_le_weak; apply Zle_lt_trans with (2:= H).
+apply Zle_trans with (1 * base (ZnZ.digits op) + 0); auto with zarith.
+apply Zplus_le_compat; auto.
+apply Zmult_gt_0_le_compat_r; auto with zarith.
+  case (ZnZ.spec_to_Z (snd v)); auto with zarith.
+  case p1; red; simpl; intros; discriminate.
+  case (ZnZ.spec_to_Z (snd v)); auto with zarith.
+intros p Hp; case (Z_mod_lt x exx.(vN)); auto with zarith.
+rewrite Hp; intros HH; case HH; auto.
+Qed.
+
+
+Lemma c0w: wft c0.
+Proof.
+red; unfold c0; apply z2Zx1.
+Qed.
+
+Lemma c2w: wft c2.
+Proof.
+red; unfold c2; apply z2Zx1.
+Qed.
+
+Lemma c3w: wft c3.
+Proof.
+red; unfold c3; apply z2Zx1.
+Qed.
+
+Lemma Aw: wft A.
+Proof.
+red; unfold A; apply z2Zx1.
+Qed.
+
+Hint Resolve c0w c2w c3w Aw.
+
+Ltac nw :=
+  repeat (apply nplusw || apply nsubw || apply nmulw || apply c2w ||
+          apply c3w || apply Aw); auto.
+
+
+Lemma nadd_wf: forall x y sc,
+  wfe x -> wfe y -> wft sc ->
+  wfe (fst (nadd sc x y)) /\  wft (snd (nadd sc x y)).
+Proof.
+intros x; case x; clear; auto.
+intros x1 y1 z1 y; case y; clear; auto.
+  intros x2 y2 z2 sc (wfx1,(wfy1, wfz1)) (wfx2,(wfy2, wfz2)) wfsc; 
+    simpl; auto.
+   case neq.
+    2: repeat split; simpl; nw.
+   case neq.
+    2: repeat split; simpl; nw.
+   case neq.
+   repeat split; simpl; nw; auto.
+   repeat split; simpl; nw; auto.
+Qed.
+
+ Lemma ztest: forall x y,
+     x ?= y =Zeq_bool (z2Z x) (z2Z y).
+ Proof.
+ intros x y.
+ unfold neq.
+ rewrite (ZnZ.spec_compare x y); case Zcompare_spec; intros HH;
+ match goal with H: context[x] |- _ =>
+   generalize H; clear H; intros HH1
+ end.
+ symmetry; apply GZnZ.Zeq_iok; auto.
+ case_eq (Zeq_bool (z2Z x) (z2Z y)); intros H1; auto;
+   generalize HH1; generalize (Zeq_bool_eq _ _ H1); unfold z2Z;
+   intros HH; rewrite HH; auto with zarith.
+ case_eq (Zeq_bool (z2Z x) (z2Z y)); intros H1; auto;
+   generalize HH1; generalize (Zeq_bool_eq _ _ H1); unfold z2Z;
+   intros HH; rewrite HH; auto with zarith.
+ Qed.
+
+ Lemma zc0: z2Z c0 = 0.
+ Proof.
+ unfold z2Z, c0, z2Z; simpl.
+ generalize ZnZ.spec_0; auto.
+ Qed.
+
+
+Ltac iftac t := 
+  match t with 
+   context[if ?x ?= ?y then _ else _] =>
+      case_eq (x ?= y)
+  end.
+
+Ltac ftac := match goal with
+  |- context[?x = ?y] => (iftac x); 
+    let H := fresh "tmp" in 
+     (try rewrite ztest; try rewrite zc0; intros H;
+      repeat ((rewrite nmulz in H || rewrite nplusz in H || rewrite nsubz in H); auto);
+      try (rewrite H; clear H))
+    end.
+
+Require Import Zmod.
+
+Lemma c2ww: forall x, ZEll.nmul (vN exx) 2 x = ZEll.nmul (vN exx) (z2Z c2) x.
+intros x; unfold ZEll.nmul.
+unfold c2; rewrite z2Zx; rewrite Zmodml; auto.
+Qed.
+Lemma c3ww: forall x, ZEll.nmul (vN exx) 3 x = ZEll.nmul (vN exx) (z2Z c3) x.
+intros x; unfold ZEll.nmul.
+unfold c3; rewrite z2Zx; rewrite Zmodml; auto.
+Qed.
+
+Lemma Aww: forall x, ZEll.nmul (vN exx) exx.(vA) x = ZEll.nmul (vN exx) (z2Z A) x.
+intros x; unfold ZEll.nmul.
+unfold A; rewrite z2Zx; rewrite Zmodml; auto.
+Qed.
+
+Lemma nadd_correct: forall x y sc,
+  wfe x -> wfe y -> wft sc ->
+  e2E (fst (nadd sc x y)) = fst (ZEll.nadd exx.(vN) exx.(vA) (z2Z sc) (e2E x) (e2E y) )/\
+  z2Z (snd (nadd sc x y)) = snd (ZEll.nadd exx.(vN) exx.(vA) (z2Z sc) (e2E x) (e2E y)).
+Proof.
+intros x; case x; clear; auto.
+intros x1 y1 z1 y; case y; clear; auto.
+  intros x2 y2 z2 sc (wfx1,(wfy1, wfz1)) (wfx2,(wfy2, wfz2)) wfsc; simpl.
+  ftac.
+  ftac.
+  ftac.
+  simpl; split; auto.
+  repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz); auto).
+  simpl; split; auto.
+  repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz||
+           rewrite c2ww || rewrite c3ww || rewrite Aww); try nw; auto).
+  rewrite nmulz; auto.
+  simpl; split; auto.
+  repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz); auto).
+  simpl; split; auto.
+  repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz ||
+           rewrite c2ww || rewrite c3ww || rewrite Aww); try nw; auto).
+  Qed.
+
+ Lemma ndouble_wf: forall x sc,
+  wfe x -> wft sc ->
+  wfe (fst (ndouble sc x)) /\  wft (snd (ndouble sc x)).
+Proof.
+intros x; case x; clear; auto.
+intros x1 y1 z1 sc (wfx1,(wfy1, wfz1)) wfsc; 
+    simpl; auto.
+  repeat (case neq; repeat split; simpl; nw; auto).
+Qed.
+
+
+Lemma ndouble_correct: forall x sc,
+  wfe x -> wft sc ->
+  e2E (fst (ndouble sc x)) = fst (ZEll.ndouble exx.(vN) exx.(vA) (z2Z sc) (e2E x))/\
+  z2Z (snd (ndouble sc x)) = snd (ZEll.ndouble exx.(vN) exx.(vA) (z2Z sc) (e2E x)).
+Proof.
+intros x; case x; clear; auto.
+  intros x1 y1 z1 sc (wfx1,(wfy1, wfz1))  wfsc; simpl.
+  ftac.
+  simpl; split; auto.
+  repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz); auto).
+  simpl; split; auto.
+  repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz ||
+           rewrite c2ww || rewrite c3ww || rewrite Aww); try nw; auto).
+  Qed.
+
+Lemma nopp_wf: forall x, wfe x -> wfe (nopp x).
+Proof.
+intros x; case x; simpl nopp; auto.
+intros x1 y1 z1 [H1 [H2 H3]]; repeat split; auto.
+Qed.
+
+Lemma scalb_wf: forall n b x sc,
+  wfe x -> wft sc ->
+  wfe (fst (scalb sc b x n)) /\  wft (snd (scalb sc b x n)).
+Proof.
+intros n; elim n; unfold scalb; fold scalb; auto.
+  intros n1 Hrec b x sc H H1.
+    case (Hrec true x sc H H1).
+    case scalb; simpl fst; simpl snd.
+    intros a1 sc1 H2 H3.
+    case (ndouble_wf _ H2 H3); auto;
+    case ndouble; simpl fst; simpl snd; intros x2 sc2 H4 H5.
+    case b; auto.
+    case (nadd_wf _ _ (nopp_wf _ H) H4 H5); auto;
+    case ndouble; simpl fst; simpl snd; intros x2 sc2 H4 H5.
+  intros n1 Hrec b x sc H H1.
+    case (Hrec false x sc H H1).
+    case scalb; simpl fst; simpl snd.
+    intros a1 sc1 H2 H3.
+    case (ndouble_wf _ H2 H3); auto;
+    case ndouble; simpl fst; simpl snd; intros x2 sc2 H4 H5.
+    case b; auto.
+    case (nadd_wf _ _ H H4 H5); auto;
+    case ndouble; simpl fst; simpl snd; intros x2 sc2 H4 H5.
+intros b x sc H H1; case b; auto.
+case (ndouble_wf _ H H1); auto.
+Qed.
+
+
+Lemma scal_wf: forall n x sc,
+  wfe x -> wft sc ->
+  wfe (fst (scal sc x n)) /\  wft (snd (scal sc x n)).
+Proof.
+intros n; exact (scalb_wf n false).
+Qed.
+
+Lemma nopp_correct: forall x,
+  wfe x -> e2E x = ZEll.nopp exx.(vN) (e2E (nopp x)).
+Proof.
+intros x; case x; simpl; auto.
+intros x1 y1 z1 [H1 [H2 H3]]; apply f_equal3 with (f := ZEll.ntriple); auto.
+rewrite nsubz; auto.
+rewrite zc0.
+unfold ZEll.nsub, ninv; simpl.
+apply sym_equal.
+rewrite <- (Z_mod_plus) with (b := -(-z2Z y1 /exx.(vN))); auto with zarith.
+rewrite <- Zopp_mult_distr_l.
+rewrite <- Zopp_plus_distr.
+rewrite Zmult_comm; rewrite Zplus_comm.
+rewrite <- Z_div_mod_eq; auto with zarith.
+rewrite Zopp_involutive; rewrite <- z2ZN.
+apply sym_equal; auto.
+Qed.
+
+Lemma scalb_correct: forall n b x sc,
+  wfe x -> wft sc ->
+  e2E (fst (scalb sc b x n)) = fst (ZEll.scalb exx.(vN) exx.(vA) (z2Z sc) b (e2E x) n)/\
+  z2Z (snd (scalb sc b x n)) = snd (ZEll.scalb exx.(vN) exx.(vA) (z2Z sc) b (e2E x) n).
+Proof.
+intros n; elim n; clear; auto.
+intros p Hrec b x sc H1 H2.
+  case b; unfold scalb; fold scalb.
+    generalize (scalb_wf p true x H1 H2);
+    generalize (Hrec true _ _ H1 H2); case scalb; simpl.
+    case ZEll.scalb; intros r1 rc1; simpl.
+    intros a2 sc2 (H3, H4) (H5, H6); subst r1 rc1.
+    apply ndouble_correct; auto.
+    generalize (scalb_wf p true x H1 H2);
+    generalize (Hrec true _ _ H1 H2); case scalb; simpl.
+    case ZEll.scalb; intros r1 rc1; simpl.
+    intros a2 sc2 (H3, H4) (H5, H6); subst r1 rc1.
+    generalize (ndouble_wf _ H5 H6); 
+      generalize (ndouble_correct _ H5 H6); case ndouble; simpl.
+    case ZEll.ndouble; intros r1 rc1; simpl.
+    intros a3 sc3 (H7,H8) (H9,H10); subst r1 rc1.
+    replace (ZEll.nopp (vN exx) (e2E x)) with
+      (e2E (nopp x)).
+    apply nadd_correct; auto. 
+    generalize H1; case x; auto.
+    intros x1 y1 z1 [HH1 [HH2 HH3]]; split; auto.
+    rewrite nopp_correct; auto.
+    apply f_equal2 with (f := ZEll.nopp); auto.
+    generalize H1; case x; simpl; auto; clear x H1.
+    intros x1 y1 z1 [HH1 [HH2 HH3]]; 
+      apply f_equal3 with (f := ZEll.ntriple); auto.
+    repeat rewrite nsubz; auto.
+    rewrite zc0.
+    unfold ZEll.nsub; simpl.
+    rewrite <- (Z_mod_plus) with (b := -(-z2Z y1 /exx.(vN))); auto with zarith.
+    rewrite <- Zopp_mult_distr_l.
+    rewrite <- Zopp_plus_distr.
+    rewrite Zmult_comm; rewrite Zplus_comm.
+    rewrite <- Z_div_mod_eq; auto with zarith.
+    rewrite Zopp_involutive; rewrite <- z2ZN.
+    apply sym_equal; auto.
+    generalize H1; case x; auto.
+    intros x1 y1 z1 [HH1 [HH2 HH3]]; split; auto.
+intros p Hrec b x sc H1 H2.
+  case b; unfold scalb; fold scalb.
+    generalize (scalb_wf p false x H1 H2);
+    generalize (Hrec false _ _ H1 H2); case scalb; simpl.
+    case ZEll.scalb; intros r1 rc1; simpl.
+    intros a2 sc2 (H3, H4) (H5, H6); subst r1 rc1.
+    generalize (ndouble_wf _ H5 H6); 
+      generalize (ndouble_correct _ H5 H6); case ndouble; simpl.
+    case ZEll.ndouble; intros r1 rc1; simpl.
+    intros a3 sc3 (H7,H8) (H9,H10); subst r1 rc1.
+    replace (ZEll.nopp (vN exx) (e2E x)) with
+      (e2E (nopp x)).
+    apply nadd_correct; auto.
+    rewrite nopp_correct; auto.
+    apply f_equal2 with (f := ZEll.nopp); auto.
+    generalize H1; case x; simpl; auto; clear x H1.
+    intros x1 y1 z1 [HH1 [HH2 HH3]]; 
+      apply f_equal3 with (f := ZEll.ntriple); auto.
+    repeat rewrite nsubz; auto.
+    rewrite zc0.
+    unfold ZEll.nsub; simpl.
+    rewrite <- (Z_mod_plus) with (b := -(-z2Z y1 /exx.(vN))); auto with zarith.
+    rewrite <- Zopp_mult_distr_l.
+    rewrite <- Zopp_plus_distr.
+    rewrite Zmult_comm; rewrite Zplus_comm.
+    rewrite <- Z_div_mod_eq; auto with zarith.
+    rewrite Zopp_involutive; rewrite <- z2ZN.
+    apply sym_equal; auto.
+    generalize H1; case x; auto.
+    intros x1 y1 z1 [HH1 [HH2 HH3]]; split; auto.
+    generalize (scalb_wf p false x H1 H2);
+    generalize (Hrec false _ _ H1 H2); case scalb; simpl.
+    case ZEll.scalb; intros r1 rc1; simpl.
+    intros a2 sc2 (H3, H4) (H5, H6); subst r1 rc1.
+    apply ndouble_correct; auto.
+intros b x sc H H1.
+case b; simpl; auto.
+apply ndouble_correct; auto.
+Qed.
+
+
+Lemma scal_correct: forall n x sc,
+  wfe x -> wft sc ->
+  e2E (fst (scal sc x n)) = fst (ZEll.scal exx.(vN) exx.(vA) (z2Z sc) (e2E x) n)/\
+  z2Z (snd (scal sc x n)) = snd (ZEll.scal exx.(vN) exx.(vA) (z2Z sc) (e2E x) n).
+Proof.
+intros n; exact (scalb_correct n false).
+Qed. 
+
+Lemma scal_list_correct: forall l x sc,
+  wfe x -> wft sc ->
+  e2E (fst (scal_list sc x l)) = fst (ZEll.scal_list exx.(vN) exx.(vA) (z2Z sc) (e2E x) l)/\
+  z2Z (snd (scal_list sc x l)) = snd (ZEll.scal_list exx.(vN) exx.(vA) (z2Z sc) (e2E x) l).
+Proof.
+intros l1; elim l1; simpl; auto.
+unfold scal_list, ZEll.scal_list; simpl; intros a l2 Hrec x sc H1 H2.
+generalize (scal_correct a _ H1 H2) (scal_wf a _ H1 H2); case scal.
+case ZEll.scal; intros r1 rsc1; simpl.
+simpl; intros a1 sc1 (H3, H4) (H5, H6); subst r1 rsc1; auto.
+Qed.
+
+Lemma scal_list_wf: forall l x sc,
+  wfe x -> wft sc ->
+  wfe (fst (scal_list sc x l)) /\  wft (snd (scal_list sc x l)).
+Proof.
+intros l1; elim l1; simpl; auto.
+unfold scal_list; intros a l Hrec x sc H1 H2; simpl.
+generalize (@scal_wf a _ _ H1 H2); 
+  case (scal sc x a); simpl; intros x1 sc1 [H3 H4]; auto.
+Qed.
+
+Lemma scalL_wf: forall l x sc,
+  wfe x -> wft sc ->
+  wfe (fst (scalL sc x l)) /\  wft (snd (scalL sc x l)).
+Proof.
+intros l1; elim l1; simpl; auto.
+intros a l2 Hrec x sc H1 H2.
+generalize (scal_wf a _ H1 H2); case scal; simpl.
+intros a1 sc1 (H3, H4); auto.
+generalize (scal_list_wf l2 _ H1 H4); case scal_list; simpl.
+intros a2 sc2; case a2; simpl; auto.
+intros x1 y1 z1 ((V1, (V2, V3)), V4); apply Hrec; auto.
+Qed. 
+
+Lemma scalL_correct: forall l x sc,
+  wfe x -> wft sc ->
+  e2E (fst (scalL sc x l)) = fst (ZEll.scalL exx.(vN) exx.(vA) (z2Z sc) (e2E x) l)/\
+  z2Z (snd (scalL sc x l)) = snd (ZEll.scalL exx.(vN) exx.(vA) (z2Z sc) (e2E x) l).
+Proof.
+intros l1; elim l1; simpl; auto.
+intros a l2 Hrec x sc H1 H2.
+generalize (scal_wf a _ H1 H2) (scal_correct a _ H1 H2); case scal; simpl.
+case ZEll.scal; intros r1 rsc1; simpl.
+intros a1 sc1 (H3, H4) (H5, H6); subst r1 rsc1.
+generalize (scal_list_wf l2 _ H1 H4) (scal_list_correct l2 _ H1 H4); case scal_list; simpl.
+case ZEll.scal_list; intros r1 rsc1; simpl.
+intros a2 sc2 (H7, H8) (H9, H10); subst r1 rsc1.
+generalize H7; clear H7; case a2; simpl; auto.
+rewrite zc0; auto.
+intros x1 y1 z1 (V1, (V2, V3)); auto.
+generalize (nmulw H8 V3) (nmulz H8 V3); intros V4 V5; rewrite <- V5.
+apply Hrec; auto.
+Qed.
+
+Lemma f4 : wft (Z2z 4).
+Proof.
+red; apply z2Zx1.
+Qed.
+
+Lemma f27 : wft (Z2z 27).
+Proof.
+red; apply z2Zx1.
+Qed.
+
+Lemma Bw : wft B.
+Proof.
+red; unfold B; apply z2Zx1.
+Qed.
+
+Hint Resolve f4 f27 Bw.
+
+Lemma mww: forall x y, ZEll.nmul (vN exx) (x mod (vN exx) ) y = ZEll.nmul (vN exx) x y.
+intros x  y; unfold ZEll.nmul; rewrite Zmodml; auto.
+Qed.
+
+Lemma wwA: forall x, ZEll.nmul (vN exx) x exx.(vA) = ZEll.nmul (vN exx) x (z2Z A).
+intros x; unfold ZEll.nmul.
+unfold A; rewrite z2Zx; rewrite Zmodmr; auto.
+Qed.
+
+Lemma wwB: forall x, ZEll.nmul (vN exx) x exx.(vB) = ZEll.nmul (vN exx) x (z2Z B).
+intros x; unfold ZEll.nmul.
+unfold B; rewrite z2Zx; rewrite Zmodmr; auto.
+Qed.
+
+ Lemma  scalL_prime: 
+  let a := ntriple (Z2z (exx.(vx))) (Z2z (exx.(vy))) c1 in
+  let isc := (Z2z 4) ** A ** A ** A  ++ (Z2z 27) ** B ** B in
+  let (a1, sc1) := scal isc a exx.(vS) in
+  let (S1,R1) := psplit exx.(vR) in
+  let (a2, sc2) := scal sc1 a1 S1 in
+  let (a3, sc3) := scalL sc2 a2 R1 in
+    match a3 with
+     nzero => if (Zeq_bool (Zgcd (z2Z sc3) exx.(vN)) 1) then prime exx.(vN)
+              else True
+   | _ => True
+   end.
+  Proof.
+  intros a isc.
+  case_eq (scal isc a (vS exx)); intros a1 sc1 Ha1.
+  case_eq (psplit (vR exx)); intros S1 R1 HS1.
+  case_eq (scal sc1 a1 S1); intros a2 sc2 Ha2.
+  case_eq (scalL sc2 a2 R1); intros a3 sc3; case a3; auto.
+  intros Ha3; case_eq (Zeq_bool (Zgcd (z2Z sc3) (vN exx)) 1); auto.
+  intros H1.
+  assert (F0: 
+     (vy exx mod vN exx) ^ 2 mod vN exx =
+       ((vx exx mod vN exx) ^ 3 + vA exx * (vx exx mod vN exx) +
+        vB exx) mod vN exx).
+      generalize exxs.(inC).
+      simpl; unfold Zpower_pos; simpl.
+      repeat rewrite Zmult_1_r.
+      intros HH.
+      match goal with |- ?t1 = ?t2 => rmod t1; auto end.
+      rewrite HH.
+      rewrite Zplus_mod; auto; symmetry; rewrite Zplus_mod; auto; symmetry.
+      apply f_equal2 with (f := Zmod); auto.
+      apply f_equal2 with (f := Zplus); auto.
+      rewrite Zplus_mod; auto; symmetry; rewrite Zplus_mod; auto; symmetry.
+      apply f_equal2 with (f := Zmod); auto.
+      apply f_equal2 with (f := Zplus); auto.
+      rewrite Zmult_mod; auto; symmetry; rewrite Zmult_mod; auto; symmetry.
+      apply f_equal2 with (f := Zmod); auto.
+      apply f_equal2 with (f := Zmult); auto.
+      rewrite Zmod_mod; auto.
+      match goal with |- ?t1 = ?t2 => rmod t2; auto end.
+      rewrite Zmult_mod; auto; symmetry; rewrite Zmult_mod; auto; symmetry.
+      apply f_equal2 with (f := Zmod); auto.
+      rewrite Zmod_mod; auto.
+   generalize (@ZEll.scalL_prime exx.(vN) 
+               (exx.(vx) mod exx.(vN))
+               (exx.(vy) mod exx.(vN))
+               exx.(vA)
+               exx.(vB) 
+               exxs.(n_pos) exxs.(n2_div) exx.(vR) 
+               exxs.(lprime) exx.(vS) exxs.(lbig) F0); simpl.
+generalize (@scal_wf (vS exx) a isc) (@scal_correct (vS exx) a isc).
+unfold isc.
+rewrite nplusz; auto; try nw; auto.
+repeat rewrite nmulz; auto; try nw; auto.
+  repeat rewrite z2Zx.
+repeat rewrite wwA || rewrite wwB|| rewrite mww.
+replace (e2E a) with (ZEll.ntriple (vx exx mod vN exx) (vy exx mod vN exx) 1).
+case ZEll.scal.
+fold isc; rewrite HS1; rewrite Ha1; simpl; auto.
+intros r1 rsc1 HH1 HH2.
+case HH1; clear HH1.
+  unfold c1; repeat split; red; try apply z2Zx1.
+  unfold isc; nw.
+case HH2; clear HH2.
+  unfold c1; repeat split; red; try apply z2Zx1.
+  unfold isc; nw.
+intros U1 U2 W1 W2; subst r1 rsc1.
+generalize (@scal_wf S1 a1 sc1) (@scal_correct S1 a1 sc1).
+case ZEll.scal.
+intros r1 rsc1 HH1 HH2.
+case HH1; clear HH1; auto.
+case HH2; clear HH2; auto.
+rewrite Ha2; simpl.
+intros U1 U2 W3 W4; subst r1 rsc1.
+generalize (@scalL_wf R1 a2 sc2) (@scalL_correct R1 a2 sc2).
+case ZEll.scalL.
+intros n; case n; auto.
+rewrite Ha3; simpl.
+intros rsc1 HH1 HH2.
+case HH1; clear HH1; auto.
+case HH2; clear HH2; auto.
+intros _ U2 _ W5; subst rsc1.
+rewrite H1; auto.
+intros x1 y1 z1 sc4; rewrite Ha3; simpl; auto.
+intros _ HH; case HH; auto.
+intros; discriminate.
+unfold a; simpl.
+unfold c1; repeat rewrite z2Zx.
+rewrite (Zmod_small 1); auto.
+generalize exxs.(n_pos).
+auto with zarith.
+Qed.
+
+End NEll.
+
+Fixpoint plength (p: positive) : positive :=
+  match p with
+    xH => xH
+  | xO p1 => Psucc (plength p1)
+  | xI p1 => Psucc (plength p1)
+  end.
+
+Theorem plength_correct: forall p, (Zpos p < 2 ^ Zpos (plength p))%Z.
+assert (F: (forall p, 2 ^ (Zpos (Psucc p)) = 2 * 2 ^ Zpos p)%Z).
+intros p; replace (Zpos (Psucc p)) with (1 + Zpos p)%Z.
+rewrite Zpower_exp; auto with zarith.
+rewrite Zpos_succ_morphism; unfold Zsucc; auto with zarith.
+intros p; elim p; simpl plength; auto.
+intros p1 Hp1; rewrite F; repeat rewrite Zpos_xI.
+assert (tmp: (forall p, 2 * p = p + p)%Z);
+  try repeat rewrite tmp; auto with zarith.
+intros p1 Hp1; rewrite F; rewrite (Zpos_xO p1).
+assert (tmp: (forall p, 2 * p = p + p)%Z);
+  try repeat rewrite tmp; auto with zarith.
+rewrite Zpower_1_r; auto with zarith.
+Qed.
+
+Theorem plength_pred_correct: forall p, (Zpos p <= 2 ^ Zpos (plength (Ppred p)))
+%Z.
+intros p; case (Psucc_pred p); intros H1.
+subst; simpl plength.
+rewrite Zpower_1_r; auto with zarith.
+pattern p at 1; rewrite <- H1.
+rewrite Zpos_succ_morphism; unfold Zsucc; auto with zarith.
+generalize (plength_correct (Ppred p)); auto with zarith.
+Qed.
+
+Definition pheight p := plength (Ppred (plength (Ppred p))).
+
+Theorem pheight_correct: forall p, (Zpos p <= 2 ^ (2 ^ (Zpos (pheight p))))%Z.
+intros p; apply Zle_trans with (1 := (plength_pred_correct p)).
+apply Zpower_le_monotone; auto with zarith.
+split; auto with zarith.
+unfold pheight; apply plength_pred_correct.
+Qed.
+
+Definition isM2 p := 
+  match p with
+    xH   => false
+|    xO _ => false
+|     _ => true
+end.
+
+Lemma isM2_correct: forall p,
+  if isM2 p then ~(Zdivide 2 p) /\ 2 < p else True.
+Proof.
+intros p; case p; simpl; auto; clear p.
+intros p1; split; auto.
+intros HH; inversion_clear HH.
+generalize H; rewrite Zmult_comm.
+case x; simpl; intros; discriminate.
+case p1; red; simpl; auto.
+Qed.
+
+Definition ell_test (N S: positive) (l: List.list (positive * positive))
+                      (A B x y: Z) :=
+  let op := cmk_op (Peano.pred (nat_of_P (get_height 31 (plength N)))) in
+  let mop := make_mod_op op (ZnZ.of_Z N) in
+    if isM2 N then
+    match (4 * N) ?= (ZEll.Zmullp l - 1) ^ 2  with
+      Lt => 
+       match y ^ 2 mod N ?= (x ^ 3 + A * x + B) mod N with
+       Eq => 
+          let ex := mkEx N S l A B x y in
+          let a := ntriple (Z2z ex op x) (Z2z ex op y) (Z2z ex op 1)  in
+          let A := (Z2z  ex op A) in
+          let B := (Z2z  ex op B) in
+          let d4 := (Z2z  ex op 4) in
+          let d27 := (Z2z  ex op 27) in
+          let da := mop.(add_mod) in
+          let dm := mop.(mul_mod) in
+          let isc := (da (dm (dm  (dm d4 A) A) A) (dm (dm d27 B) B)) in
+          let (a1, sc1) := scal ex op mop isc a S in
+          let (S1,R1) := ZEll.psplit l in
+          let (a2, sc2) := scal ex op mop sc1 a1 S1 in
+          let (a3, sc3) := scalL ex op mop sc2 a2 R1 in
+          match a3 with
+           nzero => if (Zeq_bool (Zgcd (z2Z op sc3) N) 1) then true
+                    else false
+          | _ => false
+          end
+      | _  => false
+       end
+    | _  => false
+    end 
+    else false.
+
+Lemma Zcompare_correct: forall x y,
+  match x ?= y with Eq => x = y | Gt => x > y | Lt => x < y end.
+Proof.
+intros x y; unfold Zlt, Zgt; generalize (Zcompare_Eq_eq x y); case Zcompare; auto.
+Qed.
+
+Lemma ell_test_correct: forall (N S: positive) (l: List.list (positive * positive))
+                      (A B x y: Z),
+  (forall p, List.In p l -> prime (fst p)) -> 
+  if ell_test N S l A B x y then prime N else True.
+intros N S1 l A1 B1 x y H; unfold ell_test.
+generalize (isM2_correct N); case isM2; auto.
+intros (H1, H2).
+match goal with |- context[?x ?= ?y] =>
+  generalize (Zcompare_correct x y); case Zcompare; auto
+end; intros H3.
+match goal with |- context[?x ?= ?y] =>
+  generalize (Zcompare_correct x y); case Zcompare; auto
+end; intros H4.
+set (n := Peano.pred (nat_of_P (get_height 31 (plength N)))).
+set (op := cmk_op n).
+set (mop := make_mod_op op (ZnZ.of_Z N)).
+set (exx := mkEx N S1 l A1 B1 x y).
+set (op_spec := cmk_spec n).
+assert (exxs: ex_spec exx).
+  constructor; auto.
+assert (H0: N < base (ZnZ.digits op)).
+  apply Zlt_le_trans with (1 := plength_correct N).
+  unfold op, base.
+  rewrite cmk_op_digits.
+  apply Zpower_le_monotone; split; auto with zarith.
+  generalize (get_height_correct 31 (plength N)); unfold n.
+  set (p := plength N).
+  replace (Z_of_nat (Peano.pred (nat_of_P (get_height 31 p)))) with
+       ((Zpos (get_height 31 p) - 1) ); auto with zarith.
+  rewrite pred_of_minus; rewrite inj_minus1; auto with zarith.
+  rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto with zarith.
+  generalize (lt_O_nat_of_P (get_height 31 p)); auto with zarith.
+assert (mspec: mod_spec op (zN exx op) mop).
+  unfold mop; apply make_mod_spec; auto.
+  rewrite ZnZ.of_Z_correct; auto with zarith.
+generalize (@scalL_prime exx exxs _ op (cmk_spec n) mop mspec H0).
+lazy zeta.
+unfold c1, A, B,  nplus, nmul; 
+  simpl exx.(vA); simpl exx.(vB); simpl exx.(vx); simpl exx.(vy);
+  simpl exx.(vS); simpl exx.(vR); simpl exx.(vN).
+case scal; intros a1 sc1.
+case ZEll.psplit; intros S2 R2.
+case scal; intros a2 sc2.
+case scalL; intros a3 sc3.
+case a3; auto.
+case Zeq_bool; auto.
+Qed.
+
+Time Eval vm_compute in (ell_test
+  329719147332060395689499
+  8209062
+  (List.cons (40165264598163841%positive,1%positive) List.nil)
+  (-94080)
+  9834496
+  0
+  3136).
+
+
+Time Eval vm_compute in (ell_test
+  1384435372850622112932804334308326689651568940268408537
+  13077052794
+  (List.cons (105867537178241517538435987563198410444088809%positive, 1%positive) List.nil)
+  (-677530058123796416781392907869501000001421915645008494)
+  0
+  (-169382514530949104195348226967375250000355478911252124)
+  1045670343788723904542107880373576189650857982445904291
+).
diff --git a/coqprime/num/Pock.v b/coqprime/num/Pock.v
new file mode 100644
index 000000000..3b467af5a
--- /dev/null
+++ b/coqprime/num/Pock.v
@@ -0,0 +1,964 @@
+
+(*************************************************************)
+(*      This file is distributed under the terms of the      *)
+(*      GNU Lesser General Public License Version 2.1        *)
+(*************************************************************)
+(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
+(*************************************************************)
+
+Require Import List.
+Require Import ZArith.
+Require Import Zorder.
+Require Import ZCAux.
+Require Import LucasLehmer.
+Require Import Pocklington.
+Require Import ZArith Znumtheory Zpow_facts.
+Require Import CyclicAxioms DoubleCyclic BigN Cyclic31 Int31.
+Require Import Pmod.
+Require Import Mod_op.
+Require Import W.
+Require Import Lucas.
+Require Export PocklingtonCertificat.
+Require Import NEll.
+Import CyclicAxioms DoubleType DoubleBase List.
+
+Open Scope Z_scope. 
+
+Section test.
+
+Variable w: Type.
+Variable w_op: ZnZ.Ops w.
+Variable op_spec: ZnZ.Specs w_op.
+Variable p: positive.
+Variable b: w.
+
+Notation "[| x |]" :=
+   (ZnZ.to_Z x)  (at level 0, x at level 99).
+
+Hypothesis b_pos: 0 < [|b|].
+
+Variable m_op: mod_op w.
+Variable m_op_spec: mod_spec w_op b m_op.
+
+Open Scope positive_scope.
+Open Scope P_scope.
+
+Let pow := m_op.(power_mod).
+Let times := m_op.(mul_mod).
+Let pred:= m_op.(pred_mod).
+
+(* [fold_pow_mod a [q1,_;...;qn,_]] b = a ^(q1*...*qn) mod b *)
+(* invariant a mod N = a *)
+Definition fold_pow_mod (a: w) l := 
+  fold_left
+    (fun a' (qp:positive*positive) =>  pow a' (fst qp))
+    l a.
+
+Lemma fold_pow_mod_spec : forall l (a:w), 
+  ([|a|] < [|b|])%Z -> [|fold_pow_mod a l|] = ([|a|]^(mkProd' l) mod [|b|])%Z. 
+intros l; unfold fold_pow_mod; elim l; simpl fold_left; simpl mkProd'; auto; clear l.
+intros a H; rewrite Zpower_1_r; rewrite Zmod_small; auto with zarith.
+case (ZnZ.spec_to_Z a); auto with zarith.
+intros (p1, q1) l Rec a H.
+case (ZnZ.spec_to_Z a); auto with zarith; intros U1 U2.
+rewrite Rec.
+rewrite m_op_spec.(power_mod_spec) with (t := [|a|]); auto with zarith.
+rewrite <- Zpower_mod.
+rewrite times_Zmult; rewrite Zpower_mult; auto with zarith.
+apply Zle_lt_trans with (2 := H); auto with zarith.
+rewrite Zmod_small; auto with zarith.
+rewrite m_op_spec.(power_mod_spec) with (t := [|a|]); auto with zarith.
+match goal with |- context[(?X mod ?Y)%Z] =>
+  case (Z_mod_lt X Y); auto with zarith
+end.
+rewrite Zmod_small; auto with zarith.
+Qed.
+
+
+Fixpoint all_pow_mod (prod a: w) (l:dec_prime) {struct l}: w*w :=
+  match l with
+  | nil => (prod,a)
+  | (q,_) :: l => 
+    let m := pred (fold_pow_mod a l) in
+    all_pow_mod (times prod m) (pow a q) l
+  end.
+
+
+Lemma snd_all_pow_mod :
+ forall l (prod a :w), ([|a|] < [|b|])%Z ->
+   [|snd (all_pow_mod prod a l)|] = ([|a|]^(mkProd' l) mod [|b|])%Z.
+intros l; elim l; simpl all_pow_mod; simpl mkProd'; simpl snd; clear l.
+intros _ a H; rewrite Zpower_1_r; auto with zarith.
+rewrite Zmod_small; auto with zarith.
+case (ZnZ.spec_to_Z a); auto with zarith.
+intros (p1, q1) l Rec prod a H.
+case (ZnZ.spec_to_Z a); auto with zarith; intros U1 U2.
+rewrite Rec; auto with zarith.
+rewrite m_op_spec.(power_mod_spec) with (t := [|a|]); auto with zarith.
+rewrite <- Zpower_mod.
+rewrite times_Zmult; rewrite Zpower_mult; auto with zarith.
+apply Zle_lt_trans with (2 := H); auto with zarith.
+rewrite Zmod_small; auto with zarith.
+rewrite m_op_spec.(power_mod_spec) with (t := [|a|]); auto with zarith.
+match goal with |- context[(?X mod ?Y)%Z] =>
+  case (Z_mod_lt X Y); auto with zarith
+end.
+rewrite Zmod_small; auto with zarith.
+Qed.
+
+Lemma fold_aux : forall a N l prod,
+  (fold_left
+     (fun (r : Z) (k : positive * positive) =>
+      r * (a ^(N / fst k) - 1) mod [|b|]) l (prod mod [|b|]) mod [|b|] = 
+  fold_left
+     (fun (r : Z) (k : positive * positive) =>
+      r * (a^(N / fst k) - 1)) l prod mod [|b|])%Z.
+induction l;simpl;intros.
+rewrite Zmod_mod; auto with zarith.
+rewrite <- IHl; auto with zarith.
+rewrite Zmult_mod; auto with zarith.
+rewrite Zmod_mod; auto with zarith.
+rewrite <- Zmult_mod; auto with zarith.
+Qed.
+
+Lemma fst_all_pow_mod :
+ forall l (a:w) (R:positive) (prod A :w),
+  [|prod|] = ([|prod|] mod [|b|])%Z ->
+  [|A|] = ([|a|]^R mod [|b|])%Z ->
+  [|fst (all_pow_mod prod A l)|] = 
+    ((fold_left
+      (fun r (k:positive*positive) => 
+        (r * ([|a|] ^ (R* mkProd' l / (fst k)) - 1))) l [|prod|]) mod [|b|])%Z.
+intros l; elim l; simpl all_pow_mod; simpl fold_left; simpl fst;
+  auto with zarith; clear l.
+intros (p1,q1) l Rec; simpl fst.
+intros a R prod A H1 H2.
+assert (F: (0 <= [|A|] < [|b|])%Z).
+rewrite H2.
+match goal with |- context[(?X mod ?Y)%Z] =>
+  case (Z_mod_lt X Y); auto with zarith
+end.
+assert (F1: ((fun x => x = x mod [|b|])%Z [|fold_pow_mod A l|])).
+rewrite Zmod_small; auto.
+rewrite fold_pow_mod_spec; auto with zarith.
+match goal with |- context[(?X mod ?Y)%Z] =>
+  case (Z_mod_lt X Y); auto with zarith
+end.
+assert (F2: ((fun x => x = x mod [|b|])%Z [|pred (fold_pow_mod A l)|])).
+rewrite Zmod_small; auto.
+rewrite(fun x => m_op_spec.(pred_mod_spec) x [|x|]);
+  auto with zarith.
+match goal with |- context[(?X mod ?Y)%Z] =>
+  case (Z_mod_lt X Y); auto with zarith
+end.
+rewrite (Rec a (R * p1)%positive); auto with zarith.
+rewrite(fun x y => m_op_spec.(mul_mod_spec) x y [|x|] [|y|]);
+  auto with zarith.
+rewrite(fun x => m_op_spec.(pred_mod_spec) x [|x|]);
+  auto with zarith.
+rewrite fold_pow_mod_spec; auto with zarith.
+rewrite H2.
+repeat rewrite Zpos_mult.
+repeat rewrite times_Zmult.
+repeat rewrite <- Zmult_assoc.
+apply sym_equal; rewrite <- fold_aux; auto with zarith.
+apply sym_equal; rewrite <- fold_aux; auto with zarith.
+eq_tac; auto.
+match goal with |- context[fold_left ?x  _ _] =>
+  apply f_equal2 with (f := fold_left x); auto with zarith
+end.
+rewrite Zmod_mod; auto with zarith.
+rewrite (Zmult_comm R); repeat rewrite <- Zmult_assoc;
+ rewrite (Zmult_comm p1); rewrite Z_div_mult; auto with zarith.
+repeat rewrite (Zmult_mod [|prod|]);auto with zmisc.
+eq_tac; [idtac | eq_tac]; auto.
+eq_tac; auto.
+rewrite Zmod_mod; auto.
+repeat rewrite (fun x => Zminus_mod x 1); auto with zarith.
+eq_tac; auto; eq_tac; auto.
+rewrite Zmult_comm; rewrite <- Zpower_mod; auto with zmisc. 
+rewrite Zpower_mult; auto with zarith.
+rewrite Zmod_mod; auto with zarith.
+rewrite Zmod_small; auto.
+rewrite(fun x y => m_op_spec.(mul_mod_spec) x y [|x|] [|y|]);
+  auto with zarith.
+match goal with |- context[(?X mod ?Y)%Z] =>
+  case (Z_mod_lt X Y); auto with zarith
+end.
+rewrite(fun x => m_op_spec.(power_mod_spec) x [|x|]);
+  auto with zarith.
+apply trans_equal with ([|A|] ^ p1 mod [|b|])%Z; auto.
+rewrite H2.
+rewrite Zpos_mult_morphism; rewrite Zpower_mult; auto with zarith.
+rewrite <- Zpower_mod; auto with zarith.
+rewrite Zmod_small; auto.
+Qed.
+
+
+Fixpoint pow_mod_pred (a:w) (l:dec_prime) {struct l} : w :=
+  match l with
+  | nil => a
+  | (q, p)::l =>
+    if (p ?= 1) then pow_mod_pred a l
+    else 
+      let a' := iter_pos (Ppred p) _ (fun x => pow x q) a in
+      pow_mod_pred a' l
+  end.
+
+Lemma iter_pow_mod_spec : forall q p a, [|a|] = ([|a|] mod [|b|])%Z ->
+  ([|iter_pos p _ (fun x => pow x q) a|] = [|a|]^q^p mod [|b|])%Z.
+intros q1 p1; elim p1; simpl iter_pos; clear p1.
+intros p1 Rec a Ha.
+rewrite(fun x => m_op_spec.(power_mod_spec) x [|x|]);
+  auto with zarith.
+repeat rewrite Rec; auto with zarith.
+match goal with |- (Zpower_pos ?X ?Y mod ?Z = _)%Z => 
+  apply trans_equal with (X ^ Y mod Z)%Z; auto
+end.
+repeat rewrite <- Zpower_mod; auto with zmisc.
+repeat rewrite <- Zpower_mult; auto with zmisc.
+repeat rewrite <- Zpower_mod; auto with zmisc.
+repeat rewrite <- Zpower_mult; auto with zarith zmisc.
+eq_tac; auto.
+eq_tac; auto.
+rewrite Zpos_xI.
+assert (tmp: forall x, (2 * x = x + x)%Z); auto with zarith; rewrite tmp;
+  clear tmp.
+repeat rewrite Zpower_exp; auto with zarith.
+rewrite Zpower_1_r; try ring; auto with misc.
+rewrite Zmod_mod; auto with zarith.
+rewrite Rec; auto with zmisc.
+rewrite Zmod_mod; auto with zarith.
+rewrite Rec; auto with zmisc.
+rewrite Zmod_mod; auto with zarith.
+intros p1 Rec a Ha.
+repeat rewrite Rec; auto with zarith.
+repeat rewrite <- Zpower_mod; auto with zmisc.
+repeat rewrite <- Zpower_mult; auto with zmisc.
+eq_tac; auto.
+eq_tac; auto.
+rewrite Zpos_xO.
+assert (tmp: forall x, (2 * x = x + x)%Z); auto with zarith; rewrite tmp;
+  clear tmp.
+repeat rewrite Zpower_exp; auto with zarith.
+rewrite Zmod_mod; auto with zarith.
+intros a Ha; rewrite Zpower_1_r; auto with zarith.
+rewrite(fun x => m_op_spec.(power_mod_spec) x [|x|]);
+  auto with zarith.
+Qed.
+
+Lemma pow_mod_pred_spec : forall l a,
+  ([|a|] = [|a|] mod [|b|] ->
+  [|pow_mod_pred a l|] = [|a|]^(mkProd_pred l) mod [|b|])%Z. 
+intros l; elim l; simpl pow_mod_pred; simpl mkProd_pred; clear l.
+intros; rewrite Zpower_1_r; auto with zarith.
+intros (p1,q1) l Rec a H; simpl snd; simpl fst.
+case (q1 ?= 1)%P; auto with zarith.
+rewrite Rec; auto.
+rewrite iter_pow_mod_spec; auto with zarith.
+rewrite times_Zmult; rewrite pow_Zpower.
+rewrite <- Zpower_mod; auto with zarith.
+rewrite Zpower_mult; auto with zarith.
+rewrite Zmod_small; auto with zarith.
+rewrite iter_pow_mod_spec; auto with zarith.
+match goal with |- context[(?X mod ?Y)%Z] =>
+  case (Z_mod_lt X Y); auto with zarith
+end.
+Qed.
+
+End test.
+
+Require Import Bits.
+
+Definition test_pock N a dec sqrt := 
+  if (2 ?< N) then
+    let Nm1 := Ppred N in
+    let F1 := mkProd dec in
+    match (Nm1 / F1)%P with
+    | (Npos R1, N0) =>
+      if is_odd R1 then
+        if is_even F1 then
+          if (1 ?< a) then
+            let (s,r') := (R1 / (xO F1))%P in
+            match r' with
+            | Npos r =>
+              if (a ?< N) then
+              let op := cmk_op (Peano.pred (nat_of_P (get_height 31 (plength N)))) in
+              let wN := znz_of_Z op (Zpos N) in
+              let wa := znz_of_Z op (Zpos a) in
+              let w1 := znz_of_Z op 1 in
+              let mod_op := make_mod_op op wN in
+              let pow := mod_op.(power_mod) in
+              let ttimes := mod_op.(mul_mod) in 
+              let pred:= mod_op.(pred_mod) in
+              let gcd:= ZnZ.gcd in
+              let A := pow_mod_pred _ mod_op (pow wa R1) dec in
+              match all_pow_mod _ mod_op w1 A dec with
+              | (p, aNm1) =>
+                match ZnZ.to_Z aNm1 with 
+                  (Zpos xH) => 
+                   match ZnZ.to_Z (gcd p wN) with 
+                   (Zpos xH) => 
+                    if check_s_r s r sqrt then 
+		      (N ?< (times ((times ((xO F1)+r+1) F1) + r) F1) + 1)
+                    else false
+                   | _ => false
+                   end
+                 | _ => false
+                end             
+              end else false
+            | _ => false
+            end
+	  else false
+        else false 
+      else false
+    | _=> false
+    end      
+  else false.
+
+Lemma test_pock_correct : forall N a dec sqrt,
+   (forall k, In k dec -> prime (Zpos (fst k))) ->
+   test_pock N a dec sqrt = true ->
+   prime N.
+unfold test_pock;intros N a dec sqrt H.
+match goal with |- context[if ?x then _ else _] =>
+  case_eq x; intros If1; auto
+end.
+2: intros; discriminate.
+match goal with H: (?X ?< ?Y) = true |- _ =>
+  generalize (is_lt_spec X Y); rewrite H; clear H; intros H
+end.
+generalize (div_eucl_spec (Ppred N) (mkProd dec));
+ destruct ((Ppred N) / (mkProd dec))%P as (R1,n).
+simpl fst; simpl snd; intros (H1, H2).
+destruct R1 as [ |R1].
+intros; discriminate.
+destruct n.
+2: intros; discriminate.
+match goal with |- context[if ?x then _ else _] =>
+  case_eq x; intros If2; auto
+end.
+assert (If0: Zodd R1).
+apply is_odd_Zodd; auto.
+clear If2; rename If0 into If2.
+2: intros; discriminate.
+match goal with |- context[if ?x then _ else _] =>
+  case_eq x; intros If3; auto
+end.
+assert (If0: Zeven (mkProd dec)).
+apply is_even_Zeven; auto.
+clear If3; rename If0 into If3.
+2: intros; discriminate.
+match goal with |- context[if ?x then _ else _] =>
+  case_eq x; intros If4; auto
+end.
+match goal with H: (?X ?< ?Y) = true |- _ =>
+  generalize (is_lt_spec X Y); rewrite H; clear H; intros H
+end.
+2: intros; discriminate.
+generalize (div_eucl_spec R1 (xO (mkProd dec)));
+ destruct ((R1 / xO (mkProd dec))%P) as (s,r'); simpl fst;
+ simpl snd; intros (H3, H4).
+destruct r' as [ |r].
+intros; discriminate.
+match goal with |- context[if ?x then _ else _] =>
+  case_eq x; intros If5; auto
+end.
+match goal with H: (?X ?< ?Y) = true |- _ =>
+  generalize (is_lt_spec X Y); rewrite H; clear H; intros H
+end.
+2: intros; discriminate.
+set (bb := Peano.pred (nat_of_P (get_height 31 (plength N)))).
+set (w_op := cmk_op bb).
+assert (op_spec: ZnZ.Specs w_op).
+unfold bb, w_op; apply cmk_spec; auto.
+assert (F0: N < DoubleType.base (ZnZ.digits w_op)).
+  apply Zlt_le_trans with (1 := plength_correct N).
+  unfold w_op, DoubleType.base.
+  rewrite cmk_op_digits.
+  apply Zpower_le_monotone; split; auto with zarith.
+  generalize (get_height_correct 31 (plength N)); unfold bb.
+  set (p := plength N).
+  replace (Z_of_nat (Peano.pred (nat_of_P (get_height 31 p)))) with
+       ((Zpos (get_height 31 p) - 1) ); auto with zarith.
+  rewrite pred_of_minus; rewrite inj_minus1; auto with zarith.
+  rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto with zarith.
+  generalize (lt_O_nat_of_P (get_height 31 p)); auto with zarith.
+assert (F1: ZnZ.to_Z (ZnZ.of_Z N) = N).
+rewrite ZnZ.of_Z_correct; auto with zarith.
+assert (F2: 1 < ZnZ.to_Z (ZnZ.of_Z N)).
+rewrite F1; auto with zarith.
+assert (F3: 0 < ZnZ.to_Z (ZnZ.of_Z N)); auto with zarith.
+assert (F4: ZnZ.to_Z (ZnZ.of_Z a) = a).
+rewrite ZnZ.of_Z_correct; auto with zarith.
+assert (F5: ZnZ.to_Z (ZnZ.of_Z 1) = 1).
+rewrite ZnZ.of_Z_correct; auto with zarith.
+assert (F6: N - 1 = (R1 * mkProd_pred dec)%positive * mkProd' dec).
+rewrite Zpos_mult.
+rewrite <- Zmult_assoc; rewrite mkProd_pred_mkProd; auto with zarith.
+simpl in H1; rewrite Zpos_mult in H1; rewrite <- H1; rewrite Ppred_Zminus;
+  auto with zarith.
+assert (m_spec: mod_spec w_op (znz_of_Z w_op N) 
+                  (make_mod_op w_op (znz_of_Z w_op N))).
+apply make_mod_spec; auto with zarith.
+match goal with |- context[all_pow_mod ?x ?y ?z ?t ?u] =>
+  generalize (fst_all_pow_mod x w_op op_spec _ F3 _ m_spec 
+               u (znz_of_Z w_op a) (R1*mkProd_pred dec) z t);
+  generalize (snd_all_pow_mod x w_op op_spec _ F3 _ m_spec u z t);
+  fold bb w_op;
+  case (all_pow_mod x y z t u); simpl fst; simpl snd 
+end.
+intros prod aNm1; intros H5 H6.
+case_eq (ZnZ.to_Z aNm1).
+intros; discriminate.
+2: intros; discriminate.
+intros p; case p; clear p.
+intros; discriminate.
+intros; discriminate.
+intros If6.
+case_eq (ZnZ.to_Z (ZnZ.gcd prod (znz_of_Z w_op N))).
+intros; discriminate.
+2: intros; discriminate.
+intros p; case p; clear p.
+intros; discriminate.
+intros; discriminate.
+intros If7.
+match goal with |- context[if ?x then _ else _] =>
+  case_eq x; intros If8; auto
+end.
+2: intros; discriminate.
+intros If9.
+match goal with H: (?X ?< ?Y) = true |- _ =>
+  generalize (is_lt_spec X Y); rewrite H; clear H; intros H
+end.
+assert (U1: N - 1 = mkProd dec * R1).
+rewrite <- Ppred_Zminus in H1; auto with zarith.
+rewrite H1; simpl.
+repeat rewrite Zpos_mult; auto with zarith.
+assert (HH:Z_of_N s = R1 / (2 * mkProd dec) /\ Zpos r =  R1 mod (2 * mkProd dec)).
+apply mod_unique with (2 * mkProd dec);auto with zarith.
+apply Z_mod_lt; auto with zarith.
+rewrite <- Z_div_mod_eq; auto with zarith.
+rewrite H3.
+rewrite (Zpos_xO (mkProd dec)).
+simpl Z_of_N; ring.
+case HH; clear HH; intros HH1 HH2.
+apply PocklingtonExtra with (F1:=mkProd dec) (R1:=R1) (m:=1);
+  auto with zmisc zarith.
+case (Zle_lt_or_eq 1 (mkProd dec)); auto with zarith.
+simpl in H2; auto with zarith.
+intros HH; contradict If3; rewrite <- HH.
+apply Zodd_not_Zeven; red; auto.
+intros p; case p; clear p.
+intros HH; contradict HH.
+apply not_prime_0.
+2: intros p (V1, _); contradict V1; apply Zle_not_lt; red; simpl; intros;
+     discriminate.
+intros p Hprime Hdec; exists (Zpos a);repeat split; auto with zarith.
+apply trans_equal with (2 := If6).
+rewrite H5.
+rewrite pow_mod_pred_spec with (2 := m_spec); auto with zarith.
+rewrite F1.
+rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith.
+change (znz_of_Z w_op a) with (ZnZ.of_Z a).
+change (znz_of_Z w_op N) with (ZnZ.of_Z N).
+rewrite F1; rewrite F4.
+rewrite <- Zpower_mod; auto with zarith.
+rewrite <- Zpower_mult; auto with zarith.
+rewrite mkProd_pred_mkProd; auto with zarith.
+rewrite U1; rewrite Zmult_comm.
+rewrite Zpower_mult; auto with zarith.
+rewrite <- Zpower_mod; auto with zarith.
+change (znz_of_Z w_op a) with (ZnZ.of_Z a).
+change (znz_of_Z w_op N) with (ZnZ.of_Z N).
+rewrite F1; rewrite F4; rewrite Zmod_small; auto with zarith.
+rewrite Zmod_small; auto with zarith.
+rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith.
+match goal with |- context[?X mod ?Y] =>
+  case (Z_mod_lt X Y); auto with zarith
+end.
+change (znz_of_Z w_op a) with (ZnZ.of_Z a).
+change (znz_of_Z w_op N) with (ZnZ.of_Z N).
+rewrite F1; rewrite F4; rewrite Zmod_small; auto with zarith.
+rewrite pow_mod_pred_spec with (2 := m_spec); auto with zarith.
+match goal with |- context[?X mod ?Y] =>
+  case (Z_mod_lt X Y); auto with zarith
+end.
+rewrite Zmod_small; auto with zarith.
+rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith.
+match goal with |- context[?X mod ?Y] =>
+  case (Z_mod_lt X Y); auto with zarith
+end.
+change (znz_of_Z w_op a) with (ZnZ.of_Z a).
+change (znz_of_Z w_op N) with (ZnZ.of_Z N).
+rewrite F1; rewrite F4; rewrite Zmod_small; auto with zarith.
+match type of H6 with _ -> _ -> ?X =>
+  assert (tmp: X); [apply H6 | clear H6; rename tmp into H6];
+  auto with zarith
+end.
+rewrite F1.
+change (znz_of_Z w_op 1) with (ZnZ.of_Z 1).
+rewrite F5; rewrite Zmod_small; auto with zarith.
+rewrite pow_mod_pred_spec with (2 := m_spec); auto with zarith.
+change (znz_of_Z w_op a) with (ZnZ.of_Z a).
+change (znz_of_Z w_op N) with (ZnZ.of_Z N).
+repeat (rewrite F1 || rewrite F4).
+rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith.
+change (znz_of_Z w_op a) with (ZnZ.of_Z a).
+change (znz_of_Z w_op N) with (ZnZ.of_Z N).
+repeat (rewrite F1 || rewrite F4).
+rewrite Zpos_mult; rewrite <- Zpower_mod; auto with zarith.
+rewrite Zpower_mult; auto with zarith.
+change (znz_of_Z w_op a) with (ZnZ.of_Z a).
+change (znz_of_Z w_op N) with (ZnZ.of_Z N).
+repeat (rewrite F1 || rewrite F4).
+rewrite Zmod_small; auto with zarith.
+change (znz_of_Z w_op a) with (ZnZ.of_Z a).
+change (znz_of_Z w_op N) with (ZnZ.of_Z N).
+repeat (rewrite F1 || rewrite F4).
+rewrite Zmod_small; auto with zarith.
+rewrite (power_mod_spec m_spec) with (t := a); auto with zarith.
+match goal with |- context[?X mod ?Y] =>
+  case (Z_mod_lt X Y); auto with zarith
+end.
+change (znz_of_Z w_op a) with (ZnZ.of_Z a).
+change (znz_of_Z w_op N) with (ZnZ.of_Z N).
+repeat (rewrite F1 || rewrite F4); auto.
+rewrite Zmod_small; auto with zarith.
+change (znz_of_Z w_op N) with (ZnZ.of_Z N); auto.
+auto with zarith.
+change (znz_of_Z w_op a) with (ZnZ.of_Z a) in H6.
+change (znz_of_Z w_op N) with (ZnZ.of_Z N) in H6.
+change (znz_of_Z w_op 1) with (ZnZ.of_Z 1) in H6.
+rewrite F5 in H6; rewrite F1 in H6; rewrite F4 in H6.
+case in_mkProd_prime_div_in with (3 := Hdec); auto.
+intros p1 Hp1.
+rewrite <- F6 in H6.
+apply Zis_gcd_gcd; auto with zarith.
+change (rel_prime (a ^ ((N - 1) / p) - 1) N).
+match type of H6 with _ = ?X mod _ =>
+  apply rel_prime_div with (p := X); auto with zarith
+end.
+apply rel_prime_mod_rev; auto with zarith.
+red.
+pattern 1 at 4; rewrite <- If7; rewrite <- H6.
+pattern N at 2; rewrite <- F1.
+apply ZnZ.spec_gcd; auto with zarith.
+assert (foldtmp: forall (A B: Set) (f: A -> B -> A) (P: A -> Prop) l a b,
+  In b l -> (forall x, P (f x b)) ->
+  (forall x y, P x -> P (f x y)) ->
+  P (fold_left f l a)).
+assert (foldtmp0: forall (A B: Set) (f: A -> B -> A) (P: A -> Prop) l a,
+  P a ->
+  (forall x y, P x -> P (f x y)) ->
+  P (fold_left f l a)).
+intros A B f P l; elim l; simpl; auto.
+intros A B f P l; elim l; simpl; auto.
+intros a1 b HH; case HH.
+intros a1 l1 Rec a2 b [V|V] V1 V2; subst; auto.
+apply foldtmp0; auto.
+apply Rec with (b := b); auto with zarith.
+match goal with |- context [fold_left ?f _ _] =>
+ apply (foldtmp _ _ f (fun k => Zdivide (a ^ ((N - 1) / p) - 1) k)) 
+   with (b := (p, p1)); auto with zarith
+end.
+rewrite <- HH2.
+clear F0; match goal with H: ?X < ?Y |- ?X < ?Z =>
+ replace Z with Y; auto
+end.
+repeat (rewrite Zpos_plus || rewrite Zpos_mult || rewrite times_Zmult).
+rewrite Zpos_xO; ring.
+rewrite <- HH1; rewrite <- HH2.
+apply check_s_r_correct with sqrt; auto.
+Qed.
+
+(* Simple version of pocklington for primo *)
+Definition test_spock N a dec := 
+  if (2 ?< N) then
+    let Nm1 := Ppred N in
+    let F1 := mkProd dec in
+    match (Nm1 / F1)%P with
+    | (Npos R1, N0) =>
+          if (1 ?< a) then
+            if (a ?< N) then
+              if (N ?< F1 * F1) then
+              let op := cmk_op (Peano.pred (nat_of_P (get_height 31 (plength N)))) in
+              let wN := znz_of_Z op (Zpos N) in
+              let wa := znz_of_Z op (Zpos a) in
+              let w1 := znz_of_Z op 1 in
+              let mod_op := make_mod_op op wN in
+              let pow := mod_op.(power_mod) in
+              let ttimes := mod_op.(mul_mod) in 
+              let pred:= mod_op.(pred_mod) in
+              let gcd:= ZnZ.gcd in
+              let A := pow_mod_pred _ mod_op (pow wa R1) dec in
+              match all_pow_mod _ mod_op w1 A dec with
+              | (p, aNm1) =>
+                match ZnZ.to_Z aNm1 with 
+                  (Zpos xH) => 
+                   match ZnZ.to_Z (gcd p wN) with 
+                   (Zpos xH) => true
+                   | _ => false
+                   end
+                 | _ => false
+                end             
+              end else false
+           else false
+         else false
+    | _=> false
+    end      
+  else false.
+
+Lemma test_spock_correct : forall N a dec,
+   (forall k, In k dec -> prime (Zpos (fst k))) ->
+   test_spock N a dec = true ->
+   prime N.
+unfold test_spock;intros N a dec H.
+match goal with |- context[if ?x then _ else _] =>
+  case_eq x; intros If1; auto
+end.
+2: intros; discriminate.
+match goal with H: (?X ?< ?Y) = true |- _ =>
+  generalize (is_lt_spec X Y); rewrite H; clear H; intros H
+end.
+generalize (div_eucl_spec (Ppred N) (mkProd dec));
+ destruct ((Ppred N) / (mkProd dec))%P as (R1,n).
+simpl fst; simpl snd; intros (H1, H2).
+destruct R1 as [ |R1].
+intros; discriminate.
+destruct n.
+2: intros; discriminate.
+match goal with |- context[if ?x then _ else _] =>
+  case_eq x; intros If2; auto
+end.
+match goal with H: (?X ?< ?Y) = true |- _ =>
+  generalize (is_lt_spec X Y); rewrite H; clear H; intros H
+end.
+2: intros; discriminate.
+(*
+set (bb := pred (nat_of_P (get_height 31 (plength N)))).
+set (w_op := cmk_op bb).
+assert (op_spec: znz_spec w_op).
+unfold bb, w_op; apply cmk_spec; auto.
+assert (F0: N < Basic_type.base (znz_digits w_op)).
+  apply Zlt_le_trans with (1 := plength_correct N).
+  unfold w_op, Basic_type.base.
+  rewrite cmk_op_digits.
+  apply Zpower_le_monotone; split; auto with zarith.
+  generalize (get_height_correct 31 (plength N)); unfold bb.
+  set (p := plength N).
+  replace (Z_of_nat (pred (nat_of_P (get_height 31 p)))) with
+       ((Zpos (get_height 31 p) - 1) ); auto with zarith.
+  rewrite pred_of_minus; rewrite inj_minus1; auto with zarith.
+  rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto with zarith.
+  generalize (lt_O_nat_of_P (get_height 31 p)); auto with zarith.
+*)
+set (bb := Peano.pred (nat_of_P (get_height 31 (plength N)))).
+set (w_op := cmk_op bb).
+assert (op_spec: ZnZ.Specs w_op).
+unfold bb, w_op; apply cmk_spec; auto.
+match goal with |- context[if ?x then _ else _] =>
+  case_eq x; intros If3; auto
+end.
+match goal with H: (?X ?< ?Y) = true |- _ =>
+  generalize (is_lt_spec X Y); rewrite H; clear H; intros H
+end.
+match goal with |- context[if ?x then _ else _] =>
+  case_eq x; intros If4; auto
+end.
+match goal with H: (?X ?< ?Y) = true |- _ =>
+  generalize (is_lt_spec X Y); rewrite H; clear H; intros H
+end.
+assert (F0: N < DoubleType.base (ZnZ.digits w_op)).
+  apply Zlt_le_trans with (1 := plength_correct N).
+  unfold w_op, DoubleType.base.
+  rewrite cmk_op_digits.
+  apply Zpower_le_monotone; split; auto with zarith.
+  generalize (get_height_correct 31 (plength N)); unfold bb.
+  set (p := plength N).
+  replace (Z_of_nat (Peano.pred (nat_of_P (get_height 31 p)))) with
+       ((Zpos (get_height 31 p) - 1) ); auto with zarith.
+  rewrite pred_of_minus; rewrite inj_minus1; auto with zarith.
+  rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto with zarith.
+  generalize (lt_O_nat_of_P (get_height 31 p)); auto with zarith.
+assert (F1: ZnZ.to_Z (ZnZ.of_Z N) = N).
+rewrite ZnZ.of_Z_correct; auto with zarith.
+assert (F2: 1 < ZnZ.to_Z (ZnZ.of_Z N)).
+rewrite F1; auto with zarith.
+assert (F3: 0 < ZnZ.to_Z (ZnZ.of_Z N)); auto with zarith.
+assert (F4: ZnZ.to_Z (ZnZ.of_Z a) = a).
+rewrite ZnZ.of_Z_correct; auto with zarith.
+assert (F5: ZnZ.to_Z (ZnZ.of_Z 1) = 1).
+rewrite ZnZ.of_Z_correct; auto with zarith.
+assert (F6: N - 1 = (R1 * mkProd_pred dec)%positive * mkProd' dec).
+rewrite Zpos_mult.
+rewrite <- Zmult_assoc; rewrite mkProd_pred_mkProd; auto with zarith.
+simpl in H1; rewrite Zpos_mult in H1; rewrite <- H1; rewrite Ppred_Zminus;
+  auto with zarith.
+assert (m_spec: mod_spec w_op (znz_of_Z w_op N) 
+                  (make_mod_op w_op (znz_of_Z w_op N))).
+apply make_mod_spec; auto with zarith.
+match goal with |- context[all_pow_mod ?x ?y ?z ?t ?u] =>
+  generalize (fst_all_pow_mod x w_op op_spec _ F3 _ m_spec 
+               u (znz_of_Z w_op a) (R1*mkProd_pred dec) z t);
+  generalize (snd_all_pow_mod x w_op op_spec _ F3 _ m_spec u z t);
+  fold bb w_op;
+  case (all_pow_mod x y z t u); simpl fst; simpl snd 
+end.
+2: intros; discriminate.
+intros prod aNm1; intros H5 H6.
+case_eq (ZnZ.to_Z aNm1).
+intros; discriminate.
+2: intros; discriminate.
+intros p; case p; clear p.
+intros; discriminate.
+intros; discriminate.
+intros If5.
+case_eq (ZnZ.to_Z (ZnZ.gcd prod (znz_of_Z w_op N))).
+intros; discriminate.
+2: intros; discriminate.
+intros p; case p; clear p.
+intros; discriminate.
+intros; discriminate.
+intros If6 _.
+assert (U1: N - 1 = mkProd dec * R1).
+rewrite <- Ppred_Zminus in H1; auto with zarith.
+rewrite H1; simpl.
+repeat rewrite Zpos_mult; auto with zarith.
+apply PocklingtonCorollary1 with (F1:=mkProd dec) (R1:=R1);
+  auto with zmisc zarith.
+case (Zle_lt_or_eq 1 (mkProd dec)); auto with zarith.
+simpl in H2; auto with zarith.
+intros HH; contradict If4; rewrite Zpos_mult_morphism;
+  rewrite <- HH.
+apply Zle_not_lt; auto with zarith.
+intros p; case p; clear p.
+intros HH; contradict HH.
+apply not_prime_0.
+2: intros p (V1, _); contradict V1; apply Zle_not_lt; red; simpl; intros;
+     discriminate.
+intros p Hprime Hdec; exists (Zpos a);repeat split; auto with zarith.
+apply trans_equal with (2 := If5).
+rewrite H5.
+rewrite pow_mod_pred_spec with (2 := m_spec); auto with zarith.
+rewrite F1.
+rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith.
+change (znz_of_Z w_op N) with (ZnZ.of_Z N).
+change (znz_of_Z w_op a) with (ZnZ.of_Z a).
+rewrite F1; rewrite F4.
+rewrite <- Zpower_mod; auto with zarith.
+rewrite <- Zpower_mult; auto with zarith.
+rewrite mkProd_pred_mkProd; auto with zarith.
+rewrite U1; rewrite Zmult_comm.
+rewrite Zpower_mult; auto with zarith.
+rewrite <- Zpower_mod; auto with zarith.
+change (znz_of_Z w_op N) with (ZnZ.of_Z N).
+change (znz_of_Z w_op a) with (ZnZ.of_Z a).
+rewrite F1; rewrite F4; rewrite Zmod_small; auto with zarith.
+change (znz_of_Z w_op N) with (ZnZ.of_Z N).
+change (znz_of_Z w_op a) with (ZnZ.of_Z a).
+rewrite Zmod_small; auto with zarith.
+rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith.
+match goal with |- context[?X mod ?Y] =>
+  case (Z_mod_lt X Y); auto with zarith
+end.
+change (znz_of_Z w_op N) with (ZnZ.of_Z N).
+change (znz_of_Z w_op a) with (ZnZ.of_Z a).
+rewrite F1; rewrite F4; rewrite Zmod_small; auto with zarith.
+rewrite pow_mod_pred_spec with (2 := m_spec); auto with zarith.
+match goal with |- context[?X mod ?Y] =>
+  case (Z_mod_lt X Y); auto with zarith
+end.
+rewrite Zmod_small; auto with zarith.
+rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith.
+match goal with |- context[?X mod ?Y] =>
+  case (Z_mod_lt X Y); auto with zarith
+end.
+change (znz_of_Z w_op N) with (ZnZ.of_Z N).
+change (znz_of_Z w_op a) with (ZnZ.of_Z a).
+rewrite F1; rewrite F4; rewrite Zmod_small; auto with zarith.
+match type of H6 with _ -> _ -> ?X =>
+  assert (tmp: X); [apply H6 | clear H6; rename tmp into H6];
+  auto with zarith
+end.
+rewrite F1.
+change (znz_of_Z w_op 1) with (ZnZ.of_Z 1).
+rewrite F5; rewrite Zmod_small; auto with zarith.
+rewrite pow_mod_pred_spec with (2 := m_spec); auto with zarith.
+change (znz_of_Z w_op N) with (ZnZ.of_Z N).
+change (znz_of_Z w_op a) with (ZnZ.of_Z a).
+repeat (rewrite F1 || rewrite F4).
+rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith.
+change (znz_of_Z w_op N) with (ZnZ.of_Z N).
+repeat (rewrite F1 || rewrite F4).
+rewrite Zpos_mult; rewrite <- Zpower_mod; auto with zarith.
+rewrite Zpower_mult; auto with zarith.
+change (znz_of_Z w_op N) with (ZnZ.of_Z N).
+repeat (rewrite F1 || rewrite F4).
+rewrite Zmod_small; auto with zarith.
+rewrite Zmod_small; auto with zarith.
+rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith.
+match goal with |- context[?X mod ?Y] =>
+  case (Z_mod_lt X Y); auto with zarith
+end.
+change (znz_of_Z w_op N) with (ZnZ.of_Z N).
+change (znz_of_Z w_op a) with (ZnZ.of_Z a).
+repeat (rewrite F1 || rewrite F4).
+rewrite Zmod_small; auto with zarith.
+change (znz_of_Z w_op N) with (ZnZ.of_Z N) in H6.
+change (znz_of_Z w_op a) with (ZnZ.of_Z a) in H6.
+change (znz_of_Z w_op 1) with (ZnZ.of_Z 1) in H6.
+rewrite F5 in H6; rewrite F1 in H6; rewrite F4 in H6.
+case in_mkProd_prime_div_in with (3 := Hdec); auto.
+intros p1 Hp1.
+rewrite <- F6 in H6.
+apply Zis_gcd_gcd; auto with zarith.
+change (rel_prime (a ^ ((N - 1) / p) - 1) N).
+match type of H6 with _ = ?X mod _ =>
+  apply rel_prime_div with (p := X); auto with zarith
+end.
+apply rel_prime_mod_rev; auto with zarith.
+red.
+pattern 1 at 4; rewrite <- If6; rewrite <- H6.
+pattern N at 2; rewrite <- F1.
+apply ZnZ.spec_gcd; auto with zarith.
+assert (foldtmp: forall (A B: Set) (f: A -> B -> A) (P: A -> Prop) l a b,
+  In b l -> (forall x, P (f x b)) ->
+  (forall x y, P x -> P (f x y)) ->
+  P (fold_left f l a)).
+assert (foldtmp0: forall (A B: Set) (f: A -> B -> A) (P: A -> Prop) l a,
+  P a ->
+  (forall x y, P x -> P (f x y)) ->
+  P (fold_left f l a)).
+intros A B f P l; elim l; simpl; auto.
+intros A B f P l; elim l; simpl; auto.
+intros a1 b HH; case HH.
+intros a1 l1 Rec a2 b [V|V] V1 V2; subst; auto.
+apply foldtmp0; auto.
+apply Rec with (b := b); auto with zarith.
+match goal with |- context [fold_left ?f _ _] =>
+ apply (foldtmp _ _ f (fun k => Zdivide (a ^ ((N - 1) / p) - 1) k)) 
+   with (b := (p, p1)); auto with zarith
+end.
+intros; discriminate.
+Qed.
+
+Fixpoint test_Certif (lc : Certif) : bool :=
+  match lc with
+  | nil => true
+  | (Proof_certif _ _) :: lc => test_Certif lc
+  | (Lucas_certif n p) :: lc =>
+     let xx := test_Certif lc in
+     if xx then
+     let yy := gt2 p in 
+     if yy then
+       match p with 
+         Zpos p1 => 
+           let zz := Mp p in
+           match zz with
+          | Zpos n' =>
+             if (n ?= n')%P then
+               let tt :=  lucas p1 in
+               match tt with
+               | Z0 => true
+               | _ => false
+               end
+             else false
+           | _ => false
+           end
+         | _ => false
+       end
+    else false 
+    else false
+  | (Pock_certif n a dec sqrt) :: lc =>
+    let xx := test_pock n a dec sqrt in 
+    if xx then 
+      let yy := all_in lc dec in
+      (if yy then test_Certif lc else false)
+    else false
+  | (SPock_certif n a dec) :: lc =>
+    let xx :=test_spock n a dec in
+    if xx then
+      let yy := all_in lc dec in
+      (if yy then test_Certif lc else false)
+    else false
+  | (Ell_certif n ss l a b x y) :: lc =>
+    let xx := ell_test n ss l a b x y in
+    if xx then
+     let yy :=  all_in lc l in 
+     if yy then test_Certif lc else false
+    else false
+  end.
+
+Lemma test_Certif_In_Prime : 
+  forall lc, test_Certif lc = true -> 
+   forall c, In c lc -> prime (nprim c).
+intros lc; elim lc; simpl; auto.
+intros _ c H; case H.
+intros a; case a; simpl; clear a lc.
+intros N p l Rec H c [H1 | H1]; subst; auto with arith.
+intros n p l; case (test_Certif l); auto with zarith.
+2: intros; discriminate.
+intros H H1 c [H2 | H2]; subst; auto with arith.
+simpl nprim.
+generalize H1; clear H1.
+case_eq (gt2 p).
+2: intros; discriminate.
+case p; clear p; try (intros; discriminate; fail).
+unfold gt2; intros p H1.
+match goal with H: (?X ?< ?Y) = true |- _ =>
+  generalize (is_lt_spec X Y); rewrite H; clear H; intros H
+end.
+unfold Mp; case_eq (2 ^ p  -1); try (intros; discriminate; fail).
+intros p1 Hp1.
+case_eq (n ?= p1)%P; try rewrite <- Hp1.
+2: intros; discriminate.
+intros H2.
+match goal with H: (?X ?= ?Y)%P = true |- _ =>
+  generalize (is_eq_eq _ _ H); clear H; intros H
+end.
+generalize (lucas_prime H1); rewrite Hp1; rewrite <- H2.
+case (lucas p); try (intros; discriminate; fail); auto.
+intros N a d p l H.
+generalize (test_pock_correct N a d p).
+case (test_pock N a d p); auto.
+2: intros; discriminate.
+generalize (all_in_In l d).
+case (all_in l d).
+2: intros; discriminate.
+intros H1 H2 H3 c [H4 | H4]; subst; simpl; auto.
+apply H2; auto.
+intros k Hk.
+case H1 with (2 := Hk); auto.
+intros x (Hx1, Hx2); rewrite Hx2; auto.
+intros N a d l H.
+generalize (test_spock_correct N a d).
+case test_spock; auto.
+2: intros; discriminate.
+generalize (all_in_In l d).
+case (all_in l d).
+2: intros; discriminate.
+intros H1 H2 H3 c [H4 | H4]; subst; simpl; auto.
+apply H2; auto.
+intros k Hk.
+case H1 with (2 := Hk); auto.
+intros x (Hx1, Hx2); rewrite Hx2; auto.
+intros N S l A B x y l1.
+generalize (all_in_In l1 l).
+generalize (ell_test_correct N S l A B x y).
+case ell_test.
+case all_in; auto.
+intros H1 H2 H3 H4 c [H5 | H5]; try subst c; simpl; auto.
+apply H1.
+intros p Hp; case (H2 (refl_equal true) p); auto.
+intros x1 (Hx1, Hx2); rewrite Hx2; auto.
+intros; discriminate.
+intros; discriminate.
+Qed.
+
+Lemma Pocklington_refl : 
+  forall c lc, test_Certif (c::lc) = true -> prime (nprim c).
+Proof.
+ intros c lc Heq;apply test_Certif_In_Prime with (c::lc);trivial;simpl;auto.
+Qed.
+
diff --git a/coqprime/num/W.v b/coqprime/num/W.v
new file mode 100644
index 000000000..d26e2657e
--- /dev/null
+++ b/coqprime/num/W.v
@@ -0,0 +1,200 @@
+
+(*************************************************************)
+(*      This file is distributed under the terms of the      *)
+(*      GNU Lesser General Public License Version 2.1        *)
+(*************************************************************)
+(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
+(*************************************************************)
+
+Set Implicit Arguments.
+Require Import CyclicAxioms DoubleCyclic BigN Cyclic31 Int31.
+Require Import ZArith ZCAux.
+
+(* ** Type of words ** *)
+
+
+(* Make the words *)
+
+Definition mk_word: forall (w: Type) (n:nat), Type.
+fix 2.
+intros w n; case n; simpl.
+exact int31.
+intros n1; exact (zn2z (mk_word w n1)).
+Defined.
+
+(* Make the op *)
+Fixpoint mk_op (w : Type) (op : ZnZ.Ops w) (n : nat) {struct n} :
+  ZnZ.Ops (word w n) :=
+  match n return (ZnZ.Ops (word w n)) with
+  | O => op
+  | S n1 => mk_zn2z_ops_karatsuba (mk_op op n1)
+  end.
+
+Theorem mk_op_digits: forall w (op: ZnZ.Ops w) n, 
+  (Zpos (ZnZ.digits (mk_op op n)) = 2 ^ Z_of_nat n * Zpos (ZnZ.digits op))%Z.
+intros w op n; elim n; simpl mk_op; auto; clear n.
+intros n Rec; simpl ZnZ.digits.
+rewrite Zpos_xO; rewrite Rec.
+rewrite Zmult_assoc; apply f_equal2 with (f := Zmult); auto.
+rewrite inj_S; unfold Zsucc; rewrite Zplus_comm.
+rewrite Zpower_exp; auto with zarith.
+Qed.
+
+Theorem digits_pos: forall w (op: ZnZ.Ops w) n,
+  (1 < Zpos (ZnZ.digits op) ->  1 < Zpos (ZnZ.digits (mk_op op n)))%Z.
+intros w op n H.
+rewrite mk_op_digits.
+rewrite <- (Zmult_1_r 1).
+apply Zle_lt_trans with (2 ^ (Z_of_nat n) * 1)%Z.
+apply Zmult_le_compat_r; auto with zarith.
+rewrite <- (Zpower_0_r 2).
+apply Zpower_le_monotone; auto with zarith.
+apply Zmult_lt_compat_l; auto with zarith.
+Qed.
+
+Fixpoint mk_spec (w : Type) (op : ZnZ.Ops w) (op_spec : ZnZ.Specs op) 
+    (H: (1 < Zpos (ZnZ.digits op))%Z)  (n : nat)
+            {struct n} : ZnZ.Specs (mk_op op n) :=
+  match n return (ZnZ.Specs (mk_op op n)) with
+  | O => op_spec
+  | S n1 =>
+      @mk_zn2z_specs_karatsuba (word w n1) (mk_op op n1)
+        (* (digits_pos op n1 H) *) (mk_spec op_spec H n1)
+  end.
+
+(* ** Operators ** *)
+Definition w31_1_op := mk_zn2z_ops int31_ops.           
+Definition w31_2_op := mk_zn2z_ops w31_1_op.
+Definition w31_3_op := mk_zn2z_ops w31_2_op.
+Definition w31_4_op := mk_zn2z_ops_karatsuba w31_3_op.
+Definition w31_5_op := mk_zn2z_ops_karatsuba w31_4_op.
+Definition w31_6_op := mk_zn2z_ops_karatsuba w31_5_op.
+Definition w31_7_op := mk_zn2z_ops_karatsuba w31_6_op.
+Definition w31_8_op := mk_zn2z_ops_karatsuba w31_7_op.
+Definition w31_9_op := mk_zn2z_ops_karatsuba w31_8_op.
+Definition w31_10_op := mk_zn2z_ops_karatsuba w31_9_op.
+Definition w31_11_op := mk_zn2z_ops_karatsuba w31_10_op.
+Definition w31_12_op := mk_zn2z_ops_karatsuba w31_11_op.
+Definition w31_13_op := mk_zn2z_ops_karatsuba w31_12_op.
+Definition w31_14_op := mk_zn2z_ops_karatsuba w31_13_op.
+
+Definition cmk_op: forall (n: nat), ZnZ.Ops (word int31 n).
+intros n; case n; clear n.
+exact int31_ops.
+intros n; case n; clear n.
+exact w31_1_op.
+intros n; case n; clear n.
+exact w31_2_op.
+intros n; case n; clear n.
+exact w31_3_op.
+intros n; case n; clear n.
+exact w31_4_op.
+intros n; case n; clear n.
+exact w31_5_op.
+intros n; case n; clear n.
+exact w31_6_op.
+intros n; case n; clear n.
+exact w31_7_op.
+intros n; case n; clear n.
+exact w31_8_op.
+intros n; case n; clear n.
+exact w31_9_op.
+intros n; case n; clear n.
+exact w31_10_op.
+intros n; case n; clear n.
+exact w31_11_op.
+intros n; case n; clear n.
+exact w31_12_op.
+intros n; case n; clear n.
+exact w31_13_op.
+intros n; case n; clear n.
+exact w31_14_op.
+intros n.
+match goal with |- context[S ?X] =>
+ exact (mk_op int31_ops (S X))
+end.
+Defined.
+
+Definition cmk_spec: forall n, ZnZ.Specs (cmk_op n).
+assert (S1: ZnZ.Specs w31_1_op).
+unfold w31_1_op; apply mk_zn2z_specs; auto with zarith.
+exact int31_specs.
+assert (S2: ZnZ.Specs w31_2_op).
+unfold w31_2_op; apply mk_zn2z_specs; auto with zarith.
+assert (S3: ZnZ.Specs w31_3_op).
+unfold w31_3_op; apply mk_zn2z_specs; auto with zarith.
+assert (S4: ZnZ.Specs w31_4_op).
+unfold w31_4_op; apply mk_zn2z_specs_karatsuba; auto with zarith.
+assert (S5: ZnZ.Specs w31_5_op).
+unfold w31_5_op; apply mk_zn2z_specs_karatsuba; auto with zarith.
+assert (S6: ZnZ.Specs w31_6_op).
+unfold w31_6_op; apply mk_zn2z_specs_karatsuba; auto with zarith.
+assert (S7: ZnZ.Specs w31_7_op).
+unfold w31_7_op; apply mk_zn2z_specs_karatsuba; auto with zarith.
+assert (S8: ZnZ.Specs w31_8_op).
+unfold w31_8_op; apply mk_zn2z_specs_karatsuba; auto with zarith.
+assert (S9: ZnZ.Specs w31_9_op).
+unfold w31_9_op; apply mk_zn2z_specs_karatsuba; auto with zarith.
+assert (S10: ZnZ.Specs w31_10_op).
+unfold w31_10_op; apply mk_zn2z_specs_karatsuba; auto with zarith.
+assert (S11: ZnZ.Specs w31_11_op).
+unfold w31_11_op; apply mk_zn2z_specs_karatsuba; auto with zarith.
+assert (S12: ZnZ.Specs w31_12_op).
+unfold w31_12_op; apply mk_zn2z_specs_karatsuba; auto with zarith.
+assert (S13: ZnZ.Specs w31_13_op).
+unfold w31_13_op; apply mk_zn2z_specs_karatsuba; auto with zarith.
+assert (S14: ZnZ.Specs w31_14_op).
+unfold w31_14_op; apply mk_zn2z_specs_karatsuba; auto with zarith.
+intros n; case n; clear n.
+exact int31_specs.
+intros n; case n; clear n.
+exact S1.
+intros n; case n; clear n.
+exact S2.
+intros n; case n; clear n.
+exact S3.
+intros n; case n; clear n.
+exact S4.
+intros n; case n; clear n.
+exact S5.
+intros n; case n; clear n.
+exact S6.
+intros n; case n; clear n.
+exact S7.
+intros n; case n; clear n.
+exact S8.
+intros n; case n; clear n.
+exact S9.
+intros n; case n; clear n.
+exact S10.
+intros n; case n; clear n.
+exact S11.
+intros n; case n; clear n.
+exact S12.
+intros n; case n; clear n.
+exact S13.
+intros n; case n; clear n.
+exact S14.
+intro n.
+simpl cmk_op.
+repeat match goal with |- ZnZ.Specs
+ (mk_zn2z_ops_karatsuba ?X) =>
+  generalize (@mk_zn2z_specs_karatsuba _ X); intros tmp;
+  apply tmp; clear tmp; auto with zarith
+end.
+(*
+apply digits_pos.
+*)
+auto with zarith.
+apply mk_spec.
+exact int31_specs.
+auto with zarith.
+Defined.
+
+
+Theorem cmk_op_digits: forall n, 
+  (Zpos (ZnZ.digits (cmk_op n)) = 2 ^ (Z_of_nat n) * 31)%Z.
+do 15 (intros n; case n; clear n; [try reflexivity | idtac]).
+intros n; unfold cmk_op; lazy beta.
+rewrite mk_op_digits; auto.
+Qed.