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.

(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2018     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

Int63 numbers defines indeed a cyclic structure : Z/(2^31)Z

Author: Arnaud Spiwack (+ Pierre Letouzey)

Require Import CyclicAxioms.
Require Export ZArith.
Require Export Int63.
Import Zpow_facts.
Import Utf8.
Import Lia.

Local Open Scope int63_scope.

{2 Operators }

Definition Pdigits := Eval compute in P_of_succ_nat (size - 1).

Fixpoint positive_to_int_rec (n:nat) (p:positive) :=
  match n, p with
  | O, _ => (Npos p, 0)
  | S n, xH => (0%N, 1)
  | S n, xO p =>
    let (N,i) := positive_to_int_rec n p in
    (N, i << 1)
  | S n, xI p =>
    let (N,i) := positive_to_int_rec n p in
    (N, (i << 1) + 1)
  end.

Definition positive_to_int := positive_to_int_rec size.

Definition mulc_WW x y :=
  let (h, l) := mulc x y in
  if is_zero h then
    if is_zero l then W0
    else WW h l
  else WW h l.
Notation "n '*c' m" := (mulc_WW n m) (at level 40, no associativity) : int63_scope.

Definition pos_mod p x :=
  if p <= digits then
    let p := digits - p in
    (x << p) >> p
  else x.

Notation pos_mod_int := pos_mod.

Import ZnZ.

Instance int_ops : ZnZ.Ops int :=
{|
 digits      := Pdigits; (* number of digits *)
 zdigits     := Int63.digits; (* number of digits *)
 to_Z        := Int63.to_Z; (* conversion to Z *)
 of_pos      := positive_to_int; (* positive -> N*int63 :  p => N,i
                                      where p = N*2^31+phi i *)
 head0       := Int63.head0;  (* number of head 0 *)
 tail0       := Int63.tail0;  (* number of tail 0 *)
 zero        := 0;
 one         := 1;
 minus_one   := Int63.max_int;
 compare     := Int63.compare;
 eq0         := Int63.is_zero;
 opp_c       := Int63.oppc;
 opp         := Int63.opp;
 opp_carry   := Int63.oppcarry;
 succ_c      := Int63.succc;
 add_c       := Int63.addc;
 add_carry_c := Int63.addcarryc;
 succ        := Int63.succ;
 add         := Int63.add;
 add_carry   := Int63.addcarry;
 pred_c      := Int63.predc;
 sub_c       := Int63.subc;
 sub_carry_c := Int63.subcarryc;
 pred        := Int63.pred;
 sub         := Int63.sub;
 sub_carry   := Int63.subcarry;
 mul_c       := mulc_WW;
 mul         := Int63.mul;
 square_c    := fun x => mulc_WW x x;
 div21       := diveucl_21;
 div_gt      := diveucl; (* this is supposed to be the special case of
                         division a/b where a > b *)
 div         := diveucl;
 modulo_gt   := Int63.mod;
 modulo      := Int63.mod;
 gcd_gt      := Int63.gcd;
 gcd         := Int63.gcd;
 add_mul_div := Int63.addmuldiv;
 pos_mod     := pos_mod_int;
 is_even     := Int63.is_even;
 sqrt2       := Int63.sqrt2;
 sqrt        := Int63.sqrt;
 ZnZ.lor     := Int63.lor;
 ZnZ.land    := Int63.land;
 ZnZ.lxor    := Int63.lxor
|}.

Local Open Scope Z_scope.

Lemma is_zero_spec_aux : forall x : int, is_zero x = true -> [|x|] = 0%Z.∀ x : int, is_zero x = true → φ (x) = 0
Proof.∀ x : int, is_zero x = true → φ (x) = 0
 intros x;rewrite is_zero_spec;intros H;rewrite H;trivial.
Qed.

Lemma positive_to_int_spec :
  forall p : positive,
    Zpos p =
      Z_of_N (fst (positive_to_int p)) * wB + to_Z (snd (positive_to_int p)).∀ p : positive,
  Z.pos p =
  Z.of_N (fst (positive_to_int p)) * wB +
  to_Z (snd (positive_to_int p))
Proof.∀ p : positive,
  Z.pos p =
  Z.of_N (fst (positive_to_int p)) * wB +
  to_Z (snd (positive_to_int p))
 assert (H: (wB <= wB) -> forall p : positive,
  Zpos p = Z_of_N (fst (positive_to_int p)) * wB + [|snd (positive_to_int p)|] /\
  [|snd (positive_to_int p)|] < wB).wB <= wB
→ ∀ p : positive,
    Z.pos p =
    Z.of_N (fst (positive_to_int p)) * wB +
    φ (snd (positive_to_int p))
    ∧ φ (snd (positive_to_int p)) < wB
H:wB <= wB
→ ∀ p : positive,
    Z.pos p =
    Z.of_N (fst (positive_to_int p)) * wB +
    φ (snd (positive_to_int p))
    ∧ φ (snd (positive_to_int p)) < wB
∀ p : positive,
  Z.pos p =
  Z.of_N (fst (positive_to_int p)) * wB +
  to_Z (snd (positive_to_int p))
  2: intros p; case (H (Z.le_refl wB) p); auto.wB <= wB
→ ∀ p : positive,
    Z.pos p =
    Z.of_N (fst (positive_to_int p)) * wB +
    φ (snd (positive_to_int p))
    ∧ φ (snd (positive_to_int p)) < wB
 unfold positive_to_int, wB at 1 3 4.2 ^ Z.of_nat size <= wB
→ ∀ p : positive,
    Z.pos p =
    Z.of_N (fst (positive_to_int_rec size p)) *
    2 ^ Z.of_nat size +
    φ (snd (positive_to_int_rec size p))
    ∧ φ (snd (positive_to_int_rec size p)) <
      2 ^ Z.of_nat size
 elim size.2 ^ Z.of_nat 0 <= wB
→ ∀ p : positive,
    Z.pos p =
    Z.of_N (fst (positive_to_int_rec 0 p)) *
    2 ^ Z.of_nat 0 + φ (snd (positive_to_int_rec 0 p))
    ∧ φ (snd (positive_to_int_rec 0 p)) <
      2 ^ Z.of_nat 0
∀ n : nat,
  (2 ^ Z.of_nat n <= wB
   → ∀ p : positive,
       Z.pos p =
       Z.of_N (fst (positive_to_int_rec n p)) *
       2 ^ Z.of_nat n +
       φ (snd (positive_to_int_rec n p))
       ∧ φ (snd (positive_to_int_rec n p)) <
         2 ^ Z.of_nat n)
  → 2 ^ Z.of_nat (S n) <= wB
    → ∀ p : positive,
        Z.pos p =
        Z.of_N (fst (positive_to_int_rec (S n) p)) *
        2 ^ Z.of_nat (S n) +
        φ (snd (positive_to_int_rec (S n) p))
        ∧ φ (snd (positive_to_int_rec (S n) p)) <
          2 ^ Z.of_nat (S n)
 intros _ p; simpl;
   rewrite to_Z_0, Pmult_1_r; split; auto with zarith; apply refl_equal.∀ n : nat,
  (2 ^ Z.of_nat n <= wB
   → ∀ p : positive,
       Z.pos p =
       Z.of_N (fst (positive_to_int_rec n p)) *
       2 ^ Z.of_nat n +
       φ (snd (positive_to_int_rec n p))
       ∧ φ (snd (positive_to_int_rec n p)) <
         2 ^ Z.of_nat n)
  → 2 ^ Z.of_nat (S n) <= wB
    → ∀ p : positive,
        Z.pos p =
        Z.of_N (fst (positive_to_int_rec (S n) p)) *
        2 ^ Z.of_nat (S n) +
        φ (snd (positive_to_int_rec (S n) p))
        ∧ φ (snd (positive_to_int_rec (S n) p)) <
          2 ^ Z.of_nat (S n)
 intros n; rewrite inj_S; unfold Z.succ; rewrite Zpower_exp, Z.pow_1_r; auto with zarith.n:nat
(2 ^ Z.of_nat n <= wB
 → ∀ p : positive,
     Z.pos p =
     Z.of_N (fst (positive_to_int_rec n p)) *
     2 ^ Z.of_nat n +
     φ (snd (positive_to_int_rec n p))
     ∧ φ (snd (positive_to_int_rec n p)) <
       2 ^ Z.of_nat n)
→ 2 ^ Z.of_nat n * 2 <= wB
  → ∀ p : positive,
      Z.pos p =
      Z.of_N (fst (positive_to_int_rec (S n) p)) *
      (2 ^ Z.of_nat n * 2) +
      φ (snd (positive_to_int_rec (S n) p))
      ∧ φ (snd (positive_to_int_rec (S n) p)) <
        2 ^ Z.of_nat n * 2
 intros IH Hle p.n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
Z.pos p =
Z.of_N (fst (positive_to_int_rec (S n) p)) *
(2 ^ Z.of_nat n * 2) +
φ (snd (positive_to_int_rec (S n) p))
∧ φ (snd (positive_to_int_rec (S n) p)) <
  2 ^ Z.of_nat n * 2
 assert (F1: 2 ^ Z_of_nat n <= wB); auto with zarith.n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
2 ^ Z.of_nat n <= wB
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
Z.pos p =
Z.of_N (fst (positive_to_int_rec (S n) p)) *
(2 ^ Z.of_nat n * 2) +
φ (snd (positive_to_int_rec (S n) p))
∧ φ (snd (positive_to_int_rec (S n) p)) <
  2 ^ Z.of_nat n * 2
  assert (0 <= 2 ^ Z_of_nat n); auto with zarith.n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
Z.pos p =
Z.of_N (fst (positive_to_int_rec (S n) p)) *
(2 ^ Z.of_nat n * 2) +
φ (snd (positive_to_int_rec (S n) p))
∧ φ (snd (positive_to_int_rec (S n) p)) <
  2 ^ Z.of_nat n * 2
 case p; simpl.n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
∀ p0 : positive,
  Z.pos p0~1 =
  Z.of_N
    (fst
       (let (N, i) := positive_to_int_rec n p0 in
        (N, (i << 1 + 1)%int63))) *
  (2 ^ Z.of_nat n * 2) +
  φ (snd
       (let (N, i) := positive_to_int_rec n p0 in
        (N, (i << 1 + 1)%int63)))
  ∧ φ (snd
         (let (N, i) := positive_to_int_rec n p0 in
          (N, (i << 1 + 1)%int63))) <
    2 ^ Z.of_nat n * 2
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
∀ p0 : positive,
  Z.pos p0~0 =
  Z.of_N
    (fst
       (let (N, i) := positive_to_int_rec n p0 in
        (N, i << 1))) * (2 ^ Z.of_nat n * 2) +
  φ (snd
       (let (N, i) := positive_to_int_rec n p0 in
        (N, i << 1)))
  ∧ φ (snd
         (let (N, i) := positive_to_int_rec n p0 in
          (N, i << 1))) < 2 ^ Z.of_nat n * 2
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
1 = φ (1) ∧ φ (1) < 2 ^ Z.of_nat n * 2
 intros p1.n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
p1:positive
Z.pos p1~1 =
Z.of_N
  (fst
     (let (N, i) := positive_to_int_rec n p1 in
      (N, (i << 1 + 1)%int63))) * (2 ^ Z.of_nat n * 2) +
φ (snd
     (let (N, i) := positive_to_int_rec n p1 in
      (N, (i << 1 + 1)%int63)))
∧ φ (snd
       (let (N, i) := positive_to_int_rec n p1 in
        (N, (i << 1 + 1)%int63))) < 2 ^ Z.of_nat n * 2
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
∀ p0 : positive,
  Z.pos p0~0 =
  Z.of_N
    (fst
       (let (N, i) := positive_to_int_rec n p0 in
        (N, i << 1))) * (2 ^ Z.of_nat n * 2) +
  φ (snd
       (let (N, i) := positive_to_int_rec n p0 in
        (N, i << 1)))
  ∧ φ (snd
         (let (N, i) := positive_to_int_rec n p0 in
          (N, i << 1))) < 2 ^ Z.of_nat n * 2
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
1 = φ (1) ∧ φ (1) < 2 ^ Z.of_nat n * 2
 generalize (IH F1 p1); case positive_to_int_rec; simpl.n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
p1:positive
∀ (n0 : N) (i : int),
  Z.pos p1 = Z.of_N n0 * 2 ^ Z.of_nat n + φ (i)
  ∧ φ (i) < 2 ^ Z.of_nat n
  → Z.pos p1~1 =
    Z.of_N n0 * (2 ^ Z.of_nat n * 2) + φ (i << 1 + 1)
    ∧ φ (i << 1 + 1) < 2 ^ Z.of_nat n * 2
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
∀ p0 : positive,
  Z.pos p0~0 =
  Z.of_N
    (fst
       (let (N, i) := positive_to_int_rec n p0 in
        (N, i << 1))) * (2 ^ Z.of_nat n * 2) +
  φ (snd
       (let (N, i) := positive_to_int_rec n p0 in
        (N, i << 1)))
  ∧ φ (snd
         (let (N, i) := positive_to_int_rec n p0 in
          (N, i << 1))) < 2 ^ Z.of_nat n * 2
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
1 = φ (1) ∧ φ (1) < 2 ^ Z.of_nat n * 2
 intros n1 i (H1,H2).n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
p1:positive
n1:N
i:int
H1:Z.pos p1 = Z.of_N n1 * 2 ^ Z.of_nat n + φ (i)
H2:φ (i) < 2 ^ Z.of_nat n
Z.pos p1~1 =
Z.of_N n1 * (2 ^ Z.of_nat n * 2) + φ (i << 1 + 1)
∧ φ (i << 1 + 1) < 2 ^ Z.of_nat n * 2
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
∀ p0 : positive,
  Z.pos p0~0 =
  Z.of_N
    (fst
       (let (N, i) := positive_to_int_rec n p0 in
        (N, i << 1))) * (2 ^ Z.of_nat n * 2) +
  φ (snd
       (let (N, i) := positive_to_int_rec n p0 in
        (N, i << 1)))
  ∧ φ (snd
         (let (N, i) := positive_to_int_rec n p0 in
          (N, i << 1))) < 2 ^ Z.of_nat n * 2
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
1 = φ (1) ∧ φ (1) < 2 ^ Z.of_nat n * 2
 rewrite Zpos_xI, H1.n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
p1:positive
n1:N
i:int
H1:Z.pos p1 = Z.of_N n1 * 2 ^ Z.of_nat n + φ (i)
H2:φ (i) < 2 ^ Z.of_nat n
2 * (Z.of_N n1 * 2 ^ Z.of_nat n + φ (i)) + 1 =
Z.of_N n1 * (2 ^ Z.of_nat n * 2) + φ (i << 1 + 1)
∧ φ (i << 1 + 1) < 2 ^ Z.of_nat n * 2
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
∀ p0 : positive,
  Z.pos p0~0 =
  Z.of_N
    (fst
       (let (N, i) := positive_to_int_rec n p0 in
        (N, i << 1))) * (2 ^ Z.of_nat n * 2) +
  φ (snd
       (let (N, i) := positive_to_int_rec n p0 in
        (N, i << 1)))
  ∧ φ (snd
         (let (N, i) := positive_to_int_rec n p0 in
          (N, i << 1))) < 2 ^ Z.of_nat n * 2
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
1 = φ (1) ∧ φ (1) < 2 ^ Z.of_nat n * 2
 replace [|i << 1  + 1|] with ([|i|] * 2 + 1).n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
p1:positive
n1:N
i:int
H1:Z.pos p1 = Z.of_N n1 * 2 ^ Z.of_nat n + φ (i)
H2:φ (i) < 2 ^ Z.of_nat n
2 * (Z.of_N n1 * 2 ^ Z.of_nat n + φ (i)) + 1 =
Z.of_N n1 * (2 ^ Z.of_nat n * 2) + (φ (i) * 2 + 1)
∧ φ (i) * 2 + 1 < 2 ^ Z.of_nat n * 2
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
p1:positive
n1:N
i:int
H1:Z.pos p1 = Z.of_N n1 * 2 ^ Z.of_nat n + φ (i)
H2:φ (i) < 2 ^ Z.of_nat n
φ (i) * 2 + 1 = φ (i << 1 + 1)
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
∀ p0 : positive,
  Z.pos p0~0 =
  Z.of_N
    (fst
       (let (N, i) := positive_to_int_rec n p0 in
        (N, i << 1))) * (2 ^ Z.of_nat n * 2) +
  φ (snd
       (let (N, i) := positive_to_int_rec n p0 in
        (N, i << 1)))
  ∧ φ (snd
         (let (N, i) := positive_to_int_rec n p0 in
          (N, i << 1))) < 2 ^ Z.of_nat n * 2
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
1 = φ (1) ∧ φ (1) < 2 ^ Z.of_nat n * 2
 split; auto with zarith; ring.n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
p1:positive
n1:N
i:int
H1:Z.pos p1 = Z.of_N n1 * 2 ^ Z.of_nat n + φ (i)
H2:φ (i) < 2 ^ Z.of_nat n
φ (i) * 2 + 1 = φ (i << 1 + 1)
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
∀ p0 : positive,
  Z.pos p0~0 =
  Z.of_N
    (fst
       (let (N, i) := positive_to_int_rec n p0 in
        (N, i << 1))) * (2 ^ Z.of_nat n * 2) +
  φ (snd
       (let (N, i) := positive_to_int_rec n p0 in
        (N, i << 1)))
  ∧ φ (snd
         (let (N, i) := positive_to_int_rec n p0 in
          (N, i << 1))) < 2 ^ Z.of_nat n * 2
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
1 = φ (1) ∧ φ (1) < 2 ^ Z.of_nat n * 2
 rewrite add_spec, lsl_spec, Zplus_mod_idemp_l, to_Z_1, Z.pow_1_r, Zmod_small; auto.n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
p1:positive
n1:N
i:int
H1:Z.pos p1 = Z.of_N n1 * 2 ^ Z.of_nat n + φ (i)
H2:φ (i) < 2 ^ Z.of_nat n
0 <= φ (i) * 2 + 1 ∧ φ (i) * 2 + 1 < wB
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
∀ p0 : positive,
  Z.pos p0~0 =
  Z.of_N
    (fst
       (let (N, i) := positive_to_int_rec n p0 in
        (N, i << 1))) * (2 ^ Z.of_nat n * 2) +
  φ (snd
       (let (N, i) := positive_to_int_rec n p0 in
        (N, i << 1)))
  ∧ φ (snd
         (let (N, i) := positive_to_int_rec n p0 in
          (N, i << 1))) < 2 ^ Z.of_nat n * 2
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
1 = φ (1) ∧ φ (1) < 2 ^ Z.of_nat n * 2
 case (to_Z_bounded i); split; auto with zarith.n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
∀ p0 : positive,
  Z.pos p0~0 =
  Z.of_N
    (fst
       (let (N, i) := positive_to_int_rec n p0 in
        (N, i << 1))) * (2 ^ Z.of_nat n * 2) +
  φ (snd
       (let (N, i) := positive_to_int_rec n p0 in
        (N, i << 1)))
  ∧ φ (snd
         (let (N, i) := positive_to_int_rec n p0 in
          (N, i << 1))) < 2 ^ Z.of_nat n * 2
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
1 = φ (1) ∧ φ (1) < 2 ^ Z.of_nat n * 2
 intros p1.n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
p1:positive
Z.pos p1~0 =
Z.of_N
  (fst
     (let (N, i) := positive_to_int_rec n p1 in
      (N, i << 1))) * (2 ^ Z.of_nat n * 2) +
φ (snd
     (let (N, i) := positive_to_int_rec n p1 in
      (N, i << 1)))
∧ φ (snd
       (let (N, i) := positive_to_int_rec n p1 in
        (N, i << 1))) < 2 ^ Z.of_nat n * 2
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
1 = φ (1) ∧ φ (1) < 2 ^ Z.of_nat n * 2
 generalize (IH F1 p1); case positive_to_int_rec; simpl.n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
p1:positive
∀ (n0 : N) (i : int),
  Z.pos p1 = Z.of_N n0 * 2 ^ Z.of_nat n + φ (i)
  ∧ φ (i) < 2 ^ Z.of_nat n
  → Z.pos p1~0 =
    Z.of_N n0 * (2 ^ Z.of_nat n * 2) + φ (i << 1)
    ∧ φ (i << 1) < 2 ^ Z.of_nat n * 2
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
1 = φ (1) ∧ φ (1) < 2 ^ Z.of_nat n * 2
 intros n1 i (H1,H2).n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
p1:positive
n1:N
i:int
H1:Z.pos p1 = Z.of_N n1 * 2 ^ Z.of_nat n + φ (i)
H2:φ (i) < 2 ^ Z.of_nat n
Z.pos p1~0 =
Z.of_N n1 * (2 ^ Z.of_nat n * 2) + φ (i << 1)
∧ φ (i << 1) < 2 ^ Z.of_nat n * 2
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
1 = φ (1) ∧ φ (1) < 2 ^ Z.of_nat n * 2
 rewrite Zpos_xO, H1.n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
p1:positive
n1:N
i:int
H1:Z.pos p1 = Z.of_N n1 * 2 ^ Z.of_nat n + φ (i)
H2:φ (i) < 2 ^ Z.of_nat n
2 * (Z.of_N n1 * 2 ^ Z.of_nat n + φ (i)) =
Z.of_N n1 * (2 ^ Z.of_nat n * 2) + φ (i << 1)
∧ φ (i << 1) < 2 ^ Z.of_nat n * 2
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
1 = φ (1) ∧ φ (1) < 2 ^ Z.of_nat n * 2
 replace [|i << 1|] with ([|i|] * 2).n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
p1:positive
n1:N
i:int
H1:Z.pos p1 = Z.of_N n1 * 2 ^ Z.of_nat n + φ (i)
H2:φ (i) < 2 ^ Z.of_nat n
2 * (Z.of_N n1 * 2 ^ Z.of_nat n + φ (i)) =
Z.of_N n1 * (2 ^ Z.of_nat n * 2) + φ (i) * 2
∧ φ (i) * 2 < 2 ^ Z.of_nat n * 2
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
p1:positive
n1:N
i:int
H1:Z.pos p1 = Z.of_N n1 * 2 ^ Z.of_nat n + φ (i)
H2:φ (i) < 2 ^ Z.of_nat n
φ (i) * 2 = φ (i << 1)
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
1 = φ (1) ∧ φ (1) < 2 ^ Z.of_nat n * 2
 split; auto with zarith; ring.n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
p1:positive
n1:N
i:int
H1:Z.pos p1 = Z.of_N n1 * 2 ^ Z.of_nat n + φ (i)
H2:φ (i) < 2 ^ Z.of_nat n
φ (i) * 2 = φ (i << 1)
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
1 = φ (1) ∧ φ (1) < 2 ^ Z.of_nat n * 2
 rewrite lsl_spec, to_Z_1, Z.pow_1_r, Zmod_small; auto.n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
p1:positive
n1:N
i:int
H1:Z.pos p1 = Z.of_N n1 * 2 ^ Z.of_nat n + φ (i)
H2:φ (i) < 2 ^ Z.of_nat n
0 <= φ (i) * 2 ∧ φ (i) * 2 < wB
n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
1 = φ (1) ∧ φ (1) < 2 ^ Z.of_nat n * 2
 case (to_Z_bounded i); split; auto with zarith.n:nat
IH:2 ^ Z.of_nat n <= wB
→ ∀ p0 : positive,
    Z.pos p0 =
    Z.of_N (fst (positive_to_int_rec n p0)) *
    2 ^ Z.of_nat n +
    φ (snd (positive_to_int_rec n p0))
    ∧ φ (snd (positive_to_int_rec n p0)) <
      2 ^ Z.of_nat n
Hle:2 ^ Z.of_nat n * 2 <= wB
p:positive
F1:2 ^ Z.of_nat n <= wB
1 = φ (1) ∧ φ (1) < 2 ^ Z.of_nat n * 2
 rewrite to_Z_1; assert (0 < 2^ Z_of_nat n); auto with zarith.
Qed.

Lemma mulc_WW_spec :
   forall x y,[|| x *c y ||] = [|x|] * [|y|].∀ x y : int, [||x *c y||] = φ (x) * φ (y)
Proof.∀ x y : int, [||x *c y||] = φ (x) * φ (y)
 intros x y;unfold mulc_WW.x, y:int
[||(let (h, l) := mulc x y in
    if is_zero h
    then if is_zero l then W0 else DoubleType.WW h l
    else DoubleType.WW h l)||] = φ (x) * φ (y)
 generalize (mulc_spec x y);destruct (mulc x y);simpl;intros Heq;rewrite Heq.x, y, i, i0:int
Heq:φ (x) * φ (y) = φ (i) * wB + φ (i0)
[||(if is_zero i
    then if is_zero i0 then W0 else DoubleType.WW i i0
    else DoubleType.WW i i0)||] = φ (i) * wB + φ (i0)
 case_eq (is_zero i);intros;trivial.x, y, i, i0:int
Heq:φ (x) * φ (y) = φ (i) * wB + φ (i0)
H:is_zero i = true
[||(if is_zero i0 then W0 else DoubleType.WW i i0)||] =
φ (i) * wB + φ (i0)
 apply is_zero_spec in H;rewrite H, to_Z_0.x, y, i, i0:int
Heq:φ (x) * φ (y) = φ (i) * wB + φ (i0)
H:i = 0%int63
[||(if is_zero i0
    then W0
    else DoubleType.WW 0%int63 i0)||] =
0 * wB + φ (i0)
 case_eq (is_zero i0);intros;trivial.x, y, i, i0:int
Heq:φ (x) * φ (y) = φ (i) * wB + φ (i0)
H:i = 0%int63
H0:is_zero i0 = true
[||W0||] = 0 * wB + φ (i0)
 apply is_zero_spec in H0;rewrite H0, to_Z_0, Zmult_comm;trivial.
Qed.

Lemma squarec_spec :
  forall x,
    [||x *c x||] = [|x|] * [|x|].∀ x : int, [||x *c x||] = φ (x) * φ (x)
Proof (fun x => mulc_WW_spec x x).

Lemma diveucl_spec_aux : forall a b, 0 < [|b|] ->
  let (q,r) := diveucl a b in
  [|a|] = [|q|] * [|b|] + [|r|] /\
  0 <= [|r|] < [|b|].∀ a b : int,
  0 < φ (b)
  → let (q, r) := diveucl a b in
    φ (a) = φ (q) * φ (b) + φ (r)
    ∧ 0 <= φ (r) ∧ φ (r) < φ (b)
Proof.∀ a b : int,
  0 < φ (b)
  → let (q, r) := diveucl a b in
    φ (a) = φ (q) * φ (b) + φ (r)
    ∧ 0 <= φ (r) ∧ φ (r) < φ (b)
 intros a b H;assert (W:= diveucl_spec a b).a, b:int
H:0 < φ (b)
W:let (q, r) := diveucl a b in
(φ (q), φ (r)) = Z.div_eucl φ (a) φ (b)
let (q, r) := diveucl a b in
φ (a) = φ (q) * φ (b) + φ (r)
∧ 0 <= φ (r) ∧ φ (r) < φ (b)
 assert ([|b|]>0) by (auto with zarith).a, b:int
H:0 < φ (b)
W:let (q, r) := diveucl a b in
(φ (q), φ (r)) = Z.div_eucl φ (a) φ (b)
H0:φ (b) > 0
let (q, r) := diveucl a b in
φ (a) = φ (q) * φ (b) + φ (r)
∧ 0 <= φ (r) ∧ φ (r) < φ (b)
 generalize (Z_div_mod [|a|] [|b|] H0).a, b:int
H:0 < φ (b)
W:let (q, r) := diveucl a b in
(φ (q), φ (r)) = Z.div_eucl φ (a) φ (b)
H0:φ (b) > 0
(let (q, r) := Z.div_eucl φ (a) φ (b) in
 φ (a) = φ (b) * q + r ∧ 0 <= r ∧ r < φ (b))
→ let (q, r) := diveucl a b in
  φ (a) = φ (q) * φ (b) + φ (r)
  ∧ 0 <= φ (r) ∧ φ (r) < φ (b)
 destruct (diveucl a b);destruct (Z.div_eucl [|a|] [|b|]).a, b:int
H:0 < φ (b)
i, i0:int
z, z0:Z
W:(φ (i), φ (i0)) = (z, z0)
H0:φ (b) > 0
φ (a) = φ (b) * z + z0 ∧ 0 <= z0 ∧ z0 < φ (b)
→ φ (a) = φ (i) * φ (b) + φ (i0)
  ∧ 0 <= φ (i0) ∧ φ (i0) < φ (b)
 inversion W;rewrite Zmult_comm;trivial.
Qed.

Lemma shift_unshift_mod_2 : forall n p a, 0 <= p <= n ->
   ((a * 2 ^ (n - p)) mod (2^n) / 2 ^ (n - p)) mod (2^n) =
   a mod 2 ^ p.∀ n p a : Z,
  0 <= p ∧ p <= n
  → ((a * 2 ^ (n - p)) mod 2 ^ n / 2 ^ (n - p))
    mod 2 ^ n = a mod 2 ^ p
 Proof.∀ n p a : Z,
  0 <= p ∧ p <= n
  → ((a * 2 ^ (n - p)) mod 2 ^ n / 2 ^ (n - p))
    mod 2 ^ n = a mod 2 ^ p
   intros n p a H.n, p, a:Z
H:0 <= p ∧ p <= n
((a * 2 ^ (n - p)) mod 2 ^ n / 2 ^ (n - p)) mod 2 ^ n =
a mod 2 ^ p
   rewrite Zmod_small.n, p, a:Z
H:0 <= p ∧ p <= n
(a * 2 ^ (n - p)) mod 2 ^ n / 2 ^ (n - p) =
a mod 2 ^ p
n, p, a:Z
H:0 <= p ∧ p <= n
0 <= (a * 2 ^ (n - p)) mod 2 ^ n / 2 ^ (n - p)
∧ (a * 2 ^ (n - p)) mod 2 ^ n / 2 ^ (n - p) < 2 ^ n
   -n, p, a:Z
H:0 <= p ∧ p <= n
(a * 2 ^ (n - p)) mod 2 ^ n / 2 ^ (n - p) =
a mod 2 ^ p rewrite Zmod_eq by auto with zarith.n, p, a:Z
H:0 <= p ∧ p <= n
(a * 2 ^ (n - p) - a * 2 ^ (n - p) / 2 ^ n * 2 ^ n) /
2 ^ (n - p) = a mod 2 ^ p
     unfold Zminus at 1.n, p, a:Z
H:0 <= p ∧ p <= n
(a * 2 ^ (n - p) + - (a * 2 ^ (n - p) / 2 ^ n * 2 ^ n)) /
2 ^ (n - p) = a mod 2 ^ p
     rewrite Zdiv.Z_div_plus_full_l by auto with zarith.n, p, a:Z
H:0 <= p ∧ p <= n
a + - (a * 2 ^ (n - p) / 2 ^ n * 2 ^ n) / 2 ^ (n - p) =
a mod 2 ^ p
     replace (2 ^ n) with (2 ^ (n - p) * 2 ^ p) by (rewrite <- Zpower_exp; [ f_equal | | ]; lia).n, p, a:Z
H:0 <= p ∧ p <= n
a +
-
(a * 2 ^ (n - p) / (2 ^ (n - p) * 2 ^ p) *
 (2 ^ (n - p) * 2 ^ p)) / 2 ^ (n - p) = a mod 2 ^ p
     rewrite <- Zdiv_Zdiv, Z_div_mult by auto with zarith.n, p, a:Z
H:0 <= p ∧ p <= n
a +
- (a / 2 ^ p * (2 ^ (n - p) * 2 ^ p)) / 2 ^ (n - p) =
a mod 2 ^ p
     rewrite (Zmult_comm (2^(n-p))), Zmult_assoc.n, p, a:Z
H:0 <= p ∧ p <= n
a + - (a / 2 ^ p * 2 ^ p * 2 ^ (n - p)) / 2 ^ (n - p) =
a mod 2 ^ p
     rewrite Zopp_mult_distr_l.n, p, a:Z
H:0 <= p ∧ p <= n
a + - (a / 2 ^ p * 2 ^ p) * 2 ^ (n - p) / 2 ^ (n - p) =
a mod 2 ^ p
     rewrite Z_div_mult by auto with zarith.n, p, a:Z
H:0 <= p ∧ p <= n
a + - (a / 2 ^ p * 2 ^ p) = a mod 2 ^ p
     symmetry; apply Zmod_eq; auto with zarith.
   -n, p, a:Z
H:0 <= p ∧ p <= n
0 <= (a * 2 ^ (n - p)) mod 2 ^ n / 2 ^ (n - p)
∧ (a * 2 ^ (n - p)) mod 2 ^ n / 2 ^ (n - p) < 2 ^ n remember (a * 2 ^ (n - p)) as b.n, p, a:Z
H:0 <= p ∧ p <= n
b:Z
Heqb:b = a * 2 ^ (n - p)
0 <= b mod 2 ^ n / 2 ^ (n - p)
∧ b mod 2 ^ n / 2 ^ (n - p) < 2 ^ n
     destruct (Z_mod_lt b (2^n)); auto with zarith.n, p, a:Z
H:0 <= p ∧ p <= n
b:Z
Heqb:b = a * 2 ^ (n - p)
H0:0 <= b mod 2 ^ n
H1:b mod 2 ^ n < 2 ^ n
0 <= b mod 2 ^ n / 2 ^ (n - p)
∧ b mod 2 ^ n / 2 ^ (n - p) < 2 ^ n
     split.n, p, a:Z
H:0 <= p ∧ p <= n
b:Z
Heqb:b = a * 2 ^ (n - p)
H0:0 <= b mod 2 ^ n
H1:b mod 2 ^ n < 2 ^ n
0 <= b mod 2 ^ n / 2 ^ (n - p)
n, p, a:Z
H:0 <= p ∧ p <= n
b:Z
Heqb:b = a * 2 ^ (n - p)
H0:0 <= b mod 2 ^ n
H1:b mod 2 ^ n < 2 ^ n
b mod 2 ^ n / 2 ^ (n - p) < 2 ^ n
     apply Z_div_pos; auto with zarith.n, p, a:Z
H:0 <= p ∧ p <= n
b:Z
Heqb:b = a * 2 ^ (n - p)
H0:0 <= b mod 2 ^ n
H1:b mod 2 ^ n < 2 ^ n
b mod 2 ^ n / 2 ^ (n - p) < 2 ^ n
     apply Zdiv_lt_upper_bound; auto with zarith.n, p, a:Z
H:0 <= p ∧ p <= n
b:Z
Heqb:b = a * 2 ^ (n - p)
H0:0 <= b mod 2 ^ n
H1:b mod 2 ^ n < 2 ^ n
b mod 2 ^ n < 2 ^ n * 2 ^ (n - p)
     apply Z.lt_le_trans with (2^n); auto with zarith.n, p, a:Z
H:0 <= p ∧ p <= n
b:Z
Heqb:b = a * 2 ^ (n - p)
H0:0 <= b mod 2 ^ n
H1:b mod 2 ^ n < 2 ^ n
2 ^ n <= 2 ^ n * 2 ^ (n - p)
     generalize (pow2_pos (n - p)); nia.
 Qed.

Lemma div_le_0 : forall p x, 0 <= x -> 0 <= x / 2 ^ p.∀ p x : Z, 0 <= x → 0 <= x / 2 ^ p
 Proof.∀ p x : Z, 0 <= x → 0 <= x / 2 ^ p
  intros p x Hle;destruct (Z_le_gt_dec 0 p).p, x:Z
Hle:0 <= x
l:0 <= p
0 <= x / 2 ^ p
p, x:Z
Hle:0 <= x
g:0 > p
0 <= x / 2 ^ p
  apply  Zdiv_le_lower_bound;auto with zarith.p, x:Z
Hle:0 <= x
g:0 > p
0 <= x / 2 ^ p
  replace (2^p) with 0.p, x:Z
Hle:0 <= x
g:0 > p
0 <= x / 0
p, x:Z
Hle:0 <= x
g:0 > p
0 = 2 ^ p
  destruct x;compute;intro;discriminate.p, x:Z
Hle:0 <= x
g:0 > p
0 = 2 ^ p
  destruct p;trivial;discriminate.
 Qed.

Lemma div_lt : forall p x y, 0 <= x < y -> x / 2^p < y.∀ p x y : Z, 0 <= x ∧ x < y → x / 2 ^ p < y
 Proof.∀ p x y : Z, 0 <= x ∧ x < y → x / 2 ^ p < y
  intros p x y H;destruct (Z_le_gt_dec 0 p).p, x, y:Z
H:0 <= x ∧ x < y
l:0 <= p
x / 2 ^ p < y
p, x, y:Z
H:0 <= x ∧ x < y
g:0 > p
x / 2 ^ p < y
  apply Zdiv_lt_upper_bound;auto with zarith.p, x, y:Z
H:0 <= x ∧ x < y
l:0 <= p
x < y * 2 ^ p
p, x, y:Z
H:0 <= x ∧ x < y
g:0 > p
x / 2 ^ p < y
  apply Z.lt_le_trans with y;auto with zarith.p, x, y:Z
H:0 <= x ∧ x < y
l:0 <= p
y <= y * 2 ^ p
p, x, y:Z
H:0 <= x ∧ x < y
g:0 > p
x / 2 ^ p < y
  rewrite <- (Zmult_1_r y);apply Zmult_le_compat;auto with zarith.p, x, y:Z
H:0 <= x ∧ x < y
l:0 <= p
1 <= 2 ^ p
p, x, y:Z
H:0 <= x ∧ x < y
g:0 > p
x / 2 ^ p < y
  assert (0 < 2^p);auto with zarith.p, x, y:Z
H:0 <= x ∧ x < y
g:0 > p
x / 2 ^ p < y
  replace (2^p) with 0.p, x, y:Z
H:0 <= x ∧ x < y
g:0 > p
x / 0 < y
p, x, y:Z
H:0 <= x ∧ x < y
g:0 > p
0 = 2 ^ p
  destruct x;change (0<y);auto with zarith.p, x, y:Z
H:0 <= x ∧ x < y
g:0 > p
0 = 2 ^ p
  destruct p;trivial;discriminate.
 Qed.

Lemma P (A B C: Prop) :
  A → (B → C) → (A → B) → C.A, B, C:Prop
A → (B → C) → (A → B) → C
Proof.A, B, C:Prop
A → (B → C) → (A → B) → C tauto. Qed.

Lemma shift_unshift_mod_3:
  forall n p a : Z,
  0 <= p <= n ->
  (a * 2 ^ (n - p)) mod 2 ^ n / 2 ^ (n - p) = a mod 2 ^ p.∀ n p a : Z,
  0 <= p ∧ p <= n
  → (a * 2 ^ (n - p)) mod 2 ^ n / 2 ^ (n - p) =
    a mod 2 ^ p
Proof.∀ n p a : Z,
  0 <= p ∧ p <= n
  → (a * 2 ^ (n - p)) mod 2 ^ n / 2 ^ (n - p) =
    a mod 2 ^ p
 intros;rewrite <- (shift_unshift_mod_2 n p a);[ | auto with zarith].n, p, a:Z
H:0 <= p ∧ p <= n
(a * 2 ^ (n - p)) mod 2 ^ n / 2 ^ (n - p) =
((a * 2 ^ (n - p)) mod 2 ^ n / 2 ^ (n - p)) mod 2 ^ n
 symmetry;apply Zmod_small.n, p, a:Z
H:0 <= p ∧ p <= n
0 <= (a * 2 ^ (n - p)) mod 2 ^ n / 2 ^ (n - p)
∧ (a * 2 ^ (n - p)) mod 2 ^ n / 2 ^ (n - p) < 2 ^ n
 generalize (a * 2 ^ (n - p));intros w.n, p, a:Z
H:0 <= p ∧ p <= n
w:Z
0 <= w mod 2 ^ n / 2 ^ (n - p)
∧ w mod 2 ^ n / 2 ^ (n - p) < 2 ^ n
 generalize (2 ^ (n - p)) (pow2_pos (n - p)); intros x; apply P.n, p, a:Z
H:0 <= p ∧ p <= n
w, x:Z
0 <= n - p
n, p, a:Z
H:0 <= p ∧ p <= n
w, x:Z
x > 0 → 0 <= w mod 2 ^ n / x ∧ w mod 2 ^ n / x < 2 ^ n lia.n, p, a:Z
H:0 <= p ∧ p <= n
w, x:Z
x > 0 → 0 <= w mod 2 ^ n / x ∧ w mod 2 ^ n / x < 2 ^ n intros hx.n, p, a:Z
H:0 <= p ∧ p <= n
w, x:Z
hx:x > 0
0 <= w mod 2 ^ n / x ∧ w mod 2 ^ n / x < 2 ^ n
 generalize (2 ^ n) (pow2_pos n); intros y; apply P.n, p, a:Z
H:0 <= p ∧ p <= n
w, x:Z
hx:x > 0
y:Z
0 <= n
n, p, a:Z
H:0 <= p ∧ p <= n
w, x:Z
hx:x > 0
y:Z
y > 0 → 0 <= w mod y / x ∧ w mod y / x < y lia.n, p, a:Z
H:0 <= p ∧ p <= n
w, x:Z
hx:x > 0
y:Z
y > 0 → 0 <= w mod y / x ∧ w mod y / x < y intros hy.n, p, a:Z
H:0 <= p ∧ p <= n
w, x:Z
hx:x > 0
y:Z
hy:y > 0
0 <= w mod y / x ∧ w mod y / x < y
 elim_div.n, p, a:Z
H:0 <= p ∧ p <= n
w, x:Z
hx:x > 0
y:Z
hy:y > 0
∀ z z0 : Z,
  (x ≠ 0
   → (let (_, r) := Z.div_eucl w y in r) = x * z + z0
     ∧ (0 <= z0 ∧ z0 < x ∨ x < z0 ∧ z0 <= 0))
  → 0 <= z ∧ z < y intros q r.n, p, a:Z
H:0 <= p ∧ p <= n
w, x:Z
hx:x > 0
y:Z
hy:y > 0
q, r:Z
(x ≠ 0
 → (let (_, r0) := Z.div_eucl w y in r0) = x * q + r
   ∧ (0 <= r ∧ r < x ∨ x < r ∧ r <= 0))
→ 0 <= q ∧ q < y apply P.n, p, a:Z
H:0 <= p ∧ p <= n
w, x:Z
hx:x > 0
y:Z
hy:y > 0
q, r:Z
x ≠ 0
n, p, a:Z
H:0 <= p ∧ p <= n
w, x:Z
hx:x > 0
y:Z
hy:y > 0
q, r:Z
(let (_, r0) := Z.div_eucl w y in r0) = x * q + r
∧ (0 <= r ∧ r < x ∨ x < r ∧ r <= 0) → 0 <= q ∧ q < y lia.n, p, a:Z
H:0 <= p ∧ p <= n
w, x:Z
hx:x > 0
y:Z
hy:y > 0
q, r:Z
(let (_, r0) := Z.div_eucl w y in r0) = x * q + r
∧ (0 <= r ∧ r < x ∨ x < r ∧ r <= 0) → 0 <= q ∧ q < y
 elim_div.n, p, a:Z
H:0 <= p ∧ p <= n
w, x:Z
hx:x > 0
y:Z
hy:y > 0
q, r:Z
∀ z z0 : Z,
  (y ≠ 0
   → w = y * z + z0
     ∧ (0 <= z0 ∧ z0 < y ∨ y < z0 ∧ z0 <= 0))
  → z0 = x * q + r ∧ (0 <= r ∧ r < x ∨ x < r ∧ r <= 0)
    → 0 <= q ∧ q < y intros z t.n, p, a:Z
H:0 <= p ∧ p <= n
w, x:Z
hx:x > 0
y:Z
hy:y > 0
q, r, z, t:Z
(y ≠ 0
 → w = y * z + t ∧ (0 <= t ∧ t < y ∨ y < t ∧ t <= 0))
→ t = x * q + r ∧ (0 <= r ∧ r < x ∨ x < r ∧ r <= 0)
  → 0 <= q ∧ q < y refine (P _ _ _ _ _).n, p, a:Z
H:0 <= p ∧ p <= n
w, x:Z
hx:x > 0
y:Z
hy:y > 0
q, r, z, t:Z
y ≠ 0
n, p, a:Z
H:0 <= p ∧ p <= n
w, x:Z
hx:x > 0
y:Z
hy:y > 0
q, r, z, t:Z
w = y * z + t ∧ (0 <= t ∧ t < y ∨ y < t ∧ t <= 0)
→ t = x * q + r ∧ (0 <= r ∧ r < x ∨ x < r ∧ r <= 0)
  → 0 <= q ∧ q < y lia.n, p, a:Z
H:0 <= p ∧ p <= n
w, x:Z
hx:x > 0
y:Z
hy:y > 0
q, r, z, t:Z
w = y * z + t ∧ (0 <= t ∧ t < y ∨ y < t ∧ t <= 0)
→ t = x * q + r ∧ (0 <= r ∧ r < x ∨ x < r ∧ r <= 0)
  → 0 <= q ∧ q < y
 intros [ ? [ ht | ] ]; [ | lia ]; subst w.n, p, a:Z
H:0 <= p ∧ p <= n
x:Z
hx:x > 0
y:Z
hy:y > 0
q, r, z, t:Z
ht:0 <= t ∧ t < y
t = x * q + r ∧ (0 <= r ∧ r < x ∨ x < r ∧ r <= 0)
→ 0 <= q ∧ q < y
 intros [ ? [ hr | ] ]; [ | lia ]; subst t.n, p, a:Z
H:0 <= p ∧ p <= n
x:Z
hx:x > 0
y:Z
hy:y > 0
q, r, z:Z
ht:0 <= x * q + r ∧ x * q + r < y
hr:0 <= r ∧ r < x
0 <= q ∧ q < y
 nia.
Qed.

Lemma pos_mod_spec w p : φ(pos_mod p w) = φ(w) mod (2 ^ φ(p)).w, p:int
φ (pos_mod p w) = φ (w) mod 2 ^ φ (p)
Proof.w, p:int
φ (pos_mod p w) = φ (w) mod 2 ^ φ (p)
  simpl.w, p:int
φ (pos_mod_int p w) = φ (w) mod 2 ^ φ (p) unfold pos_mod_int.w, p:int
φ (if p ≤ Int63.digits
   then
    (w << (Int63.digits - p)) >> (Int63.digits - p)
   else w) = φ (w) mod 2 ^ φ (p)
  assert (W:=to_Z_bounded p);assert (W':=to_Z_bounded Int63.digits);assert (W'' := to_Z_bounded w).w, p:int
W:0 <= φ (p) ∧ φ (p) < wB
W':0 <= φ (Int63.digits) ∧ φ (Int63.digits) < wB
W'':0 <= φ (w) ∧ φ (w) < wB
φ (if p ≤ Int63.digits
   then
    (w << (Int63.digits - p)) >> (Int63.digits - p)
   else w) = φ (w) mod 2 ^ φ (p)
  case lebP; intros hle.w, p:int
W:0 <= φ (p) ∧ φ (p) < wB
W':0 <= φ (Int63.digits) ∧ φ (Int63.digits) < wB
W'':0 <= φ (w) ∧ φ (w) < wB
hle:φ (p) <= φ (Int63.digits)
φ ((w << (Int63.digits - p)) >> (Int63.digits - p)) =
φ (w) mod 2 ^ φ (p)
w, p:int
W:0 <= φ (p) ∧ φ (p) < wB
W':0 <= φ (Int63.digits) ∧ φ (Int63.digits) < wB
W'':0 <= φ (w) ∧ φ (w) < wB
hle:¬ φ (p) <= φ (Int63.digits)
φ (w) = φ (w) mod 2 ^ φ (p)
  2: {w, p:int
W:0 <= φ (p) ∧ φ (p) < wB
W':0 <= φ (Int63.digits) ∧ φ (Int63.digits) < wB
W'':0 <= φ (w) ∧ φ (w) < wB
hle:¬ φ (p) <= φ (Int63.digits)
φ (w) = φ (w) mod 2 ^ φ (p)
    symmetry; apply Zmod_small.w, p:int
W:0 <= φ (p) ∧ φ (p) < wB
W':0 <= φ (Int63.digits) ∧ φ (Int63.digits) < wB
W'':0 <= φ (w) ∧ φ (w) < wB
hle:¬ φ (p) <= φ (Int63.digits)
0 <= φ (w) ∧ φ (w) < 2 ^ φ (p)
    assert (2 ^ [|Int63.digits|] < 2 ^ [|p|]); [ apply Zpower_lt_monotone; auto with zarith | ].w, p:int
W:0 <= φ (p) ∧ φ (p) < wB
W':0 <= φ (Int63.digits) ∧ φ (Int63.digits) < wB
W'':0 <= φ (w) ∧ φ (w) < wB
hle:¬ φ (p) <= φ (Int63.digits)
H:2 ^ φ (Int63.digits) < 2 ^ φ (p)
0 <= φ (w) ∧ φ (w) < 2 ^ φ (p)
    change wB with (2 ^ [|Int63.digits|]) in *; auto with zarith. }w, p:int
W:0 <= φ (p) ∧ φ (p) < wB
W':0 <= φ (Int63.digits) ∧ φ (Int63.digits) < wB
W'':0 <= φ (w) ∧ φ (w) < wB
hle:φ (p) <= φ (Int63.digits)
φ ((w << (Int63.digits - p)) >> (Int63.digits - p)) =
φ (w) mod 2 ^ φ (p)
  rewrite <- (shift_unshift_mod_3 [|Int63.digits|] [|p|] [|w|]) by auto with zarith.w, p:int
W:0 <= φ (p) ∧ φ (p) < wB
W':0 <= φ (Int63.digits) ∧ φ (Int63.digits) < wB
W'':0 <= φ (w) ∧ φ (w) < wB
hle:φ (p) <= φ (Int63.digits)
φ ((w << (Int63.digits - p)) >> (Int63.digits - p)) =
(φ (w) * 2 ^ (φ (Int63.digits) - φ (p)))
mod 2 ^ φ (Int63.digits) /
2 ^ (φ (Int63.digits) - φ (p))
  replace ([|Int63.digits|] - [|p|]) with [|Int63.digits - p|] by (rewrite sub_spec, Zmod_small; auto with zarith).w, p:int
W:0 <= φ (p) ∧ φ (p) < wB
W':0 <= φ (Int63.digits) ∧ φ (Int63.digits) < wB
W'':0 <= φ (w) ∧ φ (w) < wB
hle:φ (p) <= φ (Int63.digits)
φ ((w << (Int63.digits - p)) >> (Int63.digits - p)) =
(φ (w) * 2 ^ φ (Int63.digits - p))
mod 2 ^ φ (Int63.digits) / 2 ^ φ (Int63.digits - p)
  rewrite lsr_spec, lsl_spec; reflexivity.
Qed.

{2 Specification and proof}

Instance int_specs : ZnZ.Specs int_ops := {
    spec_to_Z   := to_Z_bounded;
    spec_of_pos := positive_to_int_spec;
    spec_zdigits := refl_equal _;
    spec_more_than_1_digit:= refl_equal _;
    spec_0 := to_Z_0;
    spec_1 := to_Z_1;
    spec_m1 := refl_equal _;
    spec_compare := compare_spec;
    spec_eq0 := is_zero_spec_aux;
    spec_opp_c := oppc_spec;
    spec_opp := opp_spec;
    spec_opp_carry := oppcarry_spec;
    spec_succ_c := succc_spec;
    spec_add_c := addc_spec;
    spec_add_carry_c := addcarryc_spec;
    spec_succ := succ_spec;
    spec_add := add_spec;
    spec_add_carry := addcarry_spec;
    spec_pred_c := predc_spec;
    spec_sub_c := subc_spec;
    spec_sub_carry_c := subcarryc_spec;
    spec_pred := pred_spec;
    spec_sub := sub_spec;
    spec_sub_carry := subcarry_spec;
    spec_mul_c := mulc_WW_spec;
    spec_mul := mul_spec;
    spec_square_c := squarec_spec;
    spec_div21 := diveucl_21_spec_aux;
    spec_div_gt := fun a b _ => diveucl_spec_aux a b;
    spec_div := diveucl_spec_aux;
    spec_modulo_gt := fun a b _ _ => mod_spec a b;
    spec_modulo := fun a b _ => mod_spec a b;
    spec_gcd_gt := fun a b _ => gcd_spec a b;
    spec_gcd := gcd_spec;
    spec_head00 := head00_spec;
    spec_head0 := head0_spec;
    spec_tail00 := tail00_spec;
    spec_tail0 := tail0_spec;
    spec_add_mul_div := addmuldiv_spec;
    spec_pos_mod := pos_mod_spec;
    spec_is_even := is_even_spec;
    spec_sqrt2 := sqrt2_spec;
    spec_sqrt := sqrt_spec;
    spec_land := land_spec';
    spec_lor := lor_spec';
    spec_lxor := lxor_spec' }.



Module Int63Cyclic <: CyclicType.
  Definition t := int.
  Definition ops := int_ops.
  Definition specs := int_specs.
End Int63Cyclic.