Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Type Z viewed modulo a particular constant corresponds to Z/nZ

as defined abstractly in CyclicAxioms.

Even if the construction provided here is not reused for building the efficient arbitrary precision numbers, it provides a simple implementation of CyclicAxioms, hence ensuring its coherence.

Set Implicit Arguments.

Require Import Bool.
Require Import ZArith.
Require Import Znumtheory.
Require Import Zpow_facts.
Require Import DoubleType.
Require Import CyclicAxioms.

Local Open Scope Z_scope.

Section ZModulo.

 Variable digits : positive.
 Hypothesis digits_ne_1 : digits <> 1%positive.

 Definition wB := base digits.

 Definition t := Z.
 Definition zdigits := Zpos digits.
 Definition to_Z x := x mod wB.

 Notation "[| x |]" := (to_Z x)  (at level 0, x at level 99).

 Notation "[+| c |]" :=
   (interp_carry 1 wB to_Z c)  (at level 0, c at level 99).

 Notation "[-| c |]" :=
   (interp_carry (-1) wB to_Z c)  (at level 0, c at level 99).

 Notation "[|| x ||]" :=
   (zn2z_to_Z wB to_Z x)  (at level 0, x at level 99).

 Lemma spec_more_than_1_digit: 1 < Zpos digits.digits:positive
digits_ne_1:digits <> 1%positive
1 < Z.pos digits
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
1 < Z.pos digits
  generalize digits_ne_1; destruct digits; red; auto.digits:positive
digits_ne_1:1%positive <> 1%positive
1%positive <> 1%positive -> (1 ?= 1) = Lt
  destruct 1; auto.
 Qed.
 Let digits_gt_1 := spec_more_than_1_digit.

 Lemma wB_pos : wB > 0.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
wB > 0
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
wB > 0
  apply Z.lt_gt.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
0 < wB
  unfold wB, base; auto with zarith.
 Qed.
 Hint Resolve wB_pos : core.

 Lemma spec_to_Z_1 : forall x, 0 <= [|x|].digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, 0 <= [|x|]
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, 0 <= [|x|]
  unfold to_Z; intros; destruct (Z_mod_lt x wB wB_pos); auto.
 Qed.

 Lemma spec_to_Z_2 : forall x, [|x|] < wB.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, [|x|] < wB
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, [|x|] < wB
  unfold to_Z; intros; destruct (Z_mod_lt x wB wB_pos); auto.
 Qed.
 Hint Resolve spec_to_Z_1 spec_to_Z_2 : core.

 Lemma spec_to_Z : forall x, 0 <= [|x|] < wB.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, 0 <= [|x|] < wB
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, 0 <= [|x|] < wB
  auto.
 Qed.

 Definition of_pos x :=
   let (q,r) := Z.pos_div_eucl x wB in (N_of_Z q, r).

 Lemma spec_of_pos : forall p,
   Zpos p = (Z.of_N (fst (of_pos p)))*wB + [|(snd (of_pos p))|].digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall p : positive,
Z.pos p =
Z.of_N (fst (of_pos p)) * wB + [|snd (of_pos p)|]
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall p : positive,
Z.pos p =
Z.of_N (fst (of_pos p)) * wB + [|snd (of_pos p)|]
  intros; unfold of_pos; simpl.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
Z.pos p =
Z.of_N
  (fst
     (let (q, r) := Z.pos_div_eucl p wB in
      (Z.to_N q, r))) * wB +
[|snd
    (let (q, r) := Z.pos_div_eucl p wB in
     (Z.to_N q, r))|]
  generalize (Z_div_mod_POS wB wB_pos p).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
(let (q, r) := Z.pos_div_eucl p wB in
 Z.pos p = wB * q + r /\ 0 <= r < wB) ->
Z.pos p =
Z.of_N
  (fst
     (let (q, r) := Z.pos_div_eucl p wB in
      (Z.to_N q, r))) * wB +
[|snd
    (let (q, r) := Z.pos_div_eucl p wB in
     (Z.to_N q, r))|]
  destruct (Z.pos_div_eucl p wB); simpl; destruct 1.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
z, z0:Z
H:Z.pos p = wB * z + z0
H0:0 <= z0 < wB
Z.pos p = Z.of_N (Z.to_N z) * wB + [|z0|]
  unfold to_Z; rewrite Zmod_small; auto.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
z, z0:Z
H:Z.pos p = wB * z + z0
H0:0 <= z0 < wB
Z.pos p = Z.of_N (Z.to_N z) * wB + z0
  assert (0 <= z).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
z, z0:Z
H:Z.pos p = wB * z + z0
H0:0 <= z0 < wB
0 <= z
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
z, z0:Z
H:Z.pos p = wB * z + z0
H0:0 <= z0 < wB
H1:0 <= z
Z.pos p = Z.of_N (Z.to_N z) * wB + z0
   replace z with (Zpos p / wB) by
    (symmetry; apply Zdiv_unique with z0; auto).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
z, z0:Z
H:Z.pos p = wB * z + z0
H0:0 <= z0 < wB
0 <= Z.pos p / wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
z, z0:Z
H:Z.pos p = wB * z + z0
H0:0 <= z0 < wB
H1:0 <= z
Z.pos p = Z.of_N (Z.to_N z) * wB + z0
   apply Z_div_pos; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
z, z0:Z
H:Z.pos p = wB * z + z0
H0:0 <= z0 < wB
H1:0 <= z
Z.pos p = Z.of_N (Z.to_N z) * wB + z0
  replace (Z.of_N (N_of_Z z)) with z by
    (destruct z; simpl; auto; elim H1; auto).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
z, z0:Z
H:Z.pos p = wB * z + z0
H0:0 <= z0 < wB
H1:0 <= z
Z.pos p = z * wB + z0
  rewrite Z.mul_comm; auto.
 Qed.

 Lemma spec_zdigits : [|zdigits|] = Zpos digits.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
[|zdigits|] = Z.pos digits
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
[|zdigits|] = Z.pos digits
  unfold to_Z, zdigits.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
Z.pos digits mod wB = Z.pos digits
  apply Zmod_small.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
0 <= Z.pos digits < wB
  unfold wB, base.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
0 <= Z.pos digits < 2 ^ Z.pos digits
  split; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
Z.pos digits < 2 ^ Z.pos digits
  apply Zpower2_lt_lin; auto with zarith.
 Qed.

 Definition zero := 0.
 Definition one := 1.
 Definition minus_one := wB - 1.

 Lemma spec_0 : [|zero|] = 0.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
[|zero|] = 0
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
[|zero|] = 0
  unfold to_Z, zero.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
0 mod wB = 0
  apply Zmod_small; generalize wB_pos; auto with zarith.
 Qed.

 Lemma spec_1 : [|one|] = 1.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
[|one|] = 1
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
[|one|] = 1
  unfold to_Z, one.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
1 mod wB = 1
  apply Zmod_small; split; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
1 < wB
  unfold wB, base.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
1 < 2 ^ Z.pos digits
  apply Z.lt_trans with (Zpos digits); auto.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
Z.pos digits < 2 ^ Z.pos digits
  apply Zpower2_lt_lin; auto with zarith.
 Qed.

 Lemma spec_Bm1 : [|minus_one|] = wB - 1.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
[|minus_one|] = wB - 1
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
[|minus_one|] = wB - 1
  unfold to_Z, minus_one.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
(wB - 1) mod wB = wB - 1
  apply Zmod_small; split; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
0 <= wB - 1
  unfold wB, base.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
0 <= 2 ^ Z.pos digits - 1
  cut (1 <= 2 ^ Zpos digits); auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
1 <= 2 ^ Z.pos digits
  apply Z.le_trans with (Zpos digits); auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
Z.pos digits <= 2 ^ Z.pos digits
  apply Zpower2_le_lin; auto with zarith.
 Qed.

 Definition compare x y := Z.compare [|x|] [|y|].

 Lemma spec_compare : forall x y,
   compare x y = Z.compare [|x|] [|y|].digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y : Z, compare x y = ([|x|] ?= [|y|])
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y : Z, compare x y = ([|x|] ?= [|y|]) reflexivity. Qed.

 Definition eq0 x :=
   match [|x|] with Z0 => true | _ => false end.

 Lemma spec_eq0 : forall x, eq0 x = true -> [|x|] = 0.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, eq0 x = true -> [|x|] = 0
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, eq0 x = true -> [|x|] = 0
  unfold eq0; intros; now destruct [|x|].
 Qed.

 Definition opp_c x :=
   if eq0 x then C0 0 else C1 (- x).
 Definition opp x := - x.
 Definition opp_carry x := - x - 1.

 Lemma spec_opp_c : forall x, [-|opp_c x|] = -[|x|].digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, [-|opp_c x|] = - [|x|]
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, [-|opp_c x|] = - [|x|]
 intros; unfold opp_c, to_Z; auto.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
interp_carry (-1) wB (fun x0 : Z => x0 mod wB)
  (if eq0 x then C0 0 else C1 (- x)) = - (x mod wB)
 case_eq (eq0 x); intros; unfold interp_carry.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 x = true
0 mod wB = - (x mod wB)
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 x = false
-1 * wB + - x mod wB = - (x mod wB)
 fold [|x|]; rewrite (spec_eq0 x H); auto.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 x = false
-1 * wB + - x mod wB = - (x mod wB)
 assert (x mod wB <> 0).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 x = false
x mod wB <> 0
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 x = false
H0:x mod wB <> 0
-1 * wB + - x mod wB = - (x mod wB)
  unfold eq0, to_Z in H.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:match x mod wB with
| 0 => true
| _ => false
end = false
x mod wB <> 0
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 x = false
H0:x mod wB <> 0
-1 * wB + - x mod wB = - (x mod wB)
  intro H0; rewrite H0 in H; discriminate.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 x = false
H0:x mod wB <> 0
-1 * wB + - x mod wB = - (x mod wB)
 rewrite Z_mod_nz_opp_full; auto with zarith.
 Qed.

 Lemma spec_opp : forall x, [|opp x|] = (-[|x|]) mod wB.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, [|opp x|] = - [|x|] mod wB
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, [|opp x|] = - [|x|] mod wB
 intros; unfold opp, to_Z; auto.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
- x mod wB = - (x mod wB) mod wB
 change ((- x) mod wB = (0 - (x mod wB)) mod wB).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
- x mod wB = (0 - x mod wB) mod wB
 rewrite Zminus_mod_idemp_r; simpl; auto.
 Qed.

 Lemma spec_opp_carry : forall x, [|opp_carry x|] = wB - [|x|] - 1.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, [|opp_carry x|] = wB - [|x|] - 1
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, [|opp_carry x|] = wB - [|x|] - 1
 intros; unfold opp_carry, to_Z; auto.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
(- x - 1) mod wB = wB - x mod wB - 1
 replace (- x - 1) with (- 1 - x) by omega.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
(-1 - x) mod wB = wB - x mod wB - 1
 rewrite <- Zminus_mod_idemp_r.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
(-1 - x mod wB) mod wB = wB - x mod wB - 1
 replace ( -1 - x mod wB) with (0 + ( -1 - x mod wB)) by omega.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
(0 + (-1 - x mod wB)) mod wB = wB - x mod wB - 1
 rewrite <- (Z_mod_same_full wB).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
(wB mod wB + (-1 - x mod wB)) mod wB =
wB - x mod wB - 1
 rewrite Zplus_mod_idemp_l.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
(wB + (-1 - x mod wB)) mod wB = wB - x mod wB - 1
 replace (wB + (-1 - x mod wB)) with (wB - x mod wB -1) by omega.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
(wB - x mod wB - 1) mod wB = wB - x mod wB - 1
 apply Zmod_small.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
0 <= wB - x mod wB - 1 < wB
 generalize (Z_mod_lt x wB wB_pos); omega.
 Qed.

 Definition succ_c x :=
  let y := Z.succ x in
  if eq0 y then C1 0 else C0 y.

 Definition add_c x y :=
  let z := [|x|] + [|y|] in
  if Z_lt_le_dec z wB then C0 z else C1 (z-wB).

 Definition add_carry_c x y :=
  let z := [|x|]+[|y|]+1 in
  if Z_lt_le_dec z wB then C0 z else C1 (z-wB).

 Definition succ := Z.succ.
 Definition add := Z.add.
 Definition add_carry x y := x + y + 1.

 Lemma Zmod_equal :
  forall x y z, z>0 -> (x-y) mod z = 0 -> x mod z = y mod z.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y z : Z,
z > 0 -> (x - y) mod z = 0 -> x mod z = y mod z
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y z : Z,
z > 0 -> (x - y) mod z = 0 -> x mod z = y mod z
 intros.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, z:Z
H:z > 0
H0:(x - y) mod z = 0
x mod z = y mod z
 generalize (Z_div_mod_eq (x-y) z H); rewrite H0, Z.add_0_r.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, z:Z
H:z > 0
H0:(x - y) mod z = 0
x - y = z * ((x - y) / z) -> x mod z = y mod z
 remember ((x-y)/z) as k.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, z:Z
H:z > 0
H0:(x - y) mod z = 0
k:Z
Heqk:k = (x - y) / z
x - y = z * k -> x mod z = y mod z
 rewrite Z.sub_move_r, Z.add_comm, Z.mul_comm.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, z:Z
H:z > 0
H0:(x - y) mod z = 0
k:Z
Heqk:k = (x - y) / z
x = y + k * z -> x mod z = y mod z intros ->.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
y, z:Z
H:z > 0
k:Z
Heqk:k = (y + k * z - y) / z
H0:(y + k * z - y) mod z = 0
(y + k * z) mod z = y mod z
 now apply Z_mod_plus.
 Qed.

 Lemma spec_succ_c : forall x, [+|succ_c x|] = [|x|] + 1.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, [+|succ_c x|] = [|x|] + 1
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, [+|succ_c x|] = [|x|] + 1
 intros; unfold succ_c, to_Z, Z.succ.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
interp_carry 1 wB (fun x0 : Z => x0 mod wB)
  (if eq0 (x + 1) then C1 0 else C0 (x + 1)) =
x mod wB + 1
 case_eq (eq0 (x+1)); intros; unfold interp_carry.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = true
1 * wB + 0 mod wB = x mod wB + 1
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = false
(x + 1) mod wB = x mod wB + 1

 rewrite Z.mul_1_l.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = true
wB + 0 mod wB = x mod wB + 1
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = false
(x + 1) mod wB = x mod wB + 1
 replace (wB + 0 mod wB) with wB by auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = true
wB = x mod wB + 1
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = false
(x + 1) mod wB = x mod wB + 1
 symmetry.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = true
x mod wB + 1 = wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = false
(x + 1) mod wB = x mod wB + 1 rewrite Z.add_move_r.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = true
x mod wB = wB - 1
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = false
(x + 1) mod wB = x mod wB + 1
 assert ((x+1) mod wB = 0) by (apply spec_eq0; auto).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = true
H0:(x + 1) mod wB = 0
x mod wB = wB - 1
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = false
(x + 1) mod wB = x mod wB + 1
 replace (wB-1) with ((wB-1) mod wB) by
  (apply Zmod_small; generalize wB_pos; omega).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = true
H0:(x + 1) mod wB = 0
x mod wB = (wB - 1) mod wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = false
(x + 1) mod wB = x mod wB + 1
 rewrite <- Zminus_mod_idemp_l; rewrite Z_mod_same; simpl; auto.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = true
H0:(x + 1) mod wB = 0
x mod wB = -1 mod wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = false
(x + 1) mod wB = x mod wB + 1
 apply Zmod_equal; auto.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = false
(x + 1) mod wB = x mod wB + 1

 assert ((x+1) mod wB <> 0).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = false
(x + 1) mod wB <> 0
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = false
H0:(x + 1) mod wB <> 0
(x + 1) mod wB = x mod wB + 1
  unfold eq0, to_Z in *; now destruct ((x+1) mod wB).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = false
H0:(x + 1) mod wB <> 0
(x + 1) mod wB = x mod wB + 1
 assert (x mod wB + 1 <> wB).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = false
