
(*************************************************************)
(*      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.

From Bignums Require Import DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv.
From Bignums Require Import DoubleCyclic BigN.
Require Import CyclicAxioms Cyclic31.
Require Import ZArith ZCAux.
Import CyclicAxioms DoubleType DoubleBase.

(* For backward compatibility. The intended value is Set,
   but we use Type when compiling against an old version
   of the standard library. *)
Definition univ_of_cycles : Type.
Proof.
  first [let _ := constr:(word : Set -> nat -> Set) in exact Set | exact Type].
Defined.


Theorem Zpos_pos: forall x, 0 < Zpos x.
red; simpl; auto.
Qed.
Global Hint Resolve Zpos_pos: zarith.

Section Mod_op.

 Variable w : univ_of_cycles.

 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 : core.

 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 Z.compare_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 Z.compare_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 Z.lt_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 Z.lt_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 Z.lt_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 Z.compare_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 Z.le_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 Z.le_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 Z.le_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) by auto with zarith.
 assert (F1: [|n|] < Zpos (ZnZ.digits w_op)).
 case (Zle_or_lt (Zpos (ZnZ.digits w_op)) [|n|]). 2: auto.
 intros H1; contradict Hp1; apply Zle_not_lt; unfold base.
 apply Z.le_trans with (2 ^ [|n|] * 1). 2: 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.
 pattern [|n|]; rewrite <- Zplus_0_r.
 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 ).
 2: 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 Z.lt_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.
 rewrite _w0_is_0; rewrite Zmult_0_l.
 rewrite Zplus_0_l.
 autorewrite with w_rewrite.
 rewrite (fun x y => Zmod_small (x - y)).
 unfold w_zdigits; rewrite ZnZ.spec_zdigits.
 assert (tmp: forall p q, p - (p - q) = q) by (intros; ring).
  rewrite tmp; clear tmp.
 rewrite Zmod_small. reflexivity.
 split. auto with zarith.
 apply Z.le_lt_trans with (2 := U2).
 apply Zdiv_le_upper_bound. auto with zarith.
 apply Z.le_trans with ([|w2|] * (2 ^ 0)).
 simpl Zpower; rewrite Zmult_1_r; reflexivity.
 apply Zmult_le_compat_l. 2: 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|]) by 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 Z.le_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 Z.le_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 Z.le_trans with (2 ^ [|ZnZ.head0 b|] * 1);
   auto with zarith.
 rewrite Zmult_1_r; unfold base; apply Zpower_le_monotone; auto with zarith.
 apply Z.le_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 Z.compare_spec; intros H2;
 match goal with H: context[w_mul_c] |- _ =>
   generalize H; clear H
 end.
 rewrite _w0_is_0.
 unfold w_mul_c, ww_to_Z, w_to_Z, w_digits; rewrite ZnZ.spec_mul_c.
 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.
 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.
 apply Z.lt_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.
 apply Zmult_lt_compat.
 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. 2: 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).
 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 Z.lt_le_trans with Y; auto with zarith
 end.
 apply Z.lt_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 by auto with zarith.
 rewrite <- (Z_div_mult ([|w2|] * [|w3|]) (2 ^ [|n|]))
  by auto with zarith; rewrite Zmult_comm.
 rewrite <- ZnZ.spec_mul_c.
 unfold w_mul_c in H3; unfold ww_to_Z in H3;simpl 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 by auto with zarith.
 rewrite Zplus_mod.
 rewrite Z_mod_mult.
 rewrite Zplus_0_l.
 rewrite Zmod_mod.
 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 Z.compare_spec;
   intros H2;
 match goal with H: context[w_square_c] |- _ =>
   generalize H; clear H
 end; autorewrite with w_rewrite.
 rewrite _w0_is_0.
 unfold w_square_c, ww_to_Z, w_to_Z, w_digits; rewrite ZnZ.spec_square_c.
 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.
 apply Z.lt_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.
 apply Zmult_lt_compat.
 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 by 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 Z.lt_le_trans with Y; auto with zarith
 end.
 apply Z.lt_trans with (2 ^ [|n|] * ([|b|] * [|b|])).
 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 by auto with zarith.
 rewrite <- (Z_div_mult ([|w2|] * [|w2|]) (2 ^ [|n|]))
  by auto with zarith; rewrite Zmult_comm.
 rewrite <- ZnZ.spec_square_c.
 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 by auto with zarith.
 rewrite Zplus_mod.
 rewrite Z_mod_mult.
 rewrite Zplus_0_l.
 rewrite Zmod_mod.
 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.
 rewrite Zmax_right.
 auto with zarith.
 rewrite Zpos_xO.
 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.
 rewrite spec_ww_digits; simpl ww_to_Z.
 change (w_to_Z w0) with [|w0|].
 unfold w0; rewrite ZnZ.spec_0; autorewrite with rm10.
 change (w_to_Z zp) with [|zp|].
 rewrite zp_b.
 rewrite Zmod_small.
 rewrite <- p_p1; ring.
 unfold ww_digits; split.
 rewrite <- p_p1.
 assert (0 < Zpos p1); auto with zarith.
 apply Z.le_lt_trans with (Zpos (xO w_digits)).
 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 : core.

 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.
 absurd (0 < [|x|] * base (ZnZ.digits w_op) + [|y|]).
 unfold w_to_Z, w_digits in H5;auto with zarith.
 match goal with |- _ < ?X + _ =>
  apply Z.lt_le_trans with X; auto with zarith
 end.
 case Zle_lt_or_eq with (1 := H3); clear H3; intros H3. 2: auto with zarith.
 absurd (0 < [|x|] * base (ZnZ.digits w_op) + [|y|]).
 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).
 rewrite p_p1; auto with zarith.
 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_full with (b := 2 ^ Zpos p).
 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)).
   rewrite zp1_b; rewrite <- p_p1.
   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.
 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.
 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 by auto with zarith.
 apply Z.lt_le_trans with (base (ww_digits (ZnZ.digits w_op))).
   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.
 intros H1;
   generalize (high_zero (WW w2 w3)); unfold w_digits;intros tmp;
   simpl fst in tmp; simpl ww_to_Z in tmp.
   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 by auto with zarith.
 apply Z.lt_le_trans with (1 := Hx).
 apply Z.le_trans with (2 ^ Zpos p * 2 ^ Zpos p).
 rewrite p_b; apply Zmult_le_compat_r; auto with zarith.
 rewrite <- Zpower_exp by auto with zarith.
 apply Zpower_le_monotone; auto with zarith.
 split.
 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 by auto with zarith.
 apply Z.lt_le_trans with (base (ww_digits (ZnZ.digits w_op))).
   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 Z.compare_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.