H0:(x + 1) mod wB <> 0
x mod wB + 1 <> wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = false
H0:(x + 1) mod wB <> 0
H1:x mod wB + 1 <> wB
(x + 1) mod wB = x mod wB + 1
  contradict H0.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = false
H0:x mod wB + 1 = wB
(x + 1) mod wB = 0
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = false
H0:(x + 1) mod wB <> 0
H1:x mod wB + 1 <> wB
(x + 1) mod wB = x mod wB + 1
  rewrite Z.add_move_r in H0; simpl in H0.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = false
H0:x mod wB = wB - 1
(x + 1) mod wB = 0
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = false
H0:(x + 1) mod wB <> 0
H1:x mod wB + 1 <> wB
(x + 1) mod wB = x mod wB + 1
  rewrite <- Zplus_mod_idemp_l; rewrite H0.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = false
H0:x mod wB = wB - 1
(wB - 1 + 1) mod wB = 0
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = false
H0:(x + 1) mod wB <> 0
H1:x mod wB + 1 <> wB
(x + 1) mod wB = x mod wB + 1
  replace (wB-1+1) with wB; auto with zarith; apply Z_mod_same; auto.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = false
H0:(x + 1) mod wB <> 0
H1:x mod wB + 1 <> wB
(x + 1) mod wB = x mod wB + 1
 rewrite <- Zplus_mod_idemp_l.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = false
H0:(x + 1) mod wB <> 0
H1:x mod wB + 1 <> wB
(x mod wB + 1) mod wB = x mod wB + 1
 apply Zmod_small.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 (x + 1) = false
H0:(x + 1) mod wB <> 0
H1:x mod wB + 1 <> wB
0 <= x mod wB + 1 < wB
 generalize (Z_mod_lt x wB wB_pos); omega.
 Qed.

 Lemma spec_add_c : forall x y, [+|add_c x y|] = [|x|] + [|y|].digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y : Z, [+|add_c x y|] = [|x|] + [|y|]
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y : Z, [+|add_c x y|] = [|x|] + [|y|]
 intros; unfold add_c, to_Z, interp_carry.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
match
  (if Z_lt_le_dec (x mod wB + y mod wB) wB
   then C0 (x mod wB + y mod wB)
   else C1 (x mod wB + y mod wB - wB))
with
| C0 x0 => x0 mod wB
| C1 x0 => 1 * wB + x0 mod wB
end = x mod wB + y mod wB
 destruct Z_lt_le_dec.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:x mod wB + y mod wB < wB
(x mod wB + y mod wB) mod wB = x mod wB + y mod wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:wB <= x mod wB + y mod wB
1 * wB + (x mod wB + y mod wB - wB) mod wB =
x mod wB + y mod wB
 apply Zmod_small;
  generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:wB <= x mod wB + y mod wB
1 * wB + (x mod wB + y mod wB - wB) mod wB =
x mod wB + y mod wB
 rewrite Z.mul_1_l, Z.add_comm, Z.add_move_r.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:wB <= x mod wB + y mod wB
(x mod wB + y mod wB - wB) mod wB =
x mod wB + y mod wB - wB
 apply Zmod_small;
  generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega.
 Qed.

 Lemma spec_add_carry_c : forall x y, [+|add_carry_c x y|] = [|x|] + [|y|] + 1.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y : Z,
[+|add_carry_c x y|] = [|x|] + [|y|] + 1
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y : Z,
[+|add_carry_c x y|] = [|x|] + [|y|] + 1
 intros; unfold add_carry_c, to_Z, interp_carry.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
match
  (if Z_lt_le_dec (x mod wB + y mod wB + 1) wB
   then C0 (x mod wB + y mod wB + 1)
   else C1 (x mod wB + y mod wB + 1 - wB))
with
| C0 x0 => x0 mod wB
| C1 x0 => 1 * wB + x0 mod wB
end = x mod wB + y mod wB + 1
 destruct Z_lt_le_dec.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:x mod wB + y mod wB + 1 < wB
(x mod wB + y mod wB + 1) mod wB =
x mod wB + y mod wB + 1
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:wB <= x mod wB + y mod wB + 1
1 * wB + (x mod wB + y mod wB + 1 - wB) mod wB =
x mod wB + y mod wB + 1
 apply Zmod_small;
  generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:wB <= x mod wB + y mod wB + 1
1 * wB + (x mod wB + y mod wB + 1 - wB) mod wB =
x mod wB + y mod wB + 1
 rewrite Z.mul_1_l, Z.add_comm, Z.add_move_r.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:wB <= x mod wB + y mod wB + 1
(x mod wB + y mod wB + 1 - wB) mod wB =
x mod wB + y mod wB + 1 - wB
 apply Zmod_small;
  generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega.
 Qed.

 Lemma spec_succ : forall x, [|succ x|] = ([|x|] + 1) mod wB.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, [|succ x|] = ([|x|] + 1) mod wB
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, [|succ x|] = ([|x|] + 1) mod wB
 intros; unfold succ, to_Z, Z.succ.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
(x + 1) mod wB = (x mod wB + 1) mod wB
 symmetry; apply Zplus_mod_idemp_l.
 Qed.

 Lemma spec_add : forall x y, [|add x y|] = ([|x|] + [|y|]) mod wB.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y : Z, [|add x y|] = ([|x|] + [|y|]) mod wB
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y : Z, [|add x y|] = ([|x|] + [|y|]) mod wB
 intros; unfold add, to_Z; apply Zplus_mod.
 Qed.

 Lemma spec_add_carry :
	 forall x y, [|add_carry x y|] = ([|x|] + [|y|] + 1) mod wB.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y : Z,
[|add_carry x y|] = ([|x|] + [|y|] + 1) mod wB
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y : Z,
[|add_carry x y|] = ([|x|] + [|y|] + 1) mod wB
 intros; unfold add_carry, to_Z.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
(x + y + 1) mod wB = (x mod wB + y mod wB + 1) mod wB
 rewrite <- Zplus_mod_idemp_l.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
((x + y) mod wB + 1) mod wB =
(x mod wB + y mod wB + 1) mod wB
 rewrite (Zplus_mod x y).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
((x mod wB + y mod wB) mod wB + 1) mod wB =
(x mod wB + y mod wB + 1) mod wB
 rewrite Zplus_mod_idemp_l; auto.
 Qed.

 Definition pred_c x :=
  if eq0 x then C1 (wB-1) else C0 (x-1).

 Definition sub_c x y :=
  let z := [|x|]-[|y|] in
  if Z_lt_le_dec z 0 then C1 (wB+z) else C0 z.

 Definition sub_carry_c x y :=
  let z := [|x|]-[|y|]-1 in
  if Z_lt_le_dec z 0 then C1 (wB+z) else C0 z.

 Definition pred := Z.pred.
 Definition sub := Z.sub.
 Definition sub_carry x y := x - y - 1.

 Lemma spec_pred_c : forall x, [-|pred_c x|] = [|x|] - 1.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, [-|pred_c x|] = [|x|] - 1
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, [-|pred_c x|] = [|x|] - 1
 intros; unfold pred_c, to_Z, interp_carry.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
match (if eq0 x then C1 (wB - 1) else C0 (x - 1)) with
| C0 x0 => x0 mod wB
| C1 x0 => -1 * wB + x0 mod wB
end = x mod wB - 1
 case_eq (eq0 x); intros.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 x = true
-1 * wB + (wB - 1) mod wB = x mod wB - 1
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 x = false
(x - 1) mod wB = x mod wB - 1
 fold [|x|]; rewrite spec_eq0; auto.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 x = true
-1 * wB + (wB - 1) mod wB = 0 - 1
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 x = false
(x - 1) mod wB = x mod wB - 1
 replace ((wB-1) mod wB) with (wB-1); auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 x = true
wB - 1 = (wB - 1) mod wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 x = false
(x - 1) mod wB = x mod wB - 1
 symmetry; apply Zmod_small; generalize wB_pos; omega.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 x = false
(x - 1) mod wB = x mod wB - 1

 assert (x mod wB <> 0).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 x = false
x mod wB <> 0
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 x = false
H0:x mod wB <> 0
(x - 1) mod wB = x mod wB - 1
  unfold eq0, to_Z in *; now destruct (x mod wB).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 x = false
H0:x mod wB <> 0
(x - 1) mod wB = x mod wB - 1
 rewrite <- Zminus_mod_idemp_l.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 x = false
H0:x mod wB <> 0
(x mod wB - 1) mod wB = x mod wB - 1
 apply Zmod_small.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:eq0 x = false
H0:x mod wB <> 0
0 <= x mod wB - 1 < wB
 generalize (Z_mod_lt x wB wB_pos); omega.
 Qed.

 Lemma spec_sub_c : forall x y, [-|sub_c x y|] = [|x|] - [|y|].digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y : Z, [-|sub_c x y|] = [|x|] - [|y|]
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y : Z, [-|sub_c x y|] = [|x|] - [|y|]
 intros; unfold sub_c, to_Z, interp_carry.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
match
  (if Z_lt_le_dec (x mod wB - y mod wB) 0
   then C1 (wB + (x mod wB - y mod wB))
   else C0 (x mod wB - y mod wB))
with
| C0 x0 => x0 mod wB
| C1 x0 => -1 * wB + x0 mod wB
end = x mod wB - y mod wB
 destruct Z_lt_le_dec.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:x mod wB - y mod wB < 0
-1 * wB + (wB + (x mod wB - y mod wB)) mod wB =
x mod wB - y mod wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:0 <= x mod wB - y mod wB
(x mod wB - y mod wB) mod wB = x mod wB - y mod wB
 replace ((wB + (x mod wB - y mod wB)) mod wB) with
   (wB + (x mod wB - y mod wB)).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:x mod wB - y mod wB < 0
-1 * wB + (wB + (x mod wB - y mod wB)) =
x mod wB - y mod wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:x mod wB - y mod wB < 0
wB + (x mod wB - y mod wB) =
(wB + (x mod wB - y mod wB)) mod wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:0 <= x mod wB - y mod wB
(x mod wB - y mod wB) mod wB = x mod wB - y mod wB
 omega.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:x mod wB - y mod wB < 0
wB + (x mod wB - y mod wB) =
(wB + (x mod wB - y mod wB)) mod wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:0 <= x mod wB - y mod wB
(x mod wB - y mod wB) mod wB = x mod wB - y mod wB
 symmetry; apply Zmod_small.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:x mod wB - y mod wB < 0
0 <= wB + (x mod wB - y mod wB) < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:0 <= x mod wB - y mod wB
(x mod wB - y mod wB) mod wB = x mod wB - y mod wB
 generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:0 <= x mod wB - y mod wB
(x mod wB - y mod wB) mod wB = x mod wB - y mod wB

 apply Zmod_small.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:0 <= x mod wB - y mod wB
0 <= x mod wB - y mod wB < wB
 generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega.
 Qed.

 Lemma spec_sub_carry_c : forall x y, [-|sub_carry_c x y|] = [|x|] - [|y|] - 1.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y : Z,
[-|sub_carry_c x y|] = [|x|] - [|y|] - 1
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y : Z,
[-|sub_carry_c x y|] = [|x|] - [|y|] - 1
 intros; unfold sub_carry_c, to_Z, interp_carry.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
match
  (if Z_lt_le_dec (x mod wB - y mod wB - 1) 0
   then C1 (wB + (x mod wB - y mod wB - 1))
   else C0 (x mod wB - y mod wB - 1))
with
| C0 x0 => x0 mod wB
| C1 x0 => -1 * wB + x0 mod wB
end = x mod wB - y mod wB - 1
 destruct Z_lt_le_dec.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:x mod wB - y mod wB - 1 < 0
-1 * wB + (wB + (x mod wB - y mod wB - 1)) mod wB =
x mod wB - y mod wB - 1
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:0 <= x mod wB - y mod wB - 1
(x mod wB - y mod wB - 1) mod wB =
x mod wB - y mod wB - 1
 replace ((wB + (x mod wB - y mod wB - 1)) mod wB) with
   (wB + (x mod wB - y mod wB -1)).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:x mod wB - y mod wB - 1 < 0
-1 * wB + (wB + (x mod wB - y mod wB - 1)) =
x mod wB - y mod wB - 1
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:x mod wB - y mod wB - 1 < 0
wB + (x mod wB - y mod wB - 1) =
(wB + (x mod wB - y mod wB - 1)) mod wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:0 <= x mod wB - y mod wB - 1
(x mod wB - y mod wB - 1) mod wB =
x mod wB - y mod wB - 1
 omega.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:x mod wB - y mod wB - 1 < 0
wB + (x mod wB - y mod wB - 1) =
(wB + (x mod wB - y mod wB - 1)) mod wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:0 <= x mod wB - y mod wB - 1
(x mod wB - y mod wB - 1) mod wB =
x mod wB - y mod wB - 1
 symmetry; apply Zmod_small.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:x mod wB - y mod wB - 1 < 0
0 <= wB + (x mod wB - y mod wB - 1) < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:0 <= x mod wB - y mod wB - 1
(x mod wB - y mod wB - 1) mod wB =
x mod wB - y mod wB - 1
 generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:0 <= x mod wB - y mod wB - 1
(x mod wB - y mod wB - 1) mod wB =
x mod wB - y mod wB - 1

 apply Zmod_small.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
l:0 <= x mod wB - y mod wB - 1
0 <= x mod wB - y mod wB - 1 < wB
 generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega.
 Qed.

 Lemma spec_pred : forall x, [|pred x|] = ([|x|] - 1) mod wB.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, [|pred x|] = ([|x|] - 1) mod wB
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, [|pred x|] = ([|x|] - 1) mod wB
 intros; unfold pred, to_Z, Z.pred.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
(x + -1) mod wB = (x mod wB - 1) mod wB
 rewrite <- Zplus_mod_idemp_l; auto.
 Qed.

 Lemma spec_sub : forall x y, [|sub x y|] = ([|x|] - [|y|]) mod wB.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y : Z, [|sub x y|] = ([|x|] - [|y|]) mod wB
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y : Z, [|sub x y|] = ([|x|] - [|y|]) mod wB
 intros; unfold sub, to_Z; apply Zminus_mod.
 Qed.

 Lemma spec_sub_carry :
  forall x y, [|sub_carry x y|] = ([|x|] - [|y|] - 1) mod wB.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y : Z,
[|sub_carry x y|] = ([|x|] - [|y|] - 1) mod wB
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y : Z,
[|sub_carry x y|] = ([|x|] - [|y|] - 1) mod wB
 intros; unfold sub_carry, to_Z.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
(x - y - 1) mod wB = (x mod wB - y mod wB - 1) mod wB
 rewrite <- Zminus_mod_idemp_l.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
((x - y) mod wB - 1) mod wB =
(x mod wB - y mod wB - 1) mod wB
 rewrite (Zminus_mod x y).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
((x mod wB - y mod wB) mod wB - 1) mod wB =
(x mod wB - y mod wB - 1) mod wB
 rewrite Zminus_mod_idemp_l.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
(x mod wB - y mod wB - 1) mod wB =
(x mod wB - y mod wB - 1) mod wB
 auto.
 Qed.

 Definition mul_c x y :=
  let (h,l) := Z.div_eucl ([|x|]*[|y|]) wB in
  if eq0 h then if eq0 l then W0 else WW h l else WW h l.

 Definition mul := Z.mul.

 Definition square_c x := mul_c x x.

 Lemma spec_mul_c : forall x y, [|| mul_c x y ||] = [|x|] * [|y|].digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y : Z, [||mul_c x y||] = [|x|] * [|y|]
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y : Z, [||mul_c x y||] = [|x|] * [|y|]
 intros; unfold mul_c, zn2z_to_Z.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
match
  (let (h, l) := Z.div_eucl ([|x|] * [|y|]) wB in
   if eq0 h
   then if eq0 l then W0 else WW h l
   else WW h l)
with
| W0 => 0
| WW xh xl => [|xh|] * wB + [|xl|]
end = [|x|] * [|y|]
 assert (Z.div_eucl ([|x|]*[|y|]) wB = (([|x|]*[|y|])/wB,([|x|]*[|y|]) mod wB)).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
Z.div_eucl ([|x|] * [|y|]) wB =
([|x|] * [|y|] / wB, ([|x|] * [|y|]) mod wB)
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:Z.div_eucl ([|x|] * [|y|]) wB =
([|x|] * [|y|] / wB, ([|x|] * [|y|]) mod wB)
match
  (let (h, l) := Z.div_eucl ([|x|] * [|y|]) wB in
   if eq0 h
   then if eq0 l then W0 else WW h l
   else WW h l)
with
| W0 => 0
| WW xh xl => [|xh|] * wB + [|xl|]
end = [|x|] * [|y|]
  unfold Z.modulo, Z.div; destruct Z.div_eucl; auto.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:Z.div_eucl ([|x|] * [|y|]) wB =
([|x|] * [|y|] / wB, ([|x|] * [|y|]) mod wB)
match
  (let (h, l) := Z.div_eucl ([|x|] * [|y|]) wB in
   if eq0 h
   then if eq0 l then W0 else WW h l
   else WW h l)
with
| W0 => 0
| WW xh xl => [|xh|] * wB + [|xl|]
end = [|x|] * [|y|]
 generalize (Z_div_mod ([|x|]*[|y|]) wB wB_pos); destruct Z.div_eucl as (h,l).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, h, l:Z
H:(h, l) =
([|x|] * [|y|] / wB, ([|x|] * [|y|]) mod wB)
[|x|] * [|y|] = wB * h + l /\ 0 <= l < wB ->
match
  (if eq0 h
   then if eq0 l then W0 else WW h l
   else WW h l)
with
| W0 => 0
| WW xh xl => [|xh|] * wB + [|xl|]
end = [|x|] * [|y|]
 destruct 1; injection H as ? ?.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, h, l:Z
H:h = [|x|] * [|y|] / wB
H2:l = ([|x|] * [|y|]) mod wB
H0:[|x|] * [|y|] = wB * h + l
H1:0 <= l < wB
match
  (if eq0 h
   then if eq0 l then W0 else WW h l
   else WW h l)
with
| W0 => 0
| WW xh xl => [|xh|] * wB + [|xl|]
end = [|x|] * [|y|]
 rewrite H0.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, h, l:Z
H:h = [|x|] * [|y|] / wB
H2:l = ([|x|] * [|y|]) mod wB
H0:[|x|] * [|y|] = wB * h + l
H1:0 <= l < wB
match
  (if eq0 h
   then if eq0 l then W0 else WW h l
   else WW h l)
with
| W0 => 0
| WW xh xl => [|xh|] * wB + [|xl|]
end = wB * h + l
 assert ([|l|] = l).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, h, l:Z
H:h = [|x|] * [|y|] / wB
H2:l = ([|x|] * [|y|]) mod wB
H0:[|x|] * [|y|] = wB * h + l
H1:0 <= l < wB
[|l|] = l
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, h, l:Z
H:h = [|x|] * [|y|] / wB
H2:l = ([|x|] * [|y|]) mod wB
H0:[|x|] * [|y|] = wB * h + l
H1:0 <= l < wB
H3:[|l|] = l
match
  (if eq0 h
   then if eq0 l then W0 else WW h l
   else WW h l)
with
| W0 => 0
| WW xh xl => [|xh|] * wB + [|xl|]
end = wB * h + l
  apply Zmod_small; auto.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, h, l:Z
H:h = [|x|] * [|y|] / wB
H2:l = ([|x|] * [|y|]) mod wB
H0:[|x|] * [|y|] = wB * h + l
H1:0 <= l < wB
H3:[|l|] = l
match
  (if eq0 h
   then if eq0 l then W0 else WW h l
   else WW h l)
with
| W0 => 0
| WW xh xl => [|xh|] * wB + [|xl|]
end = wB * h + l
 assert ([|h|] = h).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, h, l:Z
H:h = [|x|] * [|y|] / wB
H2:l = ([|x|] * [|y|]) mod wB
H0:[|x|] * [|y|] = wB * h + l
H1:0 <= l < wB
H3:[|l|] = l
[|h|] = h
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, h, l:Z
H:h = [|x|] * [|y|] / wB
H2:l = ([|x|] * [|y|]) mod wB
H0:[|x|] * [|y|] = wB * h + l
H1:0 <= l < wB
H3:[|l|] = l
H4:[|h|] = h
match
  (if eq0 h
   then if eq0 l then W0 else WW h l
   else WW h l)
with
| W0 => 0
| WW xh xl => [|xh|] * wB + [|xl|]
end = wB * h + l
  apply Zmod_small.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, h, l:Z
H:h = [|x|] * [|y|] / wB
H2:l = ([|x|] * [|y|]) mod wB
H0:[|x|] * [|y|] = wB * h + l
H1:0 <= l < wB
H3:[|l|] = l
0 <= h < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, h, l:Z
H:h = [|x|] * [|y|] / wB
H2:l = ([|x|] * [|y|]) mod wB
H0:[|x|] * [|y|] = wB * h + l
H1:0 <= l < wB
H3:[|l|] = l
H4:[|h|] = h
match
  (if eq0 h
   then if eq0 l then W0 else WW h l
   else WW h l)
with
| W0 => 0
| WW xh xl => [|xh|] * wB + [|xl|]
end = wB * h + l
  subst h.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, l:Z
H2:l = ([|x|] * [|y|]) mod wB
H0:[|x|] * [|y|] = wB * ([|x|] * [|y|] / wB) + l
H1:0 <= l < wB
H3:[|l|] = l
0 <= [|x|] * [|y|] / wB < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, h, l:Z
H:h = [|x|] * [|y|] / wB
H2:l = ([|x|] * [|y|]) mod wB
H0:[|x|] * [|y|] = wB * h + l
H1:0 <= l < wB
H3:[|l|] = l
H4:[|h|] = h
match
  (if eq0 h
   then if eq0 l then W0 else WW h l
   else WW h l)
with
| W0 => 0
| WW xh xl => [|xh|] * wB + [|xl|]
end = wB * h + l
  split.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, l:Z
H2:l = ([|x|] * [|y|]) mod wB
H0:[|x|] * [|y|] = wB * ([|x|] * [|y|] / wB) + l
H1:0 <= l < wB
H3:[|l|] = l
0 <= [|x|] * [|y|] / wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, l:Z
H2:l = ([|x|] * [|y|]) mod wB
H0:[|x|] * [|y|] = wB * ([|x|] * [|y|] / wB) + l
H1:0 <= l < wB
H3:[|l|] = l
[|x|] * [|y|] / wB < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, h, l:Z
H:h = [|x|] * [|y|] / wB
H2:l = ([|x|] * [|y|]) mod wB
H0:[|x|] * [|y|] = wB * h + l
H1:0 <= l < wB
H3:[|l|] = l
H4:[|h|] = h
match
  (if eq0 h
   then if eq0 l then W0 else WW h l
   else WW h l)
with
| W0 => 0
| WW xh xl => [|xh|] * wB + [|xl|]
end = wB * h + l
  apply Z_div_pos; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, l:Z
H2:l = ([|x|] * [|y|]) mod wB
H0:[|x|] * [|y|] = wB * ([|x|] * [|y|] / wB) + l
H1:0 <= l < wB
H3:[|l|] = l
[|x|] * [|y|] / wB < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, h, l:Z
H:h = [|x|] * [|y|] / wB
H2:l = ([|x|] * [|y|]) mod wB
H0:[|x|] * [|y|] = wB * h + l
H1:0 <= l < wB
H3:[|l|] = l
H4:[|h|] = h
match
  (if eq0 h
   then if eq0 l then W0 else WW h l
   else WW h l)
with
| W0 => 0
| WW xh xl => [|xh|] * wB + [|xl|]
end = wB * h + l
  apply Zdiv_lt_upper_bound; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, l:Z
H2:l = ([|x|] * [|y|]) mod wB
H0:[|x|] * [|y|] = wB * ([|x|] * [|y|] / wB) + l
H1:0 <= l < wB
H3:[|l|] = l
[|x|] * [|y|] < wB * wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, h, l:Z
H:h = [|x|] * [|y|] / wB
H2:l = ([|x|] * [|y|]) mod wB
H0:[|x|] * [|y|] = wB * h + l
H1:0 <= l < wB
H3:[|l|] = l
H4:[|h|] = h
match
  (if eq0 h
   then if eq0 l then W0 else WW h l
   else WW h l)
with
| W0 => 0
| WW xh xl => [|xh|] * wB + [|xl|]
end = wB * h + l
  apply Z.mul_lt_mono_nonneg; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, h, l:Z
H:h = [|x|] * [|y|] / wB
H2:l = ([|x|] * [|y|]) mod wB
H0:[|x|] * [|y|] = wB * h + l
H1:0 <= l < wB
H3:[|l|] = l
H4:[|h|] = h
match
  (if eq0 h
   then if eq0 l then W0 else WW h l
   else WW h l)
with
| W0 => 0
| WW xh xl => [|xh|] * wB + [|xl|]
end = wB * h + l
 clear H H0 H1 H2.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, h, l:Z
H3:[|l|] = l
H4:[|h|] = h
match
  (if eq0 h
   then if eq0 l then W0 else WW h l
   else WW h l)
with
| W0 => 0
| WW xh xl => [|xh|] * wB + [|xl|]
end = wB * h + l
 case_eq (eq0 h); simpl; intros.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, h, l:Z
H3:[|l|] = l
H4:[|h|] = h
H:eq0 h = true
match (if eq0 l then W0 else WW h l) with
| W0 => 0
| WW xh xl => [|xh|] * wB + [|xl|]
end = wB * h + l
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, h, l:Z
H3:[|l|] = l
H4:[|h|] = h
H:eq0 h = false
[|h|] * wB + [|l|] = wB * h + l
 case_eq (eq0 l); simpl; intros.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, h, l:Z
H3:[|l|] = l
H4:[|h|] = h
H:eq0 h = true
H0:eq0 l = true
0 = wB * h + l
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, h, l:Z
H3:[|l|] = l
H4:[|h|] = h
H:eq0 h = true
H0:eq0 l = false
[|h|] * wB + [|l|] = wB * h + l
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, h, l:Z
H3:[|l|] = l
H4:[|h|] = h
H:eq0 h = false
[|h|] * wB + [|l|] = wB * h + l
 rewrite <- H3, <- H4, (spec_eq0 h), (spec_eq0 l); auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, h, l:Z
H3:[|l|] = l
H4:[|h|] = h
H:eq0 h = true
H0:eq0 l = false
[|h|] * wB + [|l|] = wB * h + l
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, h, l:Z
H3:[|l|] = l
H4:[|h|] = h
H:eq0 h = false
[|h|] * wB + [|l|] = wB * h + l
 rewrite H3, H4; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, h, l:Z
H3:[|l|] = l
H4:[|h|] = h
H:eq0 h = false
[|h|] * wB + [|l|] = wB * h + l
 rewrite H3, H4; auto with zarith.
 Qed.

 Lemma spec_mul : forall x y, [|mul x y|] = ([|x|] * [|y|]) mod wB.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y : Z, [|mul x y|] = ([|x|] * [|y|]) mod wB
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y : Z, [|mul x y|] = ([|x|] * [|y|]) mod wB
 intros; unfold mul, to_Z; apply Zmult_mod.
 Qed.

 Lemma spec_square_c : forall x, [|| square_c x||] = [|x|] * [|x|].digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, [||square_c x||] = [|x|] * [|x|]
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, [||square_c x||] = [|x|] * [|x|]
 intros x; exact (spec_mul_c x x).
 Qed.

 Definition div x y := Z.div_eucl [|x|] [|y|].

 Lemma spec_div : forall a b, 0 < [|b|] ->
      let (q,r) := div a b in
      [|a|] = [|q|] * [|b|] + [|r|] /\
      0 <= [|r|] < [|b|].digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall a b : Z,
0 < [|b|] ->
let (q, r) := div a b in
[|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall a b : Z,
0 < [|b|] ->
let (q, r) := div a b in
[|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
 intros; unfold div.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
let (q, r) := Z.div_eucl [|a|] [|b|] in
[|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
 assert ([|b|]>0) by auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
let (q, r) := Z.div_eucl [|a|] [|b|] in
[|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
 assert (Z.div_eucl [|a|] [|b|] = ([|a|]/[|b|], [|a|] mod [|b|])).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
Z.div_eucl [|a|] [|b|] =
([|a|] / [|b|], [|a|] mod [|b|])
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
H1:Z.div_eucl [|a|] [|b|] =
([|a|] / [|b|], [|a|] mod [|b|])
let (q, r) := Z.div_eucl [|a|] [|b|] in
[|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
  unfold Z.modulo, Z.div; destruct Z.div_eucl; auto.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
H1:Z.div_eucl [|a|] [|b|] =
([|a|] / [|b|], [|a|] mod [|b|])
let (q, r) := Z.div_eucl [|a|] [|b|] in
[|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
 generalize (Z_div_mod [|a|] [|b|] H0).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
H1:Z.div_eucl [|a|] [|b|] =
([|a|] / [|b|], [|a|] mod [|b|])
(let (q, r) := Z.div_eucl [|a|] [|b|] in
 [|a|] = [|b|] * q + r /\ 0 <= r < [|b|]) ->
let (q, r) := Z.div_eucl [|a|] [|b|] in
[|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
 destruct Z.div_eucl as (q,r); destruct 1; intros.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
q, r:Z
H1:(q, r) = ([|a|] / [|b|], [|a|] mod [|b|])
H2:[|a|] = [|b|] * q + r
H3:0 <= r < [|b|]
[|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
 injection H1 as ? ?.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
q, r:Z
H1:q = [|a|] / [|b|]
H4:r = [|a|] mod [|b|]
H2:[|a|] = [|b|] * q + r
H3:0 <= r < [|b|]
[|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
 assert ([|r|]=r).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
q, r:Z
H1:q = [|a|] / [|b|]
H4:r = [|a|] mod [|b|]
H2:[|a|] = [|b|] * q + r
H3:0 <= r < [|b|]
[|r|] = r
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
q, r:Z
H1:q = [|a|] / [|b|]
H4:r = [|a|] mod [|b|]
H2:[|a|] = [|b|] * q + r
H3:0 <= r < [|b|]
H5:[|r|] = r
[|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
  apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|];
   auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
q, r:Z
H1:q = [|a|] / [|b|]
H4:r = [|a|] mod [|b|]
H2:[|a|] = [|b|] * q + r
H3:0 <= r < [|b|]
H5:[|r|] = r
[|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
 assert ([|q|]=q).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
q, r:Z
H1:q = [|a|] / [|b|]
H4:r = [|a|] mod [|b|]
H2:[|a|] = [|b|] * q + r
H3:0 <= r < [|b|]
H5:[|r|] = r
[|q|] = q
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
q, r:Z
H1:q = [|a|] / [|b|]
H4:r = [|a|] mod [|b|]
H2:[|a|] = [|b|] * q + r
H3:0 <= r < [|b|]
H5:[|r|] = r
H6:[|q|] = q
[|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
  apply Zmod_small.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
q, r:Z
H1:q = [|a|] / [|b|]
H4:r = [|a|] mod [|b|]
H2:[|a|] = [|b|] * q + r
H3:0 <= r < [|b|]
H5:[|r|] = r
0 <= q < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
q, r:Z
H1:q = [|a|] / [|b|]
H4:r = [|a|] mod [|b|]
H2:[|a|] = [|b|] * q + r
H3:0 <= r < [|b|]
H5:[|r|] = r
H6:[|q|] = q
[|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
  subst q.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
r:Z
H4:r = [|a|] mod [|b|]
H2:[|a|] = [|b|] * ([|a|] / [|b|]) + r
H3:0 <= r < [|b|]
H5:[|r|] = r
0 <= [|a|] / [|b|] < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
q, r:Z
H1:q = [|a|] / [|b|]
H4:r = [|a|] mod [|b|]
H2:[|a|] = [|b|] * q + r
H3:0 <= r < [|b|]
H5:[|r|] = r
H6:[|q|] = q
[|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
  split.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
r:Z
H4:r = [|a|] mod [|b|]
H2:[|a|] = [|b|] * ([|a|] / [|b|]) + r
H3:0 <= r < [|b|]
H5:[|r|] = r
0 <= [|a|] / [|b|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
r:Z
H4:r = [|a|] mod [|b|]
H2:[|a|] = [|b|] * ([|a|] / [|b|]) + r
H3:0 <= r < [|b|]
H5:[|r|] = r
[|a|] / [|b|] < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
q, r:Z
H1:q = [|a|] / [|b|]
H4:r = [|a|] mod [|b|]
H2:[|a|] = [|b|] * q + r
H3:0 <= r < [|b|]
H5:[|r|] = r
H6:[|q|] = q
[|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
  apply Z_div_pos; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
r:Z
H4:r = [|a|] mod [|b|]
H2:[|a|] = [|b|] * ([|a|] / [|b|]) + r
H3:0 <= r < [|b|]
H5:[|r|] = r
[|a|] / [|b|] < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
q, r:Z
H1:q = [|a|] / [|b|]
H4:r = [|a|] mod [|b|]
H2:[|a|] = [|b|] * q + r
H3:0 <= r < [|b|]
H5:[|r|] = r
H6:[|q|] = q
[|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
  apply Zdiv_lt_upper_bound; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
r:Z
H4:r = [|a|] mod [|b|]
H2:[|a|] = [|b|] * ([|a|] / [|b|]) + r
H3:0 <= r < [|b|]
H5:[|r|] = r
[|a|] < wB * [|b|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
q, r:Z
H1:q = [|a|] / [|b|]
H4:r = [|a|] mod [|b|]
H2:[|a|] = [|b|] * q + r
H3:0 <= r < [|b|]
H5:[|r|] = r
H6:[|q|] = q
[|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
  apply Z.lt_le_trans with (wB*1).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
r:Z
H4:r = [|a|] mod [|b|]
H2:[|a|] = [|b|] * ([|a|] / [|b|]) + r
H3:0 <= r < [|b|]
H5:[|r|] = r
[|a|] < wB * 1
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
r:Z
H4:r = [|a|] mod [|b|]
H2:[|a|] = [|b|] * ([|a|] / [|b|]) + r
H3:0 <= r < [|b|]
H5:[|r|] = r
wB * 1 <= wB * [|b|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
q, r:Z
H1:q = [|a|] / [|b|]
H4:r = [|a|] mod [|b|]
H2:[|a|] = [|b|] * q + r
H3:0 <= r < [|b|]
H5:[|r|] = r
H6:[|q|] = q
[|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
  rewrite Z.mul_1_r; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
r:Z
H4:r = [|a|] mod [|b|]
H2:[|a|] = [|b|] * ([|a|] / [|b|]) + r
H3:0 <= r < [|b|]
H5:[|r|] = r
wB * 1 <= wB * [|b|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
q, r:Z
H1:q = [|a|] / [|b|]
H4:r = [|a|] mod [|b|]
H2:[|a|] = [|b|] * q + r
H3:0 <= r < [|b|]
H5:[|r|] = r
H6:[|q|] = q
[|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
  apply Z.mul_le_mono_nonneg; generalize wB_pos; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
q, r:Z
H1:q = [|a|] / [|b|]
H4:r = [|a|] mod [|b|]
H2:[|a|] = [|b|] * q + r
H3:0 <= r < [|b|]
H5:[|r|] = r
H6:[|q|] = q
[|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
 rewrite H5, H6; rewrite Z.mul_comm; auto with zarith.
 Qed.

 Definition div_gt := div.

 Lemma spec_div_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] ->
      let (q,r) := div_gt a b in
      [|a|] = [|q|] * [|b|] + [|r|] /\
      0 <= [|r|] < [|b|].digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall a b : Z,
[|a|] > [|b|] ->
0 < [|b|] ->
let (q, r) := div_gt a b in
[|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall a b : Z,
[|a|] > [|b|] ->
0 < [|b|] ->
let (q, r) := div_gt a b in
[|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
 intros.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:[|a|] > [|b|]
H0:0 < [|b|]
let (q, r) := div_gt a b in
[|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
 apply spec_div; auto.
 Qed.

 Definition modulo x y := [|x|] mod [|y|].
 Definition modulo_gt x y := [|x|] mod [|y|].

 Lemma spec_modulo :  forall a b, 0 < [|b|] ->
      [|modulo a b|] = [|a|] mod [|b|].digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall a b : Z,
0 < [|b|] -> [|modulo a b|] = [|a|] mod [|b|]
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall a b : Z,
0 < [|b|] -> [|modulo a b|] = [|a|] mod [|b|]
 intros; unfold modulo.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
[|[|a|] mod [|b|]|] = [|a|] mod [|b|]
 apply Zmod_small.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
0 <= [|a|] mod [|b|] < wB
 assert ([|b|]>0) by auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
0 <= [|a|] mod [|b|] < wB
 generalize (Z_mod_lt [|a|] [|b|] H0) (Z_mod_lt b wB wB_pos).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 < [|b|]
H0:[|b|] > 0
0 <= [|a|] mod [|b|] < [|b|] ->
0 <= b mod wB < wB -> 0 <= [|a|] mod [|b|] < wB
 fold [|b|]; omega.
 Qed.

 Lemma spec_modulo_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] ->
      [|modulo_gt a b|] = [|a|] mod [|b|].digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall a b : Z,
[|a|] > [|b|] ->
0 < [|b|] -> [|modulo_gt a b|] = [|a|] mod [|b|]
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall a b : Z,
[|a|] > [|b|] ->
0 < [|b|] -> [|modulo_gt a b|] = [|a|] mod [|b|]
 intros; apply spec_modulo; auto.
 Qed.

 Definition gcd x y := Z.gcd [|x|] [|y|].
 Definition gcd_gt x y := Z.gcd [|x|] [|y|].

 Lemma Zgcd_bound : forall a b, 0<=a -> 0<=b -> Z.gcd a b <= Z.max a b.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall a b : Z,
0 <= a -> 0 <= b -> Z.gcd a b <= Z.max a b
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall a b : Z,
0 <= a -> 0 <= b -> Z.gcd a b <= Z.max a b
 intros.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= a
H0:0 <= b
Z.gcd a b <= Z.max a b
 generalize (Zgcd_is_gcd a b); inversion_clear 1.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= a
H0:0 <= b
H2:(Z.gcd a b | a)
H3:(Z.gcd a b | b)
H4:forall x : Z,
(x | a) -> (x | b) -> (x | Z.gcd a b)
Z.gcd a b <= Z.max a b
 destruct H2 as (q,H2); destruct H3 as (q',H3); clear H4.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= a
H0:0 <= b
q:Z
H2:a = q * Z.gcd a b
q':Z
H3:b = q' * Z.gcd a b
Z.gcd a b <= Z.max a b
 assert (H4:=Z.gcd_nonneg a b).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= a
H0:0 <= b
q:Z
H2:a = q * Z.gcd a b
q':Z
H3:b = q' * Z.gcd a b
H4:0 <= Z.gcd a b
Z.gcd a b <= Z.max a b
 destruct (Z.eq_dec (Z.gcd a b) 0) as [->|Hneq].digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= a
H0:0 <= b
q:Z
H2:a = q * Z.gcd a b
q':Z
H3:b = q' * Z.gcd a b
H4:0 <= Z.gcd a b
0 <= Z.max a b
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= a
H0:0 <= b
q:Z
H2:a = q * Z.gcd a b
q':Z
H3:b = q' * Z.gcd a b
H4:0 <= Z.gcd a b
Hneq:Z.gcd a b <> 0
Z.gcd a b <= Z.max a b
 generalize (Zmax_spec a b); omega.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= a
H0:0 <= b
q:Z
H2:a = q * Z.gcd a b
q':Z
H3:b = q' * Z.gcd a b
H4:0 <= Z.gcd a b
Hneq:Z.gcd a b <> 0
Z.gcd a b <= Z.max a b
 assert (0 <= q).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= a
H0:0 <= b
q:Z
H2:a = q * Z.gcd a b
q':Z
H3:b = q' * Z.gcd a b
H4:0 <= Z.gcd a b
Hneq:Z.gcd a b <> 0
0 <= q
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= a
H0:0 <= b
q:Z
H2:a = q * Z.gcd a b
q':Z
H3:b = q' * Z.gcd a b
H4:0 <= Z.gcd a b
Hneq:Z.gcd a b <> 0
H1:0 <= q
Z.gcd a b <= Z.max a b
  apply Z.mul_le_mono_pos_r with (Z.gcd a b); auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= a
H0:0 <= b
q:Z
H2:a = q * Z.gcd a b
q':Z
H3:b = q' * Z.gcd a b
H4:0 <= Z.gcd a b
Hneq:Z.gcd a b <> 0
H1:0 <= q
Z.gcd a b <= Z.max a b
 destruct (Z.eq_dec q 0).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= a
H0:0 <= b
q:Z
H2:a = q * Z.gcd a b
q':Z
H3:b = q' * Z.gcd a b
H4:0 <= Z.gcd a b
Hneq:Z.gcd a b <> 0
H1:0 <= q
e:q = 0
Z.gcd a b <= Z.max a b
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= a
H0:0 <= b
q:Z
H2:a = q * Z.gcd a b
q':Z
H3:b = q' * Z.gcd a b
H4:0 <= Z.gcd a b
Hneq:Z.gcd a b <> 0
H1:0 <= q
n:q <> 0
Z.gcd a b <= Z.max a b

 subst q; simpl in *; subst a; simpl; auto.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
b:Z
H:0 <= 0
H0:0 <= b
q':Z
Hneq:Z.gcd 0 b <> 0
H4:0 <= Z.gcd 0 b
H3:b = q' * Z.gcd 0 b
H1:0 <= 0
Z.abs b <= Z.max 0 b
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= a
H0:0 <= b
q:Z
H2:a = q * Z.gcd a b
q':Z
H3:b = q' * Z.gcd a b
H4:0 <= Z.gcd a b
Hneq:Z.gcd a b <> 0
H1:0 <= q
n:q <> 0
Z.gcd a b <= Z.max a b
 generalize (Zmax_spec 0 b) (Zabs_spec b); omega.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= a
H0:0 <= b
q:Z
H2:a = q * Z.gcd a b
q':Z
H3:b = q' * Z.gcd a b
H4:0 <= Z.gcd a b
Hneq:Z.gcd a b <> 0
H1:0 <= q
n:q <> 0
Z.gcd a b <= Z.max a b

 apply Z.le_trans with a.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= a
H0:0 <= b
q:Z
H2:a = q * Z.gcd a b
q':Z
H3:b = q' * Z.gcd a b
H4:0 <= Z.gcd a b
Hneq:Z.gcd a b <> 0
H1:0 <= q
n:q <> 0
Z.gcd a b <= a
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= a
H0:0 <= b
q:Z
H2:a = q * Z.gcd a b
q':Z
H3:b = q' * Z.gcd a b
H4:0 <= Z.gcd a b
Hneq:Z.gcd a b <> 0
H1:0 <= q
n:q <> 0
a <= Z.max a b
 rewrite H2 at 2.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= a
H0:0 <= b
q:Z
H2:a = q * Z.gcd a b
q':Z
H3:b = q' * Z.gcd a b
H4:0 <= Z.gcd a b
Hneq:Z.gcd a b <> 0
H1:0 <= q
n:q <> 0
Z.gcd a b <= q * Z.gcd a b
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= a
H0:0 <= b
q:Z
H2:a = q * Z.gcd a b
q':Z
H3:b = q' * Z.gcd a b
H4:0 <= Z.gcd a b
Hneq:Z.gcd a b <> 0
H1:0 <= q
n:q <> 0
a <= Z.max a b
 rewrite <- (Z.mul_1_l (Z.gcd a b)) at 1.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= a
H0:0 <= b
q:Z
H2:a = q * Z.gcd a b
q':Z
H3:b = q' * Z.gcd a b
H4:0 <= Z.gcd a b
Hneq:Z.gcd a b <> 0
H1:0 <= q
n:q <> 0
1 * Z.gcd a b <= q * Z.gcd a b
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= a
H0:0 <= b
q:Z
H2:a = q * Z.gcd a b
q':Z
H3:b = q' * Z.gcd a b
H4:0 <= Z.gcd a b
Hneq:Z.gcd a b <> 0
H1:0 <= q
n:q <> 0
a <= Z.max a b
 apply Z.mul_le_mono_nonneg; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= a
H0:0 <= b
q:Z
H2:a = q * Z.gcd a b
q':Z
H3:b = q' * Z.gcd a b
H4:0 <= Z.gcd a b
Hneq:Z.gcd a b <> 0
H1:0 <= q
n:q <> 0
a <= Z.max a b
 generalize (Zmax_spec a b); omega.
 Qed.

 Lemma spec_gcd : forall a b, Zis_gcd [|a|] [|b|] [|gcd a b|].digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall a b : Z, Zis_gcd [|a|] [|b|] [|gcd a b|]
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall a b : Z, Zis_gcd [|a|] [|b|] [|gcd a b|]
 intros; unfold gcd.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
Zis_gcd [|a|] [|b|] [|Z.gcd [|a|] [|b|]|]
 generalize (Z_mod_lt a wB wB_pos)(Z_mod_lt b wB wB_pos); intros.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= a mod wB < wB
H0:0 <= b mod wB < wB
Zis_gcd [|a|] [|b|] [|Z.gcd [|a|] [|b|]|]
 fold [|a|] in *; fold [|b|] in *.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= [|a|] < wB
H0:0 <= [|b|] < wB
Zis_gcd [|a|] [|b|] [|Z.gcd [|a|] [|b|]|]
 replace ([|Z.gcd [|a|] [|b|]|]) with (Z.gcd [|a|] [|b|]).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= [|a|] < wB
H0:0 <= [|b|] < wB
Zis_gcd [|a|] [|b|] (Z.gcd [|a|] [|b|])
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= [|a|] < wB
H0:0 <= [|b|] < wB
Z.gcd [|a|] [|b|] = [|Z.gcd [|a|] [|b|]|]
 apply Zgcd_is_gcd.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= [|a|] < wB
H0:0 <= [|b|] < wB
Z.gcd [|a|] [|b|] = [|Z.gcd [|a|] [|b|]|]
 symmetry; apply Zmod_small.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= [|a|] < wB
H0:0 <= [|b|] < wB
0 <= Z.gcd [|a|] [|b|] < wB
 split.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= [|a|] < wB
H0:0 <= [|b|] < wB
0 <= Z.gcd [|a|] [|b|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= [|a|] < wB
H0:0 <= [|b|] < wB
Z.gcd [|a|] [|b|] < wB
 apply Z.gcd_nonneg.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= [|a|] < wB
H0:0 <= [|b|] < wB
Z.gcd [|a|] [|b|] < wB
 apply Z.le_lt_trans with (Z.max [|a|] [|b|]).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= [|a|] < wB
H0:0 <= [|b|] < wB
Z.gcd [|a|] [|b|] <= Z.max [|a|] [|b|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= [|a|] < wB
H0:0 <= [|b|] < wB
Z.max [|a|] [|b|] < wB
 apply Zgcd_bound; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:0 <= [|a|] < wB
H0:0 <= [|b|] < wB
Z.max [|a|] [|b|] < wB
 generalize (Zmax_spec [|a|] [|b|]); omega.
 Qed.

 Lemma spec_gcd_gt : forall a b, [|a|] > [|b|] ->
      Zis_gcd [|a|] [|b|] [|gcd_gt a b|].digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall a b : Z,
[|a|] > [|b|] -> Zis_gcd [|a|] [|b|] [|gcd_gt a b|]
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall a b : Z,
[|a|] > [|b|] -> Zis_gcd [|a|] [|b|] [|gcd_gt a b|]
  intros.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a, b:Z
H:[|a|] > [|b|]
Zis_gcd [|a|] [|b|] [|gcd_gt a b|] apply spec_gcd; auto.
 Qed.

 Definition div21 a1 a2 b :=
  Z.div_eucl ([|a1|]*wB+[|a2|]) [|b|].

 Lemma spec_div21 : forall a1 a2 b,
      wB/2 <= [|b|] ->
      [|a1|] < [|b|] ->
      let (q,r) := div21 a1 a2 b in
      [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\
      0 <= [|r|] < [|b|].digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall a1 a2 b : Z,
wB / 2 <= [|b|] ->
[|a1|] < [|b|] ->
let (q, r) := div21 a1 a2 b in
[|a1|] * wB + [|a2|] = [|q|] * [|b|] + [|r|] /\
0 <= [|r|] < [|b|]
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall a1 a2 b : Z,
wB / 2 <= [|b|] ->
[|a1|] < [|b|] ->
let (q, r) := div21 a1 a2 b in
[|a1|] * wB + [|a2|] = [|q|] * [|b|] + [|r|] /\
0 <= [|r|] < [|b|]
 intros; unfold div21.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
let (q, r) :=
  Z.div_eucl ([|a1|] * wB + [|a2|]) [|b|] in
[|a1|] * wB + [|a2|] = [|q|] * [|b|] + [|r|] /\
0 <= [|r|] < [|b|]
 generalize (Z_mod_lt a1 wB wB_pos); fold [|a1|]; intros.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
let (q, r) :=
  Z.div_eucl ([|a1|] * wB + [|a2|]) [|b|] in
[|a1|] * wB + [|a2|] = [|q|] * [|b|] + [|r|] /\
0 <= [|r|] < [|b|]
 generalize (Z_mod_lt a2 wB wB_pos); fold [|a2|]; intros.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
let (q, r) :=
  Z.div_eucl ([|a1|] * wB + [|a2|]) [|b|] in
[|a1|] * wB + [|a2|] = [|q|] * [|b|] + [|r|] /\
0 <= [|r|] < [|b|]
 assert ([|b|]>0) by auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
let (q, r) :=
  Z.div_eucl ([|a1|] * wB + [|a2|]) [|b|] in
[|a1|] * wB + [|a2|] = [|q|] * [|b|] + [|r|] /\
0 <= [|r|] < [|b|]
 remember ([|a1|]*wB+[|a2|]) as a.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
let (q, r) := Z.div_eucl a [|b|] in
a = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
 assert (Z.div_eucl a [|b|] = (a/[|b|], a mod [|b|])).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
Z.div_eucl a [|b|] = (a / [|b|], a mod [|b|])
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
H4:Z.div_eucl a [|b|] = (a / [|b|], a mod [|b|])
let (q, r) := Z.div_eucl a [|b|] in
a = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
  unfold Z.modulo, Z.div; destruct Z.div_eucl; auto.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
H4:Z.div_eucl a [|b|] = (a / [|b|], a mod [|b|])
let (q, r) := Z.div_eucl a [|b|] in
a = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
 generalize (Z_div_mod a [|b|] H3).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
H4:Z.div_eucl a [|b|] = (a / [|b|], a mod [|b|])
(let (q, r) := Z.div_eucl a [|b|] in
 a = [|b|] * q + r /\ 0 <= r < [|b|]) ->
let (q, r) := Z.div_eucl a [|b|] in
a = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
 destruct Z.div_eucl as (q,r); destruct 1; intros.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
q, r:Z
H4:(q, r) = (a / [|b|], a mod [|b|])
H5:a = [|b|] * q + r
H6:0 <= r < [|b|]
a = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
 injection H4 as ? ?.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
q, r:Z
H4:q = a / [|b|]
H7:r = a mod [|b|]
H5:a = [|b|] * q + r
H6:0 <= r < [|b|]
a = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
 assert ([|r|]=r).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
q, r:Z
H4:q = a / [|b|]
H7:r = a mod [|b|]
H5:a = [|b|] * q + r
H6:0 <= r < [|b|]
[|r|] = r
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
q, r:Z
H4:q = a / [|b|]
H7:r = a mod [|b|]
H5:a = [|b|] * q + r
H6:0 <= r < [|b|]
H8:[|r|] = r
a = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
  apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|];
   auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
q, r:Z
H4:q = a / [|b|]
H7:r = a mod [|b|]
H5:a = [|b|] * q + r
H6:0 <= r < [|b|]
H8:[|r|] = r
a = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
 assert ([|q|]=q).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
q, r:Z
H4:q = a / [|b|]
H7:r = a mod [|b|]
H5:a = [|b|] * q + r
H6:0 <= r < [|b|]
H8:[|r|] = r
[|q|] = q
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
q, r:Z
H4:q = a / [|b|]
H7:r = a mod [|b|]
H5:a = [|b|] * q + r
H6:0 <= r < [|b|]
H8:[|r|] = r
H9:[|q|] = q
a = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
  apply Zmod_small.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
q, r:Z
H4:q = a / [|b|]
H7:r = a mod [|b|]
H5:a = [|b|] * q + r
H6:0 <= r < [|b|]
H8:[|r|] = r
0 <= q < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
q, r:Z
H4:q = a / [|b|]
H7:r = a mod [|b|]
H5:a = [|b|] * q + r
H6:0 <= r < [|b|]
H8:[|r|] = r
H9:[|q|] = q
a = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
  subst q.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
r:Z
H7:r = a mod [|b|]
H5:a = [|b|] * (a / [|b|]) + r
H6:0 <= r < [|b|]
H8:[|r|] = r
0 <= a / [|b|] < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
q, r:Z
H4:q = a / [|b|]
H7:r = a mod [|b|]
H5:a = [|b|] * q + r
H6:0 <= r < [|b|]
H8:[|r|] = r
H9:[|q|] = q
a = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
  split.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
r:Z
H7:r = a mod [|b|]
H5:a = [|b|] * (a / [|b|]) + r
H6:0 <= r < [|b|]
H8:[|r|] = r
0 <= a / [|b|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
r:Z
H7:r = a mod [|b|]
H5:a = [|b|] * (a / [|b|]) + r
H6:0 <= r < [|b|]
H8:[|r|] = r
a / [|b|] < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
q, r:Z
H4:q = a / [|b|]
H7:r = a mod [|b|]
H5:a = [|b|] * q + r
H6:0 <= r < [|b|]
H8:[|r|] = r
H9:[|q|] = q
a = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
  apply Z_div_pos; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
r:Z
H7:r = a mod [|b|]
H5:a = [|b|] * (a / [|b|]) + r
H6:0 <= r < [|b|]
H8:[|r|] = r
0 <= a
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
r:Z
H7:r = a mod [|b|]
H5:a = [|b|] * (a / [|b|]) + r
H6:0 <= r < [|b|]
H8:[|r|] = r
a / [|b|] < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
q, r:Z
H4:q = a / [|b|]
H7:r = a mod [|b|]
H5:a = [|b|] * q + r
H6:0 <= r < [|b|]
H8:[|r|] = r
H9:[|q|] = q
a = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
  subst a; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
r:Z
H7:r = a mod [|b|]
H5:a = [|b|] * (a / [|b|]) + r
H6:0 <= r < [|b|]
H8:[|r|] = r
a / [|b|] < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
q, r:Z
H4:q = a / [|b|]
H7:r = a mod [|b|]
H5:a = [|b|] * q + r
H6:0 <= r < [|b|]
H8:[|r|] = r
H9:[|q|] = q
a = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
  apply Zdiv_lt_upper_bound; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
r:Z
H7:r = a mod [|b|]
H5:a = [|b|] * (a / [|b|]) + r
H6:0 <= r < [|b|]
H8:[|r|] = r
a < wB * [|b|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
q, r:Z
H4:q = a / [|b|]
H7:r = a mod [|b|]
H5:a = [|b|] * q + r
H6:0 <= r < [|b|]
H8:[|r|] = r
H9:[|q|] = q
a = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
  subst a.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
r:Z
H5:[|a1|] * wB + [|a2|] =
[|b|] * (([|a1|] * wB + [|a2|]) / [|b|]) + r
H7:r = ([|a1|] * wB + [|a2|]) mod [|b|]
H6:0 <= r < [|b|]
H8:[|r|] = r
[|a1|] * wB + [|a2|] < wB * [|b|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
q, r:Z
H4:q = a / [|b|]
H7:r = a mod [|b|]
H5:a = [|b|] * q + r
H6:0 <= r < [|b|]
H8:[|r|] = r
H9:[|q|] = q
a = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
  replace (wB*[|b|]) with (([|b|]-1)*wB + wB) by ring.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
r:Z
H5:[|a1|] * wB + [|a2|] =
[|b|] * (([|a1|] * wB + [|a2|]) / [|b|]) + r
H7:r = ([|a1|] * wB + [|a2|]) mod [|b|]
H6:0 <= r < [|b|]
H8:[|r|] = r
[|a1|] * wB + [|a2|] < ([|b|] - 1) * wB + wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
q, r:Z
H4:q = a / [|b|]
H7:r = a mod [|b|]
H5:a = [|b|] * q + r
H6:0 <= r < [|b|]
H8:[|r|] = r
H9:[|q|] = q
a = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
  apply Z.lt_le_trans with ([|a1|]*wB+wB); auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
a1, a2, b:Z
H:wB / 2 <= [|b|]
H0:[|a1|] < [|b|]
H1:0 <= [|a1|] < wB
H2:0 <= [|a2|] < wB
H3:[|b|] > 0
a:Z
Heqa:a = [|a1|] * wB + [|a2|]
q, r:Z
H4:q = a / [|b|]
H7:r = a mod [|b|]
H5:a = [|b|] * q + r
H6:0 <= r < [|b|]
H8:[|r|] = r
H9:[|q|] = q
a = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]
 rewrite H8, H9; rewrite Z.mul_comm; auto with zarith.
 Qed.

 Definition add_mul_div p x y :=
   ([|x|] * (2 ^ [|p|]) + [|y|] / (2 ^ ((Zpos digits) - [|p|]))).
 Lemma spec_add_mul_div : forall x y p,
       [|p|] <= Zpos digits ->
       [| add_mul_div p x y |] =
         ([|x|] * (2 ^ [|p|]) +
          [|y|] / (2 ^ ((Zpos digits) - [|p|]))) mod wB.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y p : Z,
[|p|] <= Z.pos digits ->
[|add_mul_div p x y|] =
([|x|] * 2 ^ [|p|] +
 [|y|] / 2 ^ (Z.pos digits - [|p|])) mod wB
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y p : Z,
[|p|] <= Z.pos digits ->
[|add_mul_div p x y|] =
([|x|] * 2 ^ [|p|] +
 [|y|] / 2 ^ (Z.pos digits - [|p|])) mod wB
 intros; unfold add_mul_div; auto.
 Qed.

 Definition pos_mod p w := [|w|] mod (2 ^ [|p|]).
 Lemma spec_pos_mod : forall w p,
       [|pos_mod p w|] = [|w|] mod (2 ^ [|p|]).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall w p : Z, [|pos_mod p w|] = [|w|] mod 2 ^ [|p|]
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall w p : Z, [|pos_mod p w|] = [|w|] mod 2 ^ [|p|]
 intros; unfold pos_mod.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
w, p:Z
[|[|w|] mod 2 ^ [|p|]|] = [|w|] mod 2 ^ [|p|]
 apply Zmod_small.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
w, p:Z
0 <= [|w|] mod 2 ^ [|p|] < wB
 generalize (Z_mod_lt [|w|] (2 ^ [|p|])); intros.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
w, p:Z
H:2 ^ [|p|] > 0 ->
0 <= [|w|] mod 2 ^ [|p|] < 2 ^ [|p|]
0 <= [|w|] mod 2 ^ [|p|] < wB
 split.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
w, p:Z
H:2 ^ [|p|] > 0 ->
0 <= [|w|] mod 2 ^ [|p|] < 2 ^ [|p|]
0 <= [|w|] mod 2 ^ [|p|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
w, p:Z
H:2 ^ [|p|] > 0 ->
0 <= [|w|] mod 2 ^ [|p|] < 2 ^ [|p|]
[|w|] mod 2 ^ [|p|] < wB
 destruct H; auto using Z.lt_gt with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
w, p:Z
H:2 ^ [|p|] > 0 ->
0 <= [|w|] mod 2 ^ [|p|] < 2 ^ [|p|]
[|w|] mod 2 ^ [|p|] < wB
 apply Z.le_lt_trans with [|w|]; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
w, p:Z
H:2 ^ [|p|] > 0 ->
0 <= [|w|] mod 2 ^ [|p|] < 2 ^ [|p|]
[|w|] mod 2 ^ [|p|] <= [|w|]
 apply Zmod_le; auto with zarith.
 Qed.

 Definition is_even x :=
   if Z.eq_dec ([|x|] mod 2) 0 then true else false.

 Lemma spec_is_even : forall x,
      if is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z,
if is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z,
if is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1
 intros; unfold is_even; destruct Z.eq_dec; auto.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
n:[|x|] mod 2 <> 0
[|x|] mod 2 = 1
 generalize (Z_mod_lt [|x|] 2); omega.
 Qed.

 Definition sqrt x := Z.sqrt [|x|].
 Lemma spec_sqrt : forall x,
       [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z,
[|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z,
[|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2
 intros.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
[|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2
 unfold sqrt.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
[|Z.sqrt [|x|]|] ^ 2 <= [|x|] <
([|Z.sqrt [|x|]|] + 1) ^ 2
 repeat rewrite Z.pow_2_r.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
[|Z.sqrt [|x|]|] * [|Z.sqrt [|x|]|] <= [|x|] <
([|Z.sqrt [|x|]|] + 1) * ([|Z.sqrt [|x|]|] + 1)
 replace [|Z.sqrt [|x|]|] with (Z.sqrt [|x|]).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
Z.sqrt [|x|] * Z.sqrt [|x|] <= [|x|] <
(Z.sqrt [|x|] + 1) * (Z.sqrt [|x|] + 1)
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
Z.sqrt [|x|] = [|Z.sqrt [|x|]|]
 apply Z.sqrt_spec; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
Z.sqrt [|x|] = [|Z.sqrt [|x|]|]
 symmetry; apply Zmod_small.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
0 <= Z.sqrt [|x|] < wB
 split.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
0 <= Z.sqrt [|x|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
Z.sqrt [|x|] < wB apply Z.sqrt_nonneg; auto.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
Z.sqrt [|x|] < wB
 apply Z.le_lt_trans with [|x|]; auto.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
Z.sqrt [|x|] <= [|x|]
 apply Z.sqrt_le_lin; auto.
 Qed.

 Definition sqrt2 x y :=
  let z := [|x|]*wB+[|y|] in
  match z with
   | Z0 => (0, C0 0)
   | Zpos p =>
      let (s,r) := Z.sqrtrem (Zpos p) in
      (s, if Z_lt_le_dec r wB then C0 r else C1 (r-wB))
   | Zneg _ => (0, C0 0)
  end.

 Lemma spec_sqrt2 : forall x y,
       wB/ 4 <= [|x|] ->
       let (s,r) := sqrt2 x y in
          [||WW x y||] = [|s|] ^ 2 + [+|r|] /\
          [+|r|] <= 2 * [|s|].digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y : Z,
wB / 4 <= [|x|] ->
let (s, r) := sqrt2 x y in
[||WW x y||] = [|s|] ^ 2 + [+|r|] /\
[+|r|] <= 2 * [|s|]
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x y : Z,
wB / 4 <= [|x|] ->
let (s, r) := sqrt2 x y in
[||WW x y||] = [|s|] ^ 2 + [+|r|] /\
[+|r|] <= 2 * [|s|]
 intros; unfold sqrt2.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
let (s, r) :=
  match [|x|] * wB + [|y|] with
  | Z.pos p =>
      let (s, r) := Z.sqrtrem (Z.pos p) in
      (s,
      if Z_lt_le_dec r wB then C0 r else C1 (r - wB))
  | _ => (0, C0 0)
  end in
[||WW x y||] = [|s|] ^ 2 + [+|r|] /\
[+|r|] <= 2 * [|s|]
 simpl zn2z_to_Z.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
let (s, r) :=
  match [|x|] * wB + [|y|] with
  | Z.pos p =>
      let (s, r) := Z.sqrtrem (Z.pos p) in
      (s,
      if Z_lt_le_dec r wB then C0 r else C1 (r - wB))
  | _ => (0, C0 0)
  end in
[|x|] * wB + [|y|] = [|s|] ^ 2 + [+|r|] /\
[+|r|] <= 2 * [|s|]
 remember ([|x|]*wB+[|y|]) as z.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
z:Z
Heqz:z = [|x|] * wB + [|y|]
let (s, r) :=
  match z with
  | Z.pos p =>
      let (s, r) := Z.sqrtrem (Z.pos p) in
      (s,
      if Z_lt_le_dec r wB then C0 r else C1 (r - wB))
  | _ => (0, C0 0)
  end in
z = [|s|] ^ 2 + [+|r|] /\ [+|r|] <= 2 * [|s|]
 destruct z.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
Heqz:0 = [|x|] * wB + [|y|]
0 = [|0|] ^ 2 + [+|C0 0|] /\ [+|C0 0|] <= 2 * [|0|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
let (s, r) :=
  let (s, r) := Z.sqrtrem (Z.pos p) in
  (s, if Z_lt_le_dec r wB then C0 r else C1 (r - wB)) in
Z.pos p = [|s|] ^ 2 + [+|r|] /\ [+|r|] <= 2 * [|s|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
 auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
let (s, r) :=
  let (s, r) := Z.sqrtrem (Z.pos p) in
  (s, if Z_lt_le_dec r wB then C0 r else C1 (r - wB)) in
Z.pos p = [|s|] ^ 2 + [+|r|] /\ [+|r|] <= 2 * [|s|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
 generalize (Z.sqrtrem_spec (Zpos p)).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
(0 <= Z.pos p ->
 let (s, r) := Z.sqrtrem (Z.pos p) in
 Z.pos p = s * s + r /\ 0 <= r <= 2 * s) ->
let (s, r) :=
  let (s, r) := Z.sqrtrem (Z.pos p) in
  (s, if Z_lt_le_dec r wB then C0 r else C1 (r - wB)) in
Z.pos p = [|s|] ^ 2 + [+|r|] /\ [+|r|] <= 2 * [|s|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
 destruct Z.sqrtrem as (s,r); intros [U V]; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
Z.pos p =
[|s|] ^ 2 +
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] /\
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] <=
2 * [|s|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
 assert (s < wB).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
s < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
H0:s < wB
Z.pos p =
[|s|] ^ 2 +
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] /\
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] <=
2 * [|s|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
  destruct (Z_lt_le_dec s wB); auto.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
l:wB <= s
s < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
H0:s < wB
Z.pos p =
[|s|] ^ 2 +
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] /\
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] <=
2 * [|s|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
  assert (wB * wB <= Zpos p).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
l:wB <= s
wB * wB <= Z.pos p
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
l:wB <= s
H0:wB * wB <= Z.pos p
s < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
H0:s < wB
Z.pos p =
[|s|] ^ 2 +
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] /\
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] <=
2 * [|s|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
   rewrite U.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
l:wB <= s
wB * wB <= s * s + r
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
l:wB <= s
H0:wB * wB <= Z.pos p
s < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
H0:s < wB
Z.pos p =
[|s|] ^ 2 +
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] /\
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] <=
2 * [|s|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
   apply Z.le_trans with (s*s); try omega.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
l:wB <= s
wB * wB <= s * s
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
l:wB <= s
H0:wB * wB <= Z.pos p
s < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
H0:s < wB
Z.pos p =
[|s|] ^ 2 +
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] /\
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] <=
2 * [|s|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
   apply Z.mul_le_mono_nonneg; generalize wB_pos; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
l:wB <= s
H0:wB * wB <= Z.pos p
s < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
H0:s < wB
Z.pos p =
[|s|] ^ 2 +
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] /\
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] <=
2 * [|s|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
  assert (Zpos p < wB*wB).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
l:wB <= s
H0:wB * wB <= Z.pos p
Z.pos p < wB * wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
l:wB <= s
H0:wB * wB <= Z.pos p
H1:Z.pos p < wB * wB
s < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
H0:s < wB
Z.pos p =
[|s|] ^ 2 +
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] /\
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] <=
2 * [|s|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
   rewrite Heqz.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
l:wB <= s
H0:wB * wB <= Z.pos p
[|x|] * wB + [|y|] < wB * wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
l:wB <= s
H0:wB * wB <= Z.pos p
H1:Z.pos p < wB * wB
s < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
H0:s < wB
Z.pos p =
[|s|] ^ 2 +
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] /\
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] <=
2 * [|s|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
   replace (wB*wB) with ((wB-1)*wB+wB) by ring.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
l:wB <= s
H0:wB * wB <= Z.pos p
[|x|] * wB + [|y|] < (wB - 1) * wB + wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
l:wB <= s
H0:wB * wB <= Z.pos p
H1:Z.pos p < wB * wB
s < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
H0:s < wB
Z.pos p =
[|s|] ^ 2 +
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] /\
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] <=
2 * [|s|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
   apply Z.add_le_lt_mono; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
l:wB <= s
H0:wB * wB <= Z.pos p
[|x|] * wB <= (wB - 1) * wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
l:wB <= s
H0:wB * wB <= Z.pos p
H1:Z.pos p < wB * wB
s < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
H0:s < wB
Z.pos p =
[|s|] ^ 2 +
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] /\
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] <=
2 * [|s|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
   apply Z.mul_le_mono_nonneg; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
l:wB <= s
H0:wB * wB <= Z.pos p
[|x|] <= wB - 1
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
l:wB <= s
H0:wB * wB <= Z.pos p
0 <= wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
l:wB <= s
H0:wB * wB <= Z.pos p
H1:Z.pos p < wB * wB
s < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
H0:s < wB
Z.pos p =
[|s|] ^ 2 +
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] /\
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] <=
2 * [|s|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
   generalize (spec_to_Z x); auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
l:wB <= s
H0:wB * wB <= Z.pos p
0 <= wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
l:wB <= s
H0:wB * wB <= Z.pos p
H1:Z.pos p < wB * wB
s < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
H0:s < wB
Z.pos p =
[|s|] ^ 2 +
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] /\
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] <=
2 * [|s|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
   generalize wB_pos; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
l:wB <= s
H0:wB * wB <= Z.pos p
H1:Z.pos p < wB * wB
s < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
H0:s < wB
Z.pos p =
[|s|] ^ 2 +
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] /\
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] <=
2 * [|s|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
  omega.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
H0:s < wB
Z.pos p =
[|s|] ^ 2 +
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] /\
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] <=
2 * [|s|]
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
 replace [|s|] with s by (symmetry; apply Zmod_small; auto with zarith).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
H0:s < wB
Z.pos p =
s ^ 2 +
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] /\
[+|(if Z_lt_le_dec r wB then C0 r else C1 (r - wB))|] <=
2 * s
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
 destruct Z_lt_le_dec; unfold interp_carry.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
H0:s < wB
l:r < wB
Z.pos p = s ^ 2 + [|r|] /\ [|r|] <= 2 * s
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
H0:s < wB
l:wB <= r
Z.pos p = s ^ 2 + (1 * wB + [|r - wB|]) /\
1 * wB + [|r - wB|] <= 2 * s
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
 replace [|r|] with r by (symmetry; apply Zmod_small; auto with zarith).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
H0:s < wB
l:r < wB
Z.pos p = s ^ 2 + r /\ r <= 2 * s
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
H0:s < wB
l:wB <= r
Z.pos p = s ^ 2 + (1 * wB + [|r - wB|]) /\
1 * wB + [|r - wB|] <= 2 * s
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
 rewrite Z.pow_2_r; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
H0:s < wB
l:wB <= r
Z.pos p = s ^ 2 + (1 * wB + [|r - wB|]) /\
1 * wB + [|r - wB|] <= 2 * s
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
 replace [|r-wB|] with (r-wB) by (symmetry; apply Zmod_small; auto with zarith).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.pos p = [|x|] * wB + [|y|]
s, r:Z
U:Z.pos p = s * s + r
V:0 <= r <= 2 * s
H0:s < wB
l:wB <= r
Z.pos p = s ^ 2 + (1 * wB + (r - wB)) /\
1 * wB + (r - wB) <= 2 * s
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
 rewrite Z.pow_2_r; omega.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]

 assert (0<=Zneg p).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
0 <= Z.neg p
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
H0:0 <= Z.neg p
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
  rewrite Heqz; generalize wB_pos; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
H:wB / 4 <= [|x|]
p:positive
Heqz:Z.neg p = [|x|] * wB + [|y|]
H0:0 <= Z.neg p
Z.neg p = [|0|] ^ 2 + [+|C0 0|] /\
[+|C0 0|] <= 2 * [|0|]
 compute in H0; elim H0; auto.
 Qed.

 Lemma two_p_power2 : forall x, x>=0 -> two_p x = 2 ^ x.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, x >= 0 -> two_p x = 2 ^ x
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, x >= 0 -> two_p x = 2 ^ x
 intros.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:x >= 0
two_p x = 2 ^ x
 unfold two_p.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:x >= 0
match x with
| 0 => 1
| Z.pos y => two_power_pos y
| Z.neg _ => 0
end = 2 ^ x
 destruct x; simpl; auto.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
H:Z.pos p >= 0
two_power_pos p = Z.pow_pos 2 p
 apply two_power_pos_correct.
 Qed.

 Definition head0 x := match [|x|] with
   | Z0 => zdigits
   | Zpos p => zdigits - log_inf p - 1
   | _ => 0
  end.

 Lemma spec_head00:  forall x, [|x|] = 0 -> [|head0 x|] = Zpos digits.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, [|x|] = 0 -> [|head0 x|] = Z.pos digits
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, [|x|] = 0 -> [|head0 x|] = Z.pos digits
  unfold head0; intros.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:[|x|] = 0
[|match [|x|] with
  | 0 => zdigits
  | Z.pos p => zdigits - log_inf p - 1
  | Z.neg _ => 0
  end|] = Z.pos digits
  rewrite H; simpl.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:[|x|] = 0
[|zdigits|] = Z.pos digits
  apply spec_zdigits.
 Qed.

 Lemma log_inf_bounded : forall x p, Zpos x < 2^p -> log_inf x < p.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall (x : positive) (p : Z),
Z.pos x < 2 ^ p -> log_inf x < p
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall (x : positive) (p : Z),
Z.pos x < 2 ^ p -> log_inf x < p
 induction x; simpl; intros.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:positive
IHx:forall p0 : Z,
Z.pos x < 2 ^ p0 -> log_inf x < p0
p:Z
H:Z.pos x~1 < 2 ^ p
Z.succ (log_inf x) < p
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:positive
IHx:forall p0 : Z,
Z.pos x < 2 ^ p0 -> log_inf x < p0
p:Z
H:Z.pos x~0 < 2 ^ p
Z.succ (log_inf x) < p
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:Z
H:1 < 2 ^ p
0 < p

 assert (0 < p) by (destruct p; compute; auto with zarith; discriminate).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:positive
IHx:forall p0 : Z,
Z.pos x < 2 ^ p0 -> log_inf x < p0
p:Z
H:Z.pos x~1 < 2 ^ p
H0:0 < p
Z.succ (log_inf x) < p
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:positive
IHx:forall p0 : Z,
Z.pos x < 2 ^ p0 -> log_inf x < p0
p:Z
H:Z.pos x~0 < 2 ^ p
Z.succ (log_inf x) < p
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:Z
H:1 < 2 ^ p
0 < p
 cut (log_inf x < p - 1); [omega| ].digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:positive
IHx:forall p0 : Z,
Z.pos x < 2 ^ p0 -> log_inf x < p0
p:Z
H:Z.pos x~1 < 2 ^ p
H0:0 < p
log_inf x < p - 1
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:positive
IHx:forall p0 : Z,
Z.pos x < 2 ^ p0 -> log_inf x < p0
p:Z
H:Z.pos x~0 < 2 ^ p
Z.succ (log_inf x) < p
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:Z
H:1 < 2 ^ p
0 < p
 apply IHx.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:positive
IHx:forall p0 : Z,
Z.pos x < 2 ^ p0 -> log_inf x < p0
p:Z
H:Z.pos x~1 < 2 ^ p
H0:0 < p
Z.pos x < 2 ^ (p - 1)
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:positive
IHx:forall p0 : Z,
Z.pos x < 2 ^ p0 -> log_inf x < p0
p:Z
H:Z.pos x~0 < 2 ^ p
Z.succ (log_inf x) < p
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:Z
H:1 < 2 ^ p
0 < p
 change (Zpos x~1) with (2*(Zpos x)+1) in H.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:positive
IHx:forall p0 : Z,
Z.pos x < 2 ^ p0 -> log_inf x < p0
p:Z
H:2 * Z.pos x + 1 < 2 ^ p
H0:0 < p
Z.pos x < 2 ^ (p - 1)
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:positive
IHx:forall p0 : Z,
Z.pos x < 2 ^ p0 -> log_inf x < p0
p:Z
H:Z.pos x~0 < 2 ^ p
Z.succ (log_inf x) < p
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:Z
H:1 < 2 ^ p
0 < p
 replace p with (Z.succ (p-1)) in H; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:positive
IHx:forall p0 : Z,
Z.pos x < 2 ^ p0 -> log_inf x < p0
p:Z
H:2 * Z.pos x + 1 < 2 ^ Z.succ (p - 1)
H0:0 < p
Z.pos x < 2 ^ (p - 1)
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:positive
IHx:forall p0 : Z,
Z.pos x < 2 ^ p0 -> log_inf x < p0
p:Z
H:Z.pos x~0 < 2 ^ p
Z.succ (log_inf x) < p
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:Z
H:1 < 2 ^ p
0 < p
 rewrite Z.pow_succ_r in H; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:positive
IHx:forall p0 : Z,
Z.pos x < 2 ^ p0 -> log_inf x < p0
p:Z
H:Z.pos x~0 < 2 ^ p
Z.succ (log_inf x) < p
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:Z
H:1 < 2 ^ p
0 < p

 assert (0 < p) by (destruct p; compute; auto with zarith; discriminate).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:positive
IHx:forall p0 : Z,
Z.pos x < 2 ^ p0 -> log_inf x < p0
p:Z
H:Z.pos x~0 < 2 ^ p
H0:0 < p
Z.succ (log_inf x) < p
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:Z
H:1 < 2 ^ p
0 < p
 cut (log_inf x < p - 1); [omega| ].digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:positive
IHx:forall p0 : Z,
Z.pos x < 2 ^ p0 -> log_inf x < p0
p:Z
H:Z.pos x~0 < 2 ^ p
H0:0 < p
log_inf x < p - 1
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:Z
H:1 < 2 ^ p
0 < p
 apply IHx.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:positive
IHx:forall p0 : Z,
Z.pos x < 2 ^ p0 -> log_inf x < p0
p:Z
H:Z.pos x~0 < 2 ^ p
H0:0 < p
Z.pos x < 2 ^ (p - 1)
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:Z
H:1 < 2 ^ p
0 < p
 change (Zpos x~0) with (2*(Zpos x)) in H.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:positive
IHx:forall p0 : Z,
Z.pos x < 2 ^ p0 -> log_inf x < p0
p:Z
H:2 * Z.pos x < 2 ^ p
H0:0 < p
Z.pos x < 2 ^ (p - 1)
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:Z
H:1 < 2 ^ p
0 < p
 replace p with (Z.succ (p-1)) in H; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:positive
IHx:forall p0 : Z,
Z.pos x < 2 ^ p0 -> log_inf x < p0
p:Z
H:2 * Z.pos x < 2 ^ Z.succ (p - 1)
H0:0 < p
Z.pos x < 2 ^ (p - 1)
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:Z
H:1 < 2 ^ p
0 < p
 rewrite Z.pow_succ_r in H; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:Z
H:1 < 2 ^ p
0 < p

 simpl; intros; destruct p; compute; auto with zarith.
 Qed.


 Lemma spec_head0  : forall x,  0 < [|x|] ->
	 wB/ 2 <= 2 ^ ([|head0 x|]) * [|x|] < wB.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z,
0 < [|x|] -> wB / 2 <= 2 ^ [|head0 x|] * [|x|] < wB
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z,
0 < [|x|] -> wB / 2 <= 2 ^ [|head0 x|] * [|x|] < wB
 intros; unfold head0.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:0 < [|x|]
wB / 2 <=
2
^ [|match [|x|] with
    | 0 => zdigits
    | Z.pos p => zdigits - log_inf p - 1
    | Z.neg _ => 0
    end|] * [|x|] < wB
 generalize (spec_to_Z x).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:0 < [|x|]
0 <= [|x|] < wB ->
wB / 2 <=
2
^ [|match [|x|] with
    | 0 => zdigits
    | Z.pos p => zdigits - log_inf p - 1
    | Z.neg _ => 0
    end|] * [|x|] < wB
 destruct [|x|]; try discriminate.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
0 <= Z.pos p < wB ->
wB / 2 <= 2 ^ [|zdigits - log_inf p - 1|] * Z.pos p <
wB
 intros.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
wB / 2 <= 2 ^ [|zdigits - log_inf p - 1|] * Z.pos p <
wB
 destruct (log_inf_correct p).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:two_p (log_inf p) <= Z.pos p <
two_p (Z.succ (log_inf p))
wB / 2 <= 2 ^ [|zdigits - log_inf p - 1|] * Z.pos p <
wB
 rewrite 2 two_p_power2 in H2; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p < 2 ^ Z.succ (log_inf p)
wB / 2 <= 2 ^ [|zdigits - log_inf p - 1|] * Z.pos p <
wB
 assert (0 <= zdigits - log_inf p - 1 < wB).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p < 2 ^ Z.succ (log_inf p)
0 <= zdigits - log_inf p - 1 < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
wB / 2 <= 2 ^ [|zdigits - log_inf p - 1|] * Z.pos p <
wB
  split.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p < 2 ^ Z.succ (log_inf p)
0 <= zdigits - log_inf p - 1
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p < 2 ^ Z.succ (log_inf p)
zdigits - log_inf p - 1 < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
wB / 2 <= 2 ^ [|zdigits - log_inf p - 1|] * Z.pos p <
wB
  cut (log_inf p < zdigits); try omega.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p < 2 ^ Z.succ (log_inf p)
log_inf p < zdigits
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p < 2 ^ Z.succ (log_inf p)
zdigits - log_inf p - 1 < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
wB / 2 <= 2 ^ [|zdigits - log_inf p - 1|] * Z.pos p <
wB
  unfold zdigits.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p < 2 ^ Z.succ (log_inf p)
log_inf p < Z.pos digits
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p < 2 ^ Z.succ (log_inf p)
zdigits - log_inf p - 1 < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
wB / 2 <= 2 ^ [|zdigits - log_inf p - 1|] * Z.pos p <
wB
  unfold wB, base in *.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < 2 ^ Z.pos digits
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p < 2 ^ Z.succ (log_inf p)
log_inf p < Z.pos digits
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p < 2 ^ Z.succ (log_inf p)
zdigits - log_inf p - 1 < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
wB / 2 <= 2 ^ [|zdigits - log_inf p - 1|] * Z.pos p <
wB
  apply log_inf_bounded; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p < 2 ^ Z.succ (log_inf p)
zdigits - log_inf p - 1 < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
wB / 2 <= 2 ^ [|zdigits - log_inf p - 1|] * Z.pos p <
wB
  apply Z.lt_trans with zdigits.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p < 2 ^ Z.succ (log_inf p)
zdigits - log_inf p - 1 < zdigits
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p < 2 ^ Z.succ (log_inf p)
zdigits < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
wB / 2 <= 2 ^ [|zdigits - log_inf p - 1|] * Z.pos p <
wB
  omega.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p < 2 ^ Z.succ (log_inf p)
zdigits < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
wB / 2 <= 2 ^ [|zdigits - log_inf p - 1|] * Z.pos p <
wB
  unfold zdigits, wB, base; apply Zpower2_lt_lin; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
wB / 2 <= 2 ^ [|zdigits - log_inf p - 1|] * Z.pos p <
wB

 unfold to_Z; rewrite (Zmod_small _ _ H3).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
wB / 2 <= 2 ^ (zdigits - log_inf p - 1) * Z.pos p < wB
 destruct H2.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
wB / 2 <= 2 ^ (zdigits - log_inf p - 1) * Z.pos p < wB
 split.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
wB / 2 <= 2 ^ (zdigits - log_inf p - 1) * Z.pos p
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
2 ^ (zdigits - log_inf p - 1) * Z.pos p < wB
 apply Z.le_trans with (2^(zdigits - log_inf p - 1)*(2^log_inf p)).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
wB / 2 <=
2 ^ (zdigits - log_inf p - 1) * 2 ^ log_inf p
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
2 ^ (zdigits - log_inf p - 1) * 2 ^ log_inf p <=
2 ^ (zdigits - log_inf p - 1) * Z.pos p
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
2 ^ (zdigits - log_inf p - 1) * Z.pos p < wB
 apply Zdiv_le_upper_bound; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
wB <=
2 ^ (zdigits - log_inf p - 1) * 2 ^ log_inf p * 2
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
2 ^ (zdigits - log_inf p - 1) * 2 ^ log_inf p <=
2 ^ (zdigits - log_inf p - 1) * Z.pos p
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
2 ^ (zdigits - log_inf p - 1) * Z.pos p < wB
 rewrite <- Zpower_exp; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
wB <= 2 ^ (zdigits - log_inf p - 1 + log_inf p) * 2
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
2 ^ (zdigits - log_inf p - 1) * 2 ^ log_inf p <=
2 ^ (zdigits - log_inf p - 1) * Z.pos p
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
2 ^ (zdigits - log_inf p - 1) * Z.pos p < wB
 rewrite Z.mul_comm; rewrite <- Z.pow_succ_r; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
wB <= 2 ^ Z.succ (zdigits - log_inf p - 1 + log_inf p)
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
2 ^ (zdigits - log_inf p - 1) * 2 ^ log_inf p <=
2 ^ (zdigits - log_inf p - 1) * Z.pos p
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
2 ^ (zdigits - log_inf p - 1) * Z.pos p < wB
 replace (Z.succ (zdigits - log_inf p -1 +log_inf p)) with zdigits
   by ring.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
wB <= 2 ^ zdigits
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
2 ^ (zdigits - log_inf p - 1) * 2 ^ log_inf p <=
2 ^ (zdigits - log_inf p - 1) * Z.pos p
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
2 ^ (zdigits - log_inf p - 1) * Z.pos p < wB
 unfold wB, base, zdigits; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
2 ^ (zdigits - log_inf p - 1) * 2 ^ log_inf p <=
2 ^ (zdigits - log_inf p - 1) * Z.pos p
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
2 ^ (zdigits - log_inf p - 1) * Z.pos p < wB
 apply Z.mul_le_mono_nonneg; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
2 ^ (zdigits - log_inf p - 1) * Z.pos p < wB

 apply Z.lt_le_trans
   with (2^(zdigits - log_inf p - 1)*(2^(Z.succ (log_inf p)))).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
2 ^ (zdigits - log_inf p - 1) * Z.pos p <
2 ^ (zdigits - log_inf p - 1) * 2 ^ Z.succ (log_inf p)
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
2 ^ (zdigits - log_inf p - 1) * 2 ^ Z.succ (log_inf p) <=
wB
 apply Z.mul_lt_mono_pos_l; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
2 ^ (zdigits - log_inf p - 1) * 2 ^ Z.succ (log_inf p) <=
wB
 rewrite <- Zpower_exp; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
2 ^ (zdigits - log_inf p - 1 + Z.succ (log_inf p)) <=
wB
 replace (zdigits - log_inf p -1 +Z.succ (log_inf p)) with zdigits
   by ring.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:0 <= log_inf p
H2:2 ^ log_inf p <= Z.pos p
H4:Z.pos p < 2 ^ Z.succ (log_inf p)
H3:0 <= zdigits - log_inf p - 1 < wB
2 ^ zdigits <= wB
 unfold wB, base, zdigits; auto with zarith.
 Qed.

 Fixpoint Ptail p := match p with
  | xO p => (Ptail p)+1
  | _ => 0
 end.

 Lemma Ptail_pos : forall p, 0 <= Ptail p.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall p : positive, 0 <= Ptail p
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall p : positive, 0 <= Ptail p
 induction p; simpl; auto with zarith.
 Qed.
 Hint Resolve Ptail_pos : core.

 Lemma Ptail_bounded : forall p d, Zpos p < 2^(Zpos d) -> Ptail p < Zpos d.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall p d : positive,
Z.pos p < 2 ^ Z.pos d -> Ptail p < Z.pos d
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall p d : positive,
Z.pos p < 2 ^ Z.pos d -> Ptail p < Z.pos d
 induction p; try (compute; auto; fail).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d : positive,
Z.pos p < 2 ^ Z.pos d -> Ptail p < Z.pos d
forall d : positive,
Z.pos p~0 < 2 ^ Z.pos d -> Ptail p~0 < Z.pos d
 intros; simpl.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
Ptail p + 1 < Z.pos d
 assert (d <> xH).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
d <> 1%positive
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
Ptail p + 1 < Z.pos d
  intro; subst.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d : positive,
Z.pos p < 2 ^ Z.pos d -> Ptail p < Z.pos d
H:Z.pos p~0 < 2 ^ 1
False
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
Ptail p + 1 < Z.pos d
  compute in H; destruct p; discriminate.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
Ptail p + 1 < Z.pos d
 assert (Z.succ (Zpos (Pos.pred d)) = Zpos d).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
Z.succ (Z.pos (Pos.pred d)) = Z.pos d
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
H1:Z.succ (Z.pos (Pos.pred d)) = Z.pos d
Ptail p + 1 < Z.pos d
  simpl; f_equal.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
(Pos.pred d + 1)%positive = d
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
H1:Z.succ (Z.pos (Pos.pred d)) = Z.pos d
Ptail p + 1 < Z.pos d
  rewrite Pos.add_1_r.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
Pos.succ (Pos.pred d) = d
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
H1:Z.succ (Z.pos (Pos.pred d)) = Z.pos d
Ptail p + 1 < Z.pos d
  destruct (Pos.succ_pred_or d); auto.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
H1:d = 1%positive
Pos.succ (Pos.pred d) = d
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
H1:Z.succ (Z.pos (Pos.pred d)) = Z.pos d
Ptail p + 1 < Z.pos d
  rewrite H1 in H0; elim H0; auto.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
H1:Z.succ (Z.pos (Pos.pred d)) = Z.pos d
Ptail p + 1 < Z.pos d
 assert (Ptail p < Zpos (Pos.pred d)).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
H1:Z.succ (Z.pos (Pos.pred d)) = Z.pos d
Ptail p < Z.pos (Pos.pred d)
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
H1:Z.succ (Z.pos (Pos.pred d)) = Z.pos d
H2:Ptail p < Z.pos (Pos.pred d)
Ptail p + 1 < Z.pos d
  apply IHp.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
H1:Z.succ (Z.pos (Pos.pred d)) = Z.pos d
Z.pos p < 2 ^ Z.pos (Pos.pred d)
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
H1:Z.succ (Z.pos (Pos.pred d)) = Z.pos d
H2:Ptail p < Z.pos (Pos.pred d)
Ptail p + 1 < Z.pos d
  apply Z.mul_lt_mono_pos_r with 2; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
H1:Z.succ (Z.pos (Pos.pred d)) = Z.pos d
Z.pos p * 2 < 2 ^ Z.pos (Pos.pred d) * 2
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
H1:Z.succ (Z.pos (Pos.pred d)) = Z.pos d
H2:Ptail p < Z.pos (Pos.pred d)
Ptail p + 1 < Z.pos d
  rewrite (Z.mul_comm (Zpos p)).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
H1:Z.succ (Z.pos (Pos.pred d)) = Z.pos d
2 * Z.pos p < 2 ^ Z.pos (Pos.pred d) * 2
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
H1:Z.succ (Z.pos (Pos.pred d)) = Z.pos d
H2:Ptail p < Z.pos (Pos.pred d)
Ptail p + 1 < Z.pos d
  change (2 * Zpos p) with (Zpos p~0).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
H1:Z.succ (Z.pos (Pos.pred d)) = Z.pos d
Z.pos p~0 < 2 ^ Z.pos (Pos.pred d) * 2
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
H1:Z.succ (Z.pos (Pos.pred d)) = Z.pos d
H2:Ptail p < Z.pos (Pos.pred d)
Ptail p + 1 < Z.pos d
  rewrite Z.mul_comm.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
H1:Z.succ (Z.pos (Pos.pred d)) = Z.pos d
Z.pos p~0 < 2 * 2 ^ Z.pos (Pos.pred d)
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
H1:Z.succ (Z.pos (Pos.pred d)) = Z.pos d
H2:Ptail p < Z.pos (Pos.pred d)
Ptail p + 1 < Z.pos d
  rewrite <- Z.pow_succ_r; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
H1:Z.succ (Z.pos (Pos.pred d)) = Z.pos d
Z.pos p~0 < 2 ^ Z.succ (Z.pos (Pos.pred d))
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
H1:Z.succ (Z.pos (Pos.pred d)) = Z.pos d
H2:Ptail p < Z.pos (Pos.pred d)
Ptail p + 1 < Z.pos d
  rewrite H1; auto.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
p:positive
IHp:forall d0 : positive,
Z.pos p < 2 ^ Z.pos d0 -> Ptail p < Z.pos d0
d:positive
H:Z.pos p~0 < 2 ^ Z.pos d
H0:d <> 1%positive
H1:Z.succ (Z.pos (Pos.pred d)) = Z.pos d
H2:Ptail p < Z.pos (Pos.pred d)
Ptail p + 1 < Z.pos d
 rewrite <- H1; omega.
 Qed.

 Definition tail0 x :=
  match [|x|] with
   | Z0 => zdigits
   | Zpos p => Ptail p
   | Zneg _ => 0
  end.

 Lemma spec_tail00:  forall x, [|x|] = 0 -> [|tail0 x|] = Zpos digits.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, [|x|] = 0 -> [|tail0 x|] = Z.pos digits
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z, [|x|] = 0 -> [|tail0 x|] = Z.pos digits
  unfold tail0; intros.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:[|x|] = 0
[|match [|x|] with
  | 0 => zdigits
  | Z.pos p => Ptail p
  | Z.neg _ => 0
  end|] = Z.pos digits
  rewrite H; simpl.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:[|x|] = 0
[|zdigits|] = Z.pos digits
  apply spec_zdigits.
 Qed.

 Lemma spec_tail0  : forall x, 0 < [|x|] ->
         exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|tail0 x|]).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z,
0 < [|x|] ->
exists y : Z,
  0 <= y /\ [|x|] = (2 * y + 1) * 2 ^ [|tail0 x|]
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
forall x : Z,
0 < [|x|] ->
exists y : Z,
  0 <= y /\ [|x|] = (2 * y + 1) * 2 ^ [|tail0 x|]
 intros; unfold tail0.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:0 < [|x|]
exists y : Z,
  0 <= y /\
  [|x|] =
  (2 * y + 1) *
  2
  ^ [|match [|x|] with
      | 0 => zdigits
      | Z.pos p => Ptail p
      | Z.neg _ => 0
      end|]
 generalize (spec_to_Z x).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
H:0 < [|x|]
0 <= [|x|] < wB ->
exists y : Z,
  0 <= y /\
  [|x|] =
  (2 * y + 1) *
  2
  ^ [|match [|x|] with
      | 0 => zdigits
      | Z.pos p => Ptail p
      | Z.neg _ => 0
      end|]
 destruct [|x|]; try discriminate; intros.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
exists y : Z,
  0 <= y /\ Z.pos p = (2 * y + 1) * 2 ^ [|Ptail p|]
 assert ([|Ptail p|] = Ptail p).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
[|Ptail p|] = Ptail p
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:[|Ptail p|] = Ptail p
exists y : Z,
  0 <= y /\ Z.pos p = (2 * y + 1) * 2 ^ [|Ptail p|]
  apply Zmod_small.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
0 <= Ptail p < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:[|Ptail p|] = Ptail p
exists y : Z,
  0 <= y /\ Z.pos p = (2 * y + 1) * 2 ^ [|Ptail p|]
  split; auto.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
Ptail p < wB
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:[|Ptail p|] = Ptail p
exists y : Z,
  0 <= y /\ Z.pos p = (2 * y + 1) * 2 ^ [|Ptail p|]
  unfold wB, base in *.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < 2 ^ Z.pos digits
Ptail p < 2 ^ Z.pos digits
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:[|Ptail p|] = Ptail p
exists y : Z,
  0 <= y /\ Z.pos p = (2 * y + 1) * 2 ^ [|Ptail p|]
  apply Z.lt_trans with (Zpos digits).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < 2 ^ Z.pos digits
Ptail p < Z.pos digits
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < 2 ^ Z.pos digits
Z.pos digits < 2 ^ Z.pos digits
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:[|Ptail p|] = Ptail p
exists y : Z,
  0 <= y /\ Z.pos p = (2 * y + 1) * 2 ^ [|Ptail p|]
  apply Ptail_bounded; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < 2 ^ Z.pos digits
Z.pos digits < 2 ^ Z.pos digits
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:[|Ptail p|] = Ptail p
exists y : Z,
  0 <= y /\ Z.pos p = (2 * y + 1) * 2 ^ [|Ptail p|]
  apply Zpower2_lt_lin; auto with zarith.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:[|Ptail p|] = Ptail p
exists y : Z,
  0 <= y /\ Z.pos p = (2 * y + 1) * 2 ^ [|Ptail p|]
 rewrite H1.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x:Z
p:positive
H:0 < Z.pos p
H0:0 <= Z.pos p < wB
H1:[|Ptail p|] = Ptail p
exists y : Z,
  0 <= y /\ Z.pos p = (2 * y + 1) * 2 ^ Ptail p

 clear; induction p.p:positive
IHp:exists y : Z, 0 <= y /\ Z.pos p = (2 * y + 1) * 2 ^ Ptail p
exists y : Z,
  0 <= y /\ Z.pos p~1 = (2 * y + 1) * 2 ^ Ptail p~1
p:positive
IHp:exists y : Z, 0 <= y /\ Z.pos p = (2 * y + 1) * 2 ^ Ptail p
exists y : Z,
  0 <= y /\ Z.pos p~0 = (2 * y + 1) * 2 ^ Ptail p~0
exists y : Z, 0 <= y /\ 1 = (2 * y + 1) * 2 ^ Ptail 1
 exists (Zpos p); simpl; rewrite Pos.mul_1_r; auto with zarith.p:positive
IHp:exists y : Z, 0 <= y /\ Z.pos p = (2 * y + 1) * 2 ^ Ptail p
exists y : Z,
  0 <= y /\ Z.pos p~0 = (2 * y + 1) * 2 ^ Ptail p~0
exists y : Z, 0 <= y /\ 1 = (2 * y + 1) * 2 ^ Ptail 1
 destruct IHp as (y & Yp & Ye).p:positive
y:Z
Yp:0 <= y
Ye:Z.pos p = (2 * y + 1) * 2 ^ Ptail p
exists y0 : Z,
  0 <= y0 /\ Z.pos p~0 = (2 * y0 + 1) * 2 ^ Ptail p~0
exists y : Z, 0 <= y /\ 1 = (2 * y + 1) * 2 ^ Ptail 1
 exists y.p:positive
y:Z
Yp:0 <= y
Ye:Z.pos p = (2 * y + 1) * 2 ^ Ptail p
0 <= y /\ Z.pos p~0 = (2 * y + 1) * 2 ^ Ptail p~0
exists y : Z, 0 <= y /\ 1 = (2 * y + 1) * 2 ^ Ptail 1
 split; auto.p:positive
y:Z
Yp:0 <= y
Ye:Z.pos p = (2 * y + 1) * 2 ^ Ptail p
Z.pos p~0 = (2 * y + 1) * 2 ^ Ptail p~0
exists y : Z, 0 <= y /\ 1 = (2 * y + 1) * 2 ^ Ptail 1
 change (Zpos p~0) with (2*Zpos p).p:positive
y:Z
Yp:0 <= y
Ye:Z.pos p = (2 * y + 1) * 2 ^ Ptail p
2 * Z.pos p = (2 * y + 1) * 2 ^ Ptail p~0
exists y : Z, 0 <= y /\ 1 = (2 * y + 1) * 2 ^ Ptail 1
 rewrite Ye.p:positive
y:Z
Yp:0 <= y
Ye:Z.pos p = (2 * y + 1) * 2 ^ Ptail p
2 * ((2 * y + 1) * 2 ^ Ptail p) =
(2 * y + 1) * 2 ^ Ptail p~0
exists y : Z, 0 <= y /\ 1 = (2 * y + 1) * 2 ^ Ptail 1
 change (Ptail p~0) with (Z.succ (Ptail p)).p:positive
y:Z
Yp:0 <= y
Ye:Z.pos p = (2 * y + 1) * 2 ^ Ptail p
2 * ((2 * y + 1) * 2 ^ Ptail p) =
(2 * y + 1) * 2 ^ Z.succ (Ptail p)
exists y : Z, 0 <= y /\ 1 = (2 * y + 1) * 2 ^ Ptail 1
 rewrite Z.pow_succ_r; auto; ring.exists y : Z, 0 <= y /\ 1 = (2 * y + 1) * 2 ^ Ptail 1

 exists 0; simpl; auto with zarith.
 Qed.

 Definition lor := Z.lor.
 Definition land := Z.land.
 Definition lxor := Z.lxor.

 Lemma spec_lor x y : [|lor x y|] = Z.lor [|x|] [|y|].digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
[|lor x y|] = Z.lor [|x|] [|y|]
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
[|lor x y|] = Z.lor [|x|] [|y|]
 unfold lor, to_Z.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
Z.lor x y mod wB = Z.lor (x mod wB) (y mod wB)
 apply Z.bits_inj'; intros n Hn.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, n:Z
Hn:0 <= n
Z.testbit (Z.lor x y mod wB) n =
Z.testbit (Z.lor (x mod wB) (y mod wB)) n rewrite Z.lor_spec.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, n:Z
Hn:0 <= n
Z.testbit (Z.lor x y mod wB) n =
Z.testbit (x mod wB) n || Z.testbit (y mod wB) n
 unfold wB, base.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, n:Z
Hn:0 <= n
Z.testbit (Z.lor x y mod 2 ^ Z.pos digits) n =
Z.testbit (x mod 2 ^ Z.pos digits) n
|| Z.testbit (y mod 2 ^ Z.pos digits) n
 destruct (Z.le_gt_cases (Z.pos digits) n).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, n:Z
Hn:0 <= n
H:Z.pos digits <= n
Z.testbit (Z.lor x y mod 2 ^ Z.pos digits) n =
Z.testbit (x mod 2 ^ Z.pos digits) n
|| Z.testbit (y mod 2 ^ Z.pos digits) n
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, n:Z
Hn:0 <= n
H:n < Z.pos digits
Z.testbit (Z.lor x y mod 2 ^ Z.pos digits) n =
Z.testbit (x mod 2 ^ Z.pos digits) n
|| Z.testbit (y mod 2 ^ Z.pos digits) n
 -digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, n:Z
Hn:0 <= n
H:Z.pos digits <= n
Z.testbit (Z.lor x y mod 2 ^ Z.pos digits) n =
Z.testbit (x mod 2 ^ Z.pos digits) n
|| Z.testbit (y mod 2 ^ Z.pos digits) n rewrite !Z.mod_pow2_bits_high; auto with zarith.
 -digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, n:Z
Hn:0 <= n
H:n < Z.pos digits
Z.testbit (Z.lor x y mod 2 ^ Z.pos digits) n =
Z.testbit (x mod 2 ^ Z.pos digits) n
|| Z.testbit (y mod 2 ^ Z.pos digits) n rewrite !Z.mod_pow2_bits_low, Z.lor_spec; auto with zarith.
 Qed.

 Lemma spec_land x y : [|land x y|] = Z.land [|x|] [|y|].digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
[|land x y|] = Z.land [|x|] [|y|]
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
[|land x y|] = Z.land [|x|] [|y|]
 unfold land, to_Z.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
Z.land x y mod wB = Z.land (x mod wB) (y mod wB)
 apply Z.bits_inj'; intros n Hn.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, n:Z
Hn:0 <= n
Z.testbit (Z.land x y mod wB) n =
Z.testbit (Z.land (x mod wB) (y mod wB)) n rewrite Z.land_spec.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, n:Z
Hn:0 <= n
Z.testbit (Z.land x y mod wB) n =
Z.testbit (x mod wB) n && Z.testbit (y mod wB) n
 unfold wB, base.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, n:Z
Hn:0 <= n
Z.testbit (Z.land x y mod 2 ^ Z.pos digits) n =
Z.testbit (x mod 2 ^ Z.pos digits) n &&
Z.testbit (y mod 2 ^ Z.pos digits) n
 destruct (Z.le_gt_cases (Z.pos digits) n).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, n:Z
Hn:0 <= n
H:Z.pos digits <= n
Z.testbit (Z.land x y mod 2 ^ Z.pos digits) n =
Z.testbit (x mod 2 ^ Z.pos digits) n &&
Z.testbit (y mod 2 ^ Z.pos digits) n
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, n:Z
Hn:0 <= n
H:n < Z.pos digits
Z.testbit (Z.land x y mod 2 ^ Z.pos digits) n =
Z.testbit (x mod 2 ^ Z.pos digits) n &&
Z.testbit (y mod 2 ^ Z.pos digits) n
 -digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, n:Z
Hn:0 <= n
H:Z.pos digits <= n
Z.testbit (Z.land x y mod 2 ^ Z.pos digits) n =
Z.testbit (x mod 2 ^ Z.pos digits) n &&
Z.testbit (y mod 2 ^ Z.pos digits) n rewrite !Z.mod_pow2_bits_high; auto with zarith.
 -digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, n:Z
Hn:0 <= n
H:n < Z.pos digits
Z.testbit (Z.land x y mod 2 ^ Z.pos digits) n =
Z.testbit (x mod 2 ^ Z.pos digits) n &&
Z.testbit (y mod 2 ^ Z.pos digits) n rewrite !Z.mod_pow2_bits_low, Z.land_spec; auto with zarith.
 Qed.

 Lemma spec_lxor x y : [|lxor x y|] = Z.lxor [|x|] [|y|].digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
[|lxor x y|] = Z.lxor [|x|] [|y|]
 Proof.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
[|lxor x y|] = Z.lxor [|x|] [|y|]
 unfold lxor, to_Z.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y:Z
Z.lxor x y mod wB = Z.lxor (x mod wB) (y mod wB)
 apply Z.bits_inj'; intros n Hn.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, n:Z
Hn:0 <= n
Z.testbit (Z.lxor x y mod wB) n =
Z.testbit (Z.lxor (x mod wB) (y mod wB)) n rewrite Z.lxor_spec.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, n:Z
Hn:0 <= n
Z.testbit (Z.lxor x y mod wB) n =
xorb (Z.testbit (x mod wB) n) (Z.testbit (y mod wB) n)
 unfold wB, base.digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, n:Z
Hn:0 <= n
Z.testbit (Z.lxor x y mod 2 ^ Z.pos digits) n =
xorb (Z.testbit (x mod 2 ^ Z.pos digits) n)
  (Z.testbit (y mod 2 ^ Z.pos digits) n)
 destruct (Z.le_gt_cases (Z.pos digits) n).digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, n:Z
Hn:0 <= n
H:Z.pos digits <= n
Z.testbit (Z.lxor x y mod 2 ^ Z.pos digits) n =
xorb (Z.testbit (x mod 2 ^ Z.pos digits) n)
  (Z.testbit (y mod 2 ^ Z.pos digits) n)
digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, n:Z
Hn:0 <= n
H:n < Z.pos digits
Z.testbit (Z.lxor x y mod 2 ^ Z.pos digits) n =
xorb (Z.testbit (x mod 2 ^ Z.pos digits) n)
  (Z.testbit (y mod 2 ^ Z.pos digits) n)
 -digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, n:Z
Hn:0 <= n
H:Z.pos digits <= n
Z.testbit (Z.lxor x y mod 2 ^ Z.pos digits) n =
xorb (Z.testbit (x mod 2 ^ Z.pos digits) n)
  (Z.testbit (y mod 2 ^ Z.pos digits) n) rewrite !Z.mod_pow2_bits_high; auto with zarith.
 -digits:positive
digits_ne_1:digits <> 1%positive
digits_gt_1:=spec_more_than_1_digit:1 < Z.pos digits
x, y, n:Z
Hn:0 <= n
H:n < Z.pos digits
Z.testbit (Z.lxor x y mod 2 ^ Z.pos digits) n =
xorb (Z.testbit (x mod 2 ^ Z.pos digits) n)
  (Z.testbit (y mod 2 ^ Z.pos digits) n) rewrite !Z.mod_pow2_bits_low, Z.lxor_spec; auto with zarith.
 Qed.

Let's now group everything in two records

 Instance zmod_ops : ZnZ.Ops Z := ZnZ.MkOps
    (digits : positive)
    (zdigits: t)
    (to_Z   : t -> Z)
    (of_pos : positive -> N * t)
    (head0  : t -> t)
    (tail0  : t -> t)

    (zero   : t)
    (one    : t)
    (minus_one : t)

    (compare     : t -> t -> comparison)
    (eq0         : t -> bool)

    (opp_c       : t -> carry t)
    (opp         : t -> t)
    (opp_carry   : t -> t)

    (succ_c      : t -> carry t)
    (add_c       : t -> t -> carry t)
    (add_carry_c : t -> t -> carry t)
    (succ        : t -> t)
    (add         : t -> t -> t)
    (add_carry   : t -> t -> t)

    (pred_c      : t -> carry t)
    (sub_c       : t -> t -> carry t)
    (sub_carry_c : t -> t -> carry t)
    (pred        : t -> t)
    (sub         : t -> t -> t)
    (sub_carry   : t -> t -> t)

    (mul_c       : t -> t -> zn2z t)
    (mul         : t -> t -> t)
    (square_c    : t -> zn2z t)

    (div21       : t -> t -> t -> t*t)
    (div_gt      : t -> t -> t * t)
    (div         : t -> t -> t * t)

    (modulo_gt      : t -> t -> t)
    (modulo         : t -> t -> t)

    (gcd_gt      : t -> t -> t)
    (gcd         : t -> t -> t)
    (add_mul_div : t -> t -> t -> t)
    (pos_mod     : t -> t -> t)

    (is_even     : t -> bool)
    (sqrt2       : t -> t -> t * carry t)
    (sqrt        : t -> t)
    (lor         : t -> t -> t)
    (land         : t -> t -> t)
    (lxor         : t -> t -> t).

 Instance zmod_specs : ZnZ.Specs zmod_ops := ZnZ.MkSpecs
    spec_to_Z
    spec_of_pos
    spec_zdigits
    spec_more_than_1_digit

    spec_0
    spec_1
    spec_Bm1

    spec_compare
    spec_eq0

    spec_opp_c
    spec_opp
    spec_opp_carry

    spec_succ_c
    spec_add_c
    spec_add_carry_c
    spec_succ
    spec_add
    spec_add_carry

    spec_pred_c
    spec_sub_c
    spec_sub_carry_c
    spec_pred
    spec_sub
    spec_sub_carry

    spec_mul_c
    spec_mul
    spec_square_c

    spec_div21
    spec_div_gt
    spec_div

    spec_modulo_gt
    spec_modulo

    spec_gcd_gt
    spec_gcd

    spec_head00
    spec_head0
    spec_tail00
    spec_tail0

    spec_add_mul_div
    spec_pos_mod

    spec_is_even
    spec_sqrt2
    spec_sqrt
    spec_lor
    spec_land
    spec_lxor.

End ZModulo.

A modular version of the previous construction.

Module Type PositiveNotOne.
 Parameter p : positive.
 Axiom not_one : p <> 1%positive.
End PositiveNotOne.

Module ZModuloCyclicType (P:PositiveNotOne) <: CyclicType.
 Definition t := Z.
 Instance ops : ZnZ.Ops t := zmod_ops P.p.
 Instance specs : ZnZ.Specs ops := zmod_specs P.not_one.
End ZModuloCyclicType.