Frontend for the standard version of Coq (still bad computational behavior)

12 files changed, 3551 insertions, 325 deletions

diff --git a/src/configure.sh b/src/configure.sh
index 277f560..83b70d3 100755
--- a/src/configure.sh
+++ b/src/configure.sh
@@ -5,6 +5,9 @@ set -e
 if [ $@ -a $@ = -standard ]; then
     cp versions/standard/Makefile Makefile
     cp versions/standard/Int63/Int63_standard.v versions/standard/Int63/Int63.v
+    cp versions/standard/Int63/Int63Lib_standard.v versions/standard/Int63/Int63Lib.v
+    cp versions/standard/Int63/Cyclic63_standard.v versions/standard/Int63/Cyclic63.v
+    cp versions/standard/Int63/Ring63_standard.v versions/standard/Int63/Ring63.v
     cp versions/standard/Int63/Int63Native_standard.v versions/standard/Int63/Int63Native.v
     cp versions/standard/Int63/Int63Op_standard.v versions/standard/Int63/Int63Op.v
     cp versions/standard/Int63/Int63Axioms_standard.v versions/standard/Int63/Int63Axioms.v
diff --git a/src/versions/standard/Array/PArray_standard.v b/src/versions/standard/Array/PArray_standard.v
index f27664e..ddbe0ab 100644
--- a/src/versions/standard/Array/PArray_standard.v
+++ b/src/versions/standard/Array/PArray_standard.v
@@ -15,39 +15,79 @@
 (**************************************************************************)
 
 
+(* Software implementation of arrays, based on finite maps using AVL
+   trees *)
+
+
 Require Export Int63.
+Require Import Ring63.
+Require Int63Lib.
+Require FMapAVL.
+
+Local Open Scope int63_scope.
+
 
-Register array : Type -> Type as array_type.
+Module Map := FMapAVL.Make(IntOrderedType).
 
-Register make : forall {A:Type}, int -> A -> array A as array_make.
+Definition array (A:Type) : Type :=
+  (Map.t A * A * int)%type.
 
-Register get : forall {A:Type}, array A -> int -> A as array_get.
+Definition make {A:Type} (l:int) (d:A) : array A :=
+  let r :=
+      if l == 0 then
+        Map.empty A
+      else
+        foldi (fun j m => Map.add j d m) 0 (l-1) (Map.empty A) in
+  (r, d, l).
 
-Register default : forall {A:Type}, array A -> A as array_default.
+Definition get {A:Type} (t:array A) (i:int) : A :=
+  let (td,_) := t in
+  let (t,d) := td in
+  match Map.find i t with
+    | Some x => x
+    | None => d
+  end.
 
-Register set : forall {A:Type}, array A -> int -> A -> array A as array_set.
+Definition default {A:Type} (t:array A) : A :=
+  let (td,_) := t in let (_,d) := td in d.
 
-Register length : forall {A:Type}, array A -> int as array_length.
+Definition set {A:Type} (t:array A) (i:int) (a:A) : array A :=
+  let (td,l) := t in
+  if l <= i then
+    t
+  else
+    let (t,d) := td in
+    (Map.add i a t, d, l).
 
-Register copy : forall {A:Type}, array A -> array A as array_copy.
+Definition length {A:Type} (t:array A) : int :=
+  let (_,l) := t in l.
 
-Register reroot : forall {A:Type}, array A -> array A as array_reroot.
+Definition copy {A:Type} (t:array A) : array A := t.
 
-(* Not done with the vm *)
-Register init : forall {A:Type}, int -> (int -> A) -> A -> array A as array_init.
+Definition reroot : forall {A:Type}, array A -> array A := @copy.
 
-Register map : forall {A B:Type}, (A -> B) -> array A -> array B as array_map.
+Definition init {A:Type} (l:int) (f:int -> A) (d:A) : array A :=
+  let r :=
+      if l == 0 then
+        Map.empty A
+      else
+        foldi (fun j m => Map.add j (f j) m) 0 (l-1) (Map.empty A) in
+  (r, d, l).
+
+Definition map {A B:Type} (f:A -> B) (t:array A) : array B :=
+  let (td,l) := t in
+  let (t,d) := td in
+  (Map.map f t, f d, l).
 
 Delimit Scope array_scope with array.
 Notation "t '.[' i ']'" := (get t i) (at level 50) : array_scope.
 Notation "t '.[' i '<-' a ']'" := (set t i a) (at level 50) : array_scope.
 
-Local Open Scope int63_scope.
 Local Open Scope array_scope.
 
 Set Vm Optimize.
 
-Definition max_array_length := 4194302.
+Definition max_array_length := Eval vm_compute in (Int63Lib.phi_inv 4194302).
 
 (** Axioms *)
 Axiom get_outofbound : forall A (t:array A) i, (i < length t) = false -> t.[i] = default t.
@@ -62,7 +102,7 @@ Axiom default_make : forall A (a:A) size, (default (make size a)) = a.
 
 Axiom ltb_length : forall A (t:array A), length t <= max_array_length = true.
 
-Axiom length_make : forall A size (a:A), 
+Axiom length_make : forall A size (a:A),
   length (make size a) = if size <= max_array_length then size else max_array_length.
 Axiom length_set : forall A t i (a:A),
   length (t.[i<-a]) = length t.
@@ -125,22 +165,22 @@ Definition mapi {A B:Type} (f:int->A->B) (t:array A) :=
 
 Definition foldi_left {A B:Type} (f:int -> A -> B -> A) a (t:array B) :=
   let len := length t in
-  if 0 == len then a 
+  if 0 == len then a
   else foldi (fun i a => f i a (t.[i])) 0 (len - 1) a.
 
 Definition fold_left {A B:Type} (f: A -> B -> A) a (t:array B) :=
   let len := length t in
-  if 0 == len then a 
+  if 0 == len then a
   else foldi (fun i a => f a (t.[i])) 0 (length t - 1) a.
 
 Definition foldi_right {A B:Type} (f:int -> A -> B -> B) (t:array A) b :=
   let len := length t in
-  if 0 == len then b 
+  if 0 == len then b
   else foldi_down (fun i b => f i (t.[i]) b) (len - 1) 0 b.
 
 Definition fold_right {A B:Type} (f: A -> B -> B) (t:array A) b :=
   let len := length t in
-  if 0 == len then b 
+  if 0 == len then b
   else foldi_down (fun i b => f (t.[i]) b) (len - 1) 0 b.
 
 (* Lemmas *)
@@ -150,7 +190,6 @@ Proof.
  intros A t;assert (length t < length t = false).
   apply Bool.not_true_is_false; apply leb_not_gtb; apply leb_refl.
  rewrite <- (get_outofbound _ (copy t) (length t)), <- (get_outofbound _ t (length t)), get_copy;trivial.
- rewrite length_copy;trivial.
 Qed.
 
 Lemma reroot_default : forall A (t:array A), default (reroot t) = default t.
@@ -158,10 +197,9 @@ Proof.
  intros A t;assert (length t < length t = false).
   apply Bool.not_true_is_false; apply leb_not_gtb; apply leb_refl.
  rewrite <- (get_outofbound _ (reroot t) (length t)), <- (get_outofbound _ t (length t)), get_reroot;trivial.
- rewrite length_reroot;trivial.
 Qed.
 
-Lemma get_set_same_default : 
+Lemma get_set_same_default :
    forall (A : Type) (t : array A) (i : int) ,
        (t .[ i <- default t]) .[ i] = default t.
 Proof.
@@ -172,14 +210,14 @@ Proof.
 Qed.
 
 Lemma get_not_default_lt : forall A (t:array A) x,
- t.[x] <> default t -> (x < length t)%int63 = true.
+ t.[x] <> default t -> x < length t = true.
 Proof.
  intros A t x Hd.
  case_eq (x < length t);intros Heq;[trivial | ].
  elim Hd;rewrite get_outofbound;trivial.
 Qed.
 
-Lemma foldi_left_Ind : 
+Lemma foldi_left_Ind :
      forall A B (P : int -> A -> Prop) (f : int -> A -> B -> A) (t:array B),
      (forall a i, i < length t = true -> P i a -> P (i+1) (f i a (t.[i]))) ->
      forall a, P 0 a ->
@@ -196,7 +234,7 @@ Proof.
  intros;apply H;trivial. rewrite ltb_leb_sub1;auto.
 Qed.
 
-Lemma fold_left_Ind : 
+Lemma fold_left_Ind :
      forall A B (P : int -> A -> Prop) (f : A -> B -> A) (t:array B),
      (forall a i, i < length t = true -> P i a -> P (i+1) (f a (t.[i]))) ->
      forall a, P 0 a ->
@@ -206,7 +244,7 @@ Proof.
  apply (foldi_left_Ind A B P (fun i => f));trivial.
 Qed.
 
-Lemma fold_left_ind : 
+Lemma fold_left_ind :
      forall A B (P : A -> Prop) (f : A -> B -> A) (t:array B),
      (forall a i, i < length t = true -> P a -> P (f a (t.[i]))) ->
      forall a, P a ->
@@ -215,7 +253,7 @@ Proof.
  intros;apply (fold_left_Ind A B (fun _ => P));trivial.
 Qed.
 
-Lemma foldi_right_Ind : 
+Lemma foldi_right_Ind :
      forall A B (P : int -> A -> Prop) (f : int -> B -> A -> A) (t:array B),
      (forall a i, i < length t = true -> P (i+1) a -> P i (f i (t.[i]) a)) ->
      forall a, P (length t) a ->
@@ -237,8 +275,8 @@ Proof.
  rewrite <-(to_Z_add_1 _ _ H4), of_to_Z in H3;auto.
  exact H1.
 Qed.
- 
-Lemma fold_right_Ind : 
+
+Lemma fold_right_Ind :
      forall A B (P : int -> A -> Prop) (f : B -> A -> A) (t:array B),
      (forall a i, i < length t = true -> P (i+1) a -> P i (f (t.[i]) a)) ->
      forall a, P (length t) a ->
@@ -247,7 +285,7 @@ Proof.
  intros;apply (foldi_right_Ind A B P (fun i => f));trivial.
 Qed.
 
-Lemma fold_right_ind : 
+Lemma fold_right_ind :
      forall A B (P : A -> Prop) (f : B -> A -> A) (t:array B),
      (forall a i, i < length t = true -> P a -> P (f (t.[i]) a)) ->
      forall a, P a ->
@@ -292,7 +330,7 @@ Qed.
 
 Local Open Scope list_scope.
 
-Definition to_list_ntr A (t:array A) := 
+Definition to_list_ntr A (t:array A) :=
   let len := length t in
   if 0 == len then nil
   else foldi_ntr _ (fun i l => t.[i] :: l) 0 (len - 1) nil.
@@ -311,7 +349,7 @@ Proof.
  assert (0%Z <> [|length t|]);[ | omega].
    intros Heq;elim n;apply to_Z_inj;trivial.
 Qed.
-    
+
 Lemma fold_left_to_list : forall (A B:Type) (t:array A) (f: B -> A -> B) b,
    fold_left f b t = List.fold_left f (to_list t) b.
 Proof.
@@ -336,7 +374,7 @@ Local Open Scope bool_scope.
 
 Definition eqb {A:Type} (Aeqb: A->A->bool) (t1 t2:array A) :=
   (length t1 == length t2) &&
-  Aeqb (default t1) (default t2) && 
+  Aeqb (default t1) (default t2) &&
   forallbi (fun i a1 => Aeqb a1 (t2.[i])) t1.
 
 Lemma reflect_eqb : forall (A:Type) (Aeqb:A->A->bool),
@@ -358,5 +396,3 @@ Proof.
  intros i _; rewrite <- (reflect_iff _ _ (HA _ _));trivial.
  rewrite <- not_true_iff_false, <- (reflect_iff _ _ (HA _ _)) in H0;apply H0;trivial.
 Qed.
-
- 
diff --git a/src/versions/standard/Int63/Cyclic63_standard.v b/src/versions/standard/Int63/Cyclic63_standard.v
new file mode 100644
index 0000000..2c24655
--- /dev/null
+++ b/src/versions/standard/Int63/Cyclic63_standard.v
@@ -0,0 +1,2491 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(*   \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^63)Z *)
+
+(**
+Author: Arnaud Spiwack (+ Pierre Letouzey)
+*)
+
+Require Import List.
+Require Import Min.
+Require Import Int63Lib.
+Require Import Znumtheory.
+Require Import Zgcd_alt.
+Require Import Zpow_facts.
+Require Import BigNumPrelude.
+Require Import CyclicAxioms.
+Require Import ROmega.
+
+Local Open Scope nat_scope.
+Local Open Scope int63_scope.
+
+Section Basics.
+
+ (** * Basic results about [iszero], [shiftl], [shiftr] *)
+
+ Lemma iszero_eq0 : forall x, iszero x = true -> x=0.
+ Proof.
+ destruct x; simpl; intros.
+ repeat
+   match goal with H:(if ?d then _ else _) = true |- _ =>
+     destruct d; try discriminate
+   end.
+ reflexivity.
+ Qed.
+
+ Lemma iszero_not_eq0 : forall x, iszero x = false -> x<>0.
+ Proof.
+ intros x H Eq; rewrite Eq in H; simpl in *; discriminate.
+ Qed.
+
+ Lemma sneakl_shiftr : forall x,
+  x = sneakl (firstr x) (shiftr x).
+ Proof.
+ destruct x; simpl; auto.
+ Qed.
+
+ Lemma sneakr_shiftl : forall x,
+  x = sneakr (firstl x) (shiftl x).
+ Proof.
+ destruct x; simpl; auto.
+ Qed.
+
+ Lemma twice_zero : forall x,
+  twice x = 0 <-> twice_plus_one x = 1.
+ Proof.
+ destruct x; simpl in *; split;
+ intro H; injection H; intros; subst; auto.
+ Qed.
+
+ Lemma twice_or_twice_plus_one : forall x,
+  x = twice (shiftr x) \/ x = twice_plus_one (shiftr x).
+ Proof.
+ intros; case_eq (firstr x); intros.
+ destruct x; simpl in *; rewrite H; auto.
+ destruct x; simpl in *; rewrite H; auto.
+ Qed.
+
+
+
+ (** * Iterated shift to the right *)
+
+ Definition nshiftr n x := iter_nat n _ shiftr x.
+
+ Lemma nshiftr_S :
+  forall n x, nshiftr (S n) x = shiftr (nshiftr n x).
+ Proof.
+ reflexivity.
+ Qed.
+
+ Lemma nshiftr_S_tail :
+  forall n x, nshiftr (S n) x = nshiftr n (shiftr x).
+ Proof.
+ induction n; simpl; auto.
+ intros; rewrite nshiftr_S, IHn, nshiftr_S; auto.
+ Qed.
+
+ Lemma nshiftr_n_0 : forall n, nshiftr n 0 = 0.
+ Proof.
+ induction n; simpl; auto.
+ rewrite nshiftr_S, IHn; auto.
+ Qed.
+
+ Lemma nshiftr_size : forall x, nshiftr size x = 0.
+ Proof.
+ destruct x; simpl; auto.
+ Qed.
+
+ Lemma nshiftr_above_size : forall k x, size<=k ->
+  nshiftr k x = 0.
+ Proof.
+ intros.
+ replace k with ((k-size)+size)%nat by omega.
+ induction (k-size)%nat; auto.
+  rewrite nshiftr_size; auto.
+  simpl; rewrite nshiftr_S, IHn; auto.
+ Qed.
+
+ (** * Iterated shift to the left *)
+
+ Definition nshiftl n x := iter_nat n _ shiftl x.
+
+ Lemma nshiftl_S :
+  forall n x, nshiftl (S n) x = shiftl (nshiftl n x).
+ Proof.
+ reflexivity.
+ Qed.
+
+ Lemma nshiftl_S_tail :
+  forall n x, nshiftl (S n) x = nshiftl n (shiftl x).
+ Proof.
+ induction n; simpl; auto.
+ intros; rewrite nshiftl_S, IHn, nshiftl_S; auto.
+ Qed.
+
+ Lemma nshiftl_n_0 : forall n, nshiftl n 0 = 0.
+ Proof.
+ induction n; simpl; auto.
+ rewrite nshiftl_S, IHn; auto.
+ Qed.
+
+ Lemma nshiftl_size : forall x, nshiftl size x = 0.
+ Proof.
+ destruct x; simpl; auto.
+ Qed.
+
+ Lemma nshiftl_above_size : forall k x, size<=k ->
+  nshiftl k x = 0.
+ Proof.
+ intros.
+ replace k with ((k-size)+size)%nat by omega.
+ induction (k-size)%nat; auto.
+  rewrite nshiftl_size; auto.
+  simpl; rewrite nshiftl_S, IHn; auto.
+ Qed.
+
+ Lemma firstr_firstl :
+  forall x, firstr x = firstl (nshiftl (pred size) x).
+ Proof.
+ destruct x; simpl; auto.
+ Qed.
+
+ Lemma firstl_firstr :
+  forall x, firstl x = firstr (nshiftr (pred size) x).
+ Proof.
+ destruct x; simpl; auto.
+ Qed.
+
+ (** More advanced results about [nshiftr] *)
+
+ Lemma nshiftr_predsize_0_firstl : forall x,
+  nshiftr (pred size) x = 0 -> firstl x = D0.
+ Proof.
+ destruct x; compute; intros H; injection H; intros; subst; auto.
+ Qed.
+
+ Lemma nshiftr_0_propagates : forall n p x, n <= p ->
+  nshiftr n x = 0 -> nshiftr p x = 0.
+ Proof.
+ intros.
+ replace p with ((p-n)+n)%nat by omega.
+ induction (p-n)%nat.
+ simpl; auto.
+ simpl; rewrite nshiftr_S; rewrite IHn0; auto.
+ Qed.
+
+ Lemma nshiftr_0_firstl : forall n x, n < size ->
+  nshiftr n x = 0 -> firstl x = D0.
+ Proof.
+ intros.
+ apply nshiftr_predsize_0_firstl.
+ apply nshiftr_0_propagates with n; auto; omega.
+ Qed.
+
+ (** * Some induction principles over [int63] *)
+
+ (** Not used for the moment. Are they really useful ? *)
+
+ Lemma int63_ind_sneakl : forall P : int63->Prop,
+  P 0 ->
+  (forall x d, P x -> P (sneakl d x)) ->
+  forall x, P x.
+ Proof.
+ intros.
+ assert (forall n, n<=size -> P (nshiftr (size - n) x)).
+ induction n; intros.
+ rewrite nshiftr_size; auto.
+ rewrite sneakl_shiftr.
+ apply H0.
+ change (P (nshiftr (S (size - S n)) x)).
+ replace (S (size - S n))%nat with (size - n)%nat by omega.
+ apply IHn; omega.
+ change x with (nshiftr (size-size) x); auto.
+ Qed.
+
+ Lemma int63_ind_twice : forall P : int63->Prop,
+  P 0 ->
+  (forall x, P x -> P (twice x)) ->
+  (forall x, P x -> P (twice_plus_one x)) ->
+  forall x, P x.
+ Proof.
+ induction x using int63_ind_sneakl; auto.
+ destruct d; auto.
+ Qed.
+
+
+ (** * Some generic results about [recr] *)
+
+ Section Recr.
+
+ (** [recr] satisfies the fixpoint equation used for its definition. *)
+
+ Variable (A:Type)(case0:A)(caserec:digits->int63->A->A).
+
+ Lemma recr_aux_eqn : forall n x, iszero x = false ->
+   recr_aux (S n) A case0 caserec x =
+   caserec (firstr x) (shiftr x) (recr_aux n A case0 caserec (shiftr x)).
+ Proof.
+ intros; simpl; rewrite H; auto.
+ Qed.
+
+ Lemma recr_aux_converges :
+  forall n p x, n <= size -> n <= p ->
+  recr_aux n A case0 caserec (nshiftr (size - n) x) =
+  recr_aux p A case0 caserec (nshiftr (size - n) x).
+ Proof.
+ induction n.
+ simpl; intros.
+ rewrite nshiftr_size; destruct p; simpl; auto.
+ intros.
+ destruct p.
+ inversion H0.
+ unfold recr_aux; fold recr_aux.
+ destruct (iszero (nshiftr (size - S n) x)); auto.
+ f_equal.
+ change (shiftr (nshiftr (size - S n) x)) with (nshiftr (S (size - S n)) x).
+ replace (S (size - S n))%nat with (size - n)%nat by omega.
+ apply IHn; auto with arith.
+ Qed.
+
+ Lemma recr_eqn : forall x, iszero x = false ->
+  recr A case0 caserec x =
+  caserec (firstr x) (shiftr x) (recr A case0 caserec (shiftr x)).
+ Proof.
+ intros.
+ unfold recr.
+ change x with (nshiftr (size - size) x).
+ rewrite (recr_aux_converges size (S size)); auto with arith.
+ rewrite recr_aux_eqn; auto.
+ Qed.
+
+ (** [recr] is usually equivalent to a variant [recrbis]
+     written without [iszero] check. *)
+
+ Fixpoint recrbis_aux (n:nat)(A:Type)(case0:A)(caserec:digits->int63->A->A)
+ (i:int63) : A :=
+  match n with
+  | O => case0
+  | S next =>
+      let si := shiftr i in
+      caserec (firstr i) si (recrbis_aux next A case0 caserec si)
+  end.
+
+ Definition recrbis := recrbis_aux size.
+
+ (* Useless [iszero] check, to stop simplification (did not manage to
+    restrict it using Arguments) *)
+ Fixpoint recrter_aux (n:nat)(A:Type)(case0:A)(caserec:digits->int63->A->A)
+ (i:int63) : A :=
+  match n with
+  | O => case0
+  | S next =>
+    if iszero i then
+      let si := shiftr i in
+      caserec (firstr i) si (recrter_aux next A case0 caserec si)
+    else
+      let si := shiftr i in
+      caserec (firstr i) si (recrter_aux next A case0 caserec si)
+  end.
+
+ Definition recrter := recrter_aux size.
+
+ Lemma recrbis_ter_aux n:
+   forall i, recrbis_aux n A case0 caserec i = recrter_aux n A case0 caserec i.
+ Proof.
+   induction n as [|n IHn]; simpl; auto.
+   intros; case (iszero _); rewrite IHn; auto.
+ Qed.
+
+ Lemma recrbis_ter i : recrbis A case0 caserec i = recrter A case0 caserec i.
+ Proof. apply recrbis_ter_aux. Qed.
+
+ Hypothesis case0_caserec : caserec D0 0 case0 = case0.
+
+ Lemma recrbis_aux_equiv : forall n x,
+   recrbis_aux n A case0 caserec x = recr_aux n A case0 caserec x.
+ Proof.
+ induction n; simpl; auto; intros.
+ case_eq (iszero x); intros; [ | f_equal; auto ].
+ rewrite (iszero_eq0 _ H); simpl; auto.
+ fold On.
+ replace (recrbis_aux n A case0 caserec 0) with case0; auto.
+ clear H IHn; induction n; simpl; fold On; congruence.
+ Qed.
+
+ Lemma recrbis_equiv : forall x,
+   recrbis A case0 caserec x = recr A case0 caserec x.
+ Proof.
+ intros; apply recrbis_aux_equiv; auto.
+ Qed.
+
+ End Recr.
+
+ (** * Incrementation *)
+
+ Section Incr.
+
+ (** Variant of [incr] via [recrbis] *)
+
+ Let Incr (b : digits) (si rec : int63) :=
+  match b with
+   | D0 => sneakl D1 si
+   | D1 => sneakl D0 rec
+  end.
+
+ Definition incrbis_aux n x := recrbis_aux n _ In Incr x.
+
+ Lemma incrbis_aux_equiv : forall x, incrbis_aux size x = incr x.
+ Proof.
+ unfold incr, recr, incrbis_aux; fold Incr; intros.
+ apply recrbis_aux_equiv; auto.
+ Qed.
+
+ (** Recursive equations satisfied by [incr] *)
+
+ Lemma incr_eqn1 :
+  forall x, firstr x = D0 -> incr x = twice_plus_one (shiftr x).
+ Proof.
+ intros.
+ case_eq (iszero x); intros.
+ rewrite (iszero_eq0 _ H0); simpl; auto.
+ unfold incr; rewrite recr_eqn; fold incr; auto.
+ rewrite H; auto.
+ Qed.
+
+ Lemma incr_eqn2 :
+  forall x, firstr x = D1 -> incr x = twice (incr (shiftr x)).
+ Proof.
+ intros.
+ case_eq (iszero x); intros.
+ rewrite (iszero_eq0 _ H0) in H; simpl in H; discriminate.
+ unfold incr; rewrite recr_eqn; fold incr; auto.
+ rewrite H; auto.
+ Qed.
+
+ Lemma incr_twice : forall x, incr (twice x) = twice_plus_one x.
+ Proof.
+ intros.
+ rewrite incr_eqn1; destruct x; simpl; auto.
+ Qed.
+
+ Lemma incr_twice_plus_one_firstl :
+  forall x, firstl x = D0 -> incr (twice_plus_one x) = twice (incr x).
+ Proof.
+ intros.
+ rewrite incr_eqn2; [ | destruct x; simpl; auto ].
+ f_equal; f_equal.
+ destruct x; simpl in *; rewrite H; auto.
+ Qed.
+
+ (** The previous result is actually true even without the
+     constraint on [firstl], but this is harder to prove
+     (see later). *)
+
+ End Incr.
+
+ (** * Conversion to [Z] : the [phi] function *)
+
+ Section Phi.
+
+ (** Variant of [phi] via [recrbis] *)
+
+ Let Phi := fun b (_:int63) =>
+       match b with D0 => Z.double | D1 => Z.succ_double end.
+
+ Definition phibis_aux n x := recrbis_aux n _ Z0 Phi x.
+
+ Lemma phibis_aux_equiv : forall x, phibis_aux size x = phi x.
+ Proof.
+ unfold phi, recr, phibis_aux; fold Phi; intros.
+ apply recrbis_aux_equiv; auto.
+ Qed.
+
+ (** Recursive equations satisfied by [phi] *)
+
+ Lemma phi_eqn1 : forall x, firstr x = D0 ->
+  phi x = Z.double (phi (shiftr x)).
+ Proof.
+ intros.
+ case_eq (iszero x); intros.
+ rewrite (iszero_eq0 _ H0); simpl; auto.
+ intros; unfold phi; rewrite recr_eqn; fold phi; auto.
+ rewrite H; auto.
+ Qed.
+
+ Lemma phi_eqn2 : forall x, firstr x = D1 ->
+  phi x = Z.succ_double (phi (shiftr x)).
+ Proof.
+ intros.
+ case_eq (iszero x); intros.
+ rewrite (iszero_eq0 _ H0) in H; simpl in H; discriminate.
+ intros; unfold phi; rewrite recr_eqn; fold phi; auto.
+ rewrite H; auto.
+ Qed.
+
+ Lemma phi_twice_firstl : forall x, firstl x = D0 ->
+  phi (twice x) = Z.double (phi x).
+ Proof.
+ intros.
+ rewrite phi_eqn1; auto; [ | destruct x; auto ].
+ f_equal; f_equal.
+ destruct x; simpl in *; rewrite H; auto.
+ Qed.
+
+ Lemma phi_twice_plus_one_firstl : forall x, firstl x = D0 ->
+  phi (twice_plus_one x) = Z.succ_double (phi x).
+ Proof.
+ intros.
+ rewrite phi_eqn2; auto; [ | destruct x; auto ].
+ f_equal; f_equal.
+ destruct x; simpl in *; rewrite H; auto.
+ Qed.
+
+ End Phi.
+
+ (** [phi x] is positive and lower than [2^63] *)
+
+ Lemma phibis_aux_pos : forall n x, (0 <= phibis_aux n x)%Z.
+ Proof.
+ induction n.
+ simpl; unfold phibis_aux; simpl; auto with zarith.
+ intros.
+ unfold phibis_aux, recrbis_aux; fold recrbis_aux;
+  fold (phibis_aux n (shiftr x)).
+ destruct (firstr x).
+ specialize IHn with (shiftr x); rewrite Z.double_spec; omega.
+ specialize IHn with (shiftr x); rewrite Z.succ_double_spec; omega.
+ Qed.
+
+ Lemma phibis_aux_bounded :
+  forall n x, n <= size ->
+  (phibis_aux n (nshiftr (size-n) x) < 2 ^ (Z.of_nat n))%Z.
+ Proof.
+ induction n.
+ simpl; unfold phibis_aux; simpl; auto with zarith.
+ intros.
+ unfold phibis_aux, recrbis_aux; fold recrbis_aux;
+  fold (phibis_aux n (shiftr (nshiftr (size - S n) x))).
+ assert (shiftr (nshiftr (size - S n) x) =  nshiftr (size-n) x).
+  replace (size - n)%nat with (S (size - (S n))) by omega.
+  simpl; auto.
+ rewrite H0.
+ assert (H1 : n <= size) by omega.
+ specialize (IHn x H1).
+ set (y:=phibis_aux n (nshiftr (size - n) x)) in *.
+ rewrite Nat2Z.inj_succ, Z.pow_succ_r; auto with zarith.
+ case_eq (firstr (nshiftr (size - S n) x)); intros.
+ rewrite Z.double_spec; auto with zarith.
+ rewrite Z.succ_double_spec; auto with zarith.
+ Qed.
+
+ Lemma phi_bounded  : forall x, (0 <= phi x < 2 ^ (Z.of_nat size))%Z.
+ Proof.
+ intros.
+ rewrite <- phibis_aux_equiv.
+ split.
+ apply phibis_aux_pos.
+ change x with (nshiftr (size-size) x).
+ apply phibis_aux_bounded; auto.
+ Qed.
+
+ Lemma phibis_aux_lowerbound :
+  forall n x, firstr (nshiftr n x) = D1 ->
+  (2 ^ Z.of_nat n <= phibis_aux (S n) x)%Z.
+ Proof.
+ induction n.
+ intros.
+ unfold nshiftr in H; simpl in *.
+ unfold phibis_aux, recrbis_aux.
+ rewrite H, Z.succ_double_spec; omega.
+
+ intros.
+ remember (S n) as m.
+ unfold phibis_aux, recrbis_aux; fold recrbis_aux;
+  fold (phibis_aux m (shiftr x)).
+ subst m.
+ rewrite Nat2Z.inj_succ, Z.pow_succ_r; auto with zarith.
+ assert (2^(Z.of_nat n) <= phibis_aux (S n) (shiftr x))%Z.
+  apply IHn.
+  rewrite <- nshiftr_S_tail; auto.
+ destruct (firstr x).
+ change (Z.double (phibis_aux (S n) (shiftr x))) with
+        (2*(phibis_aux (S n) (shiftr x)))%Z.
+ omega.
+ rewrite Z.succ_double_spec; omega.
+ Qed.
+
+ Lemma phi_lowerbound :
+  forall x, firstl x = D1 -> (2^(Z.of_nat (pred size)) <= phi x)%Z.
+ Proof.
+ intros.
+ generalize (phibis_aux_lowerbound (pred size) x).
+ rewrite <- firstl_firstr.
+ change (S (pred size)) with size; auto.
+ rewrite phibis_aux_equiv; auto.
+ Qed.
+
+ (** * Equivalence modulo [2^n] *)
+
+ Section EqShiftL.
+
+ (** After killing [n] bits at the left, are the numbers equal ?*)
+
+ Definition EqShiftL n x y :=
+  nshiftl n x = nshiftl n y.
+
+ Lemma EqShiftL_zero : forall x y, EqShiftL O x y <-> x = y.
+ Proof.
+ unfold EqShiftL; intros; unfold nshiftl; simpl; split; auto.
+ Qed.
+
+ Lemma EqShiftL_size : forall k x y, size<=k -> EqShiftL k x y.
+ Proof.
+ red; intros; rewrite 2 nshiftl_above_size; auto.
+ Qed.
+
+ Lemma EqShiftL_le : forall k k' x y, k <= k' ->
+   EqShiftL k x y -> EqShiftL k' x y.
+ Proof.
+ unfold EqShiftL; intros.
+ replace k' with ((k'-k)+k)%nat by omega.
+ remember (k'-k)%nat as n.
+ clear Heqn H k'.
+ induction n; simpl; auto.
+ rewrite 2 nshiftl_S; f_equal; auto.
+ Qed.
+
+ Lemma EqShiftL_firstr : forall k x y, k < size ->
+  EqShiftL k x y -> firstr x = firstr y.
+ Proof.
+ intros.
+ rewrite 2 firstr_firstl.
+ f_equal.
+ apply EqShiftL_le with k; auto.
+ unfold size.
+ auto with arith.
+ Qed.
+
+ Lemma EqShiftL_twice : forall k x y,
+  EqShiftL k (twice x) (twice y) <-> EqShiftL (S k) x y.
+ Proof.
+ intros; unfold EqShiftL.
+ rewrite 2 nshiftl_S_tail; split; auto.
+ Qed.
+
+ (** * From int63 to list of digits. *)
+
+ (** Lower (=rightmost) bits comes first. *)
+
+ Definition i2l := recrbis _ nil (fun d _ rec => d::rec).
+
+ Lemma i2l_length : forall x, length (i2l x) = size.
+ Proof.
+ intros; reflexivity.
+ Qed.
+
+ Fixpoint lshiftl l x :=
+   match l with
+     | nil => x
+     | d::l => sneakl d (lshiftl l x)
+   end.
+
+ Definition l2i l := lshiftl l On.
+
+ Lemma l2i_i2l : forall x, l2i (i2l x) = x.
+ Proof.
+ destruct x; compute; auto.
+ Qed.
+
+ Lemma i2l_sneakr : forall x d,
+   i2l (sneakr d x) = tail (i2l x) ++ d::nil.
+ Proof.
+ destruct x; compute; auto.
+ Qed.
+
+ Lemma i2l_sneakl : forall x d,
+   i2l (sneakl d x) = d :: removelast (i2l x).
+ Proof.
+ destruct x; compute; auto.
+ Qed.
+
+ Lemma i2l_l2i : forall l, length l = size ->
+  i2l (l2i l) = l.
+ Proof.
+ repeat (destruct l as [ |? l]; [intros; discriminate | ]).
+ destruct l; [ | intros; discriminate].
+ intros _; compute; auto.
+ Qed.
+
+ Fixpoint cstlist (A:Type)(a:A) n :=
+  match n with
+   | O => nil
+   | S n => a::cstlist _ a n
+  end.
+
+ Lemma i2l_nshiftl : forall n x, n<=size ->
+  i2l (nshiftl n x) = cstlist _ D0 n ++ firstn (size-n) (i2l x).
+ Proof.
+ induction n.
+ intros.
+ assert (firstn (size-0) (i2l x) = i2l x).
+  rewrite <- minus_n_O, <- (i2l_length x).
+  induction (i2l x); simpl; f_equal; auto.
+ rewrite H0; clear H0.
+ reflexivity.
+
+ intros.
+ rewrite nshiftl_S.
+ unfold shiftl; rewrite i2l_sneakl.
+ simpl cstlist.
+ rewrite <- app_comm_cons; f_equal.
+ rewrite IHn; [ | omega].
+ rewrite removelast_app.
+ f_equal.
+ replace (size-n)%nat with (S (size - S n))%nat by omega.
+ rewrite removelast_firstn; auto.
+ rewrite i2l_length; omega.
+ generalize (firstn_length (size-n) (i2l x)).
+ rewrite i2l_length.
+ intros H0 H1; rewrite H1 in H0.
+ rewrite min_l in H0 by omega.
+ simpl length in H0.
+ omega.
+ Qed.
+
+ (** [i2l] can be used to define a relation equivalent to [EqShiftL] *)
+
+ Lemma EqShiftL_i2l : forall k x y,
+   EqShiftL k x y  <-> firstn (size-k) (i2l x) = firstn (size-k) (i2l y).
+ Proof.
+ intros.
+ destruct (le_lt_dec size k).
+ split; intros.
+ replace (size-k)%nat with O by omega.
+ unfold firstn; auto.
+ apply EqShiftL_size; auto.
+
+ unfold EqShiftL.
+ assert (k <= size) by omega.
+ split; intros.
+ assert (i2l (nshiftl k x) = i2l (nshiftl k y)) by (f_equal; auto).
+ rewrite 2 i2l_nshiftl in H1; auto.
+ eapply app_inv_head; eauto.
+ assert (i2l (nshiftl k x) = i2l (nshiftl k y)).
+  rewrite 2 i2l_nshiftl; auto.
+  f_equal; auto.
+ rewrite <- (l2i_i2l (nshiftl k x)), <- (l2i_i2l (nshiftl k y)).
+ f_equal; auto.
+ Qed.
+
+ (** This equivalence allows to prove easily the following delicate
+     result *)
+
+ Lemma EqShiftL_twice_plus_one : forall k x y,
+  EqShiftL k (twice_plus_one x) (twice_plus_one y) <-> EqShiftL (S k) x y.
+ Proof.
+ intros.
+ destruct (le_lt_dec size k).
+ split; intros; apply EqShiftL_size; auto.
+
+ rewrite 2 EqShiftL_i2l.
+ unfold twice_plus_one.
+ rewrite 2 i2l_sneakl.
+ replace (size-k)%nat with (S (size - S k))%nat by omega.
+ remember (size - S k)%nat as n.
+ remember (i2l x) as lx.
+ remember (i2l y) as ly.
+ simpl.
+ rewrite 2 firstn_removelast.
+ split; intros.
+ injection H; auto.
+ f_equal; auto.
+ subst ly n; rewrite i2l_length; omega.
+ subst lx n; rewrite i2l_length; omega.
+ Qed.
+
+ Lemma EqShiftL_shiftr : forall k x y, EqShiftL k x y ->
+  EqShiftL (S k) (shiftr x) (shiftr y).
+ Proof.
+ intros.
+ destruct (le_lt_dec size (S k)).
+ apply EqShiftL_size; auto.
+ case_eq (firstr x); intros.
+ rewrite <- EqShiftL_twice.
+ unfold twice; rewrite <- H0.
+ rewrite <- sneakl_shiftr.
+ rewrite (EqShiftL_firstr k x y); auto.
+ rewrite <- sneakl_shiftr; auto.
+ omega.
+ rewrite <- EqShiftL_twice_plus_one.
+ unfold twice_plus_one; rewrite <- H0.
+ rewrite <- sneakl_shiftr.
+ rewrite (EqShiftL_firstr k x y); auto.
+ rewrite <- sneakl_shiftr; auto.
+ omega.
+ Qed.
+
+ Lemma EqShiftL_incrbis : forall n k x y, n<=size ->
+  (n+k=S size)%nat ->
+  EqShiftL k x y ->
+  EqShiftL k (incrbis_aux n x) (incrbis_aux n y).
+ Proof.
+ induction n; simpl; intros.
+ red; auto.
+ destruct (eq_nat_dec k size).
+  subst k; apply EqShiftL_size; auto.
+ unfold incrbis_aux; simpl;
+  fold (incrbis_aux n (shiftr x)); fold (incrbis_aux n (shiftr y)).
+
+ rewrite (EqShiftL_firstr k x y); auto; try omega.
+ case_eq (firstr y); intros.
+ rewrite EqShiftL_twice_plus_one.
+ apply EqShiftL_shiftr; auto.
+
+ rewrite EqShiftL_twice.
+ apply IHn; try omega.
+ apply EqShiftL_shiftr; auto.
+ Qed.
+
+ Lemma EqShiftL_incr : forall x y,
+  EqShiftL 1 x y -> EqShiftL 1 (incr x) (incr y).
+ Proof.
+ intros.
+ rewrite <- 2 incrbis_aux_equiv.
+ apply EqShiftL_incrbis; auto.
+ Qed.
+
+ End EqShiftL.
+
+ (** * More equations about [incr] *)
+
+ Lemma incr_twice_plus_one :
+  forall x, incr (twice_plus_one x) = twice (incr x).
+ Proof.
+ intros.
+ rewrite incr_eqn2; [ | destruct x; simpl; auto].
+ apply EqShiftL_incr.
+ red; destruct x; simpl; auto.
+ Qed.
+
+ Lemma incr_firstr : forall x, firstr (incr x) <> firstr x.
+ Proof.
+ intros.
+ case_eq (firstr x); intros.
+ rewrite incr_eqn1; auto.
+ destruct (shiftr x); simpl; discriminate.
+ rewrite incr_eqn2; auto.
+ destruct (incr (shiftr x)); simpl; discriminate.
+ Qed.
+
+ Lemma incr_inv : forall x y,
+  incr x = twice_plus_one y -> x = twice y.
+ Proof.
+ intros.
+ case_eq (iszero x); intros.
+ rewrite (iszero_eq0 _ H0) in *; simpl in *.
+ change (incr 0) with 1 in H.
+ symmetry; rewrite twice_zero; auto.
+ case_eq (firstr x); intros.
+ rewrite incr_eqn1 in H; auto.
+ clear H0; destruct x; destruct y; simpl in *.
+ injection H; intros; subst; auto.
+ elim (incr_firstr x).
+ rewrite H1, H; destruct y; simpl; auto.
+ Qed.
+
+ (** * Conversion from [Z] : the [phi_inv] function *)
+
+ (** First, recursive equations *)
+
+ Lemma phi_inv_double_plus_one : forall z,
+   phi_inv (Z.succ_double z) = twice_plus_one (phi_inv z).
+ Proof.
+ destruct z; simpl; auto.
+ induction p; simpl.
+ rewrite 2 incr_twice; auto.
+ rewrite incr_twice, incr_twice_plus_one.
+ f_equal.
+ apply incr_inv; auto.
+ auto.
+ Qed.
+
+ Lemma phi_inv_double : forall z,
+   phi_inv (Z.double z) = twice (phi_inv z).
+ Proof.
+ destruct z; simpl; auto.
+ rewrite incr_twice_plus_one; auto.
+ Qed.
+
+ Lemma phi_inv_incr : forall z,
+  phi_inv (Z.succ z) = incr (phi_inv z).
+ Proof.
+ destruct z.
+ simpl; auto.
+ simpl; auto.
+ induction p; simpl; auto.
+ rewrite <- Pos.add_1_r, IHp, incr_twice_plus_one; auto.
+ rewrite incr_twice; auto.
+ simpl; auto.
+ destruct p; simpl; auto.
+ rewrite incr_twice; auto.
+ f_equal.
+ rewrite incr_twice_plus_one; auto.
+ induction p; simpl; auto.
+ rewrite incr_twice; auto.
+ f_equal.
+ rewrite incr_twice_plus_one; auto.
+ Qed.
+
+ (** [phi_inv o inv], the always-exact and easy-to-prove trip :
+     from int63 to Z and then back to int63. *)
+
+ Lemma phi_inv_phi_aux :
+  forall n x, n <= size ->
+   phi_inv (phibis_aux n (nshiftr (size-n) x)) =
+   nshiftr (size-n) x.
+ Proof.
+ induction n.
+ intros; simpl.
+ rewrite nshiftr_size; auto.
+ intros.
+ unfold phibis_aux, recrbis_aux; fold recrbis_aux;
+  fold (phibis_aux n (shiftr (nshiftr (size-S n) x))).
+ assert (shiftr (nshiftr (size - S n) x) = nshiftr (size-n) x).
+  replace (size - n)%nat with (S (size - (S n))); auto; omega.
+ rewrite H0.
+ case_eq (firstr (nshiftr (size - S n) x)); intros.
+
+ rewrite phi_inv_double.
+ rewrite IHn by omega.
+ rewrite <- H0.
+ remember (nshiftr (size - S n) x) as y.
+ destruct y; simpl in H1; rewrite H1; auto.
+
+ rewrite phi_inv_double_plus_one.
+ rewrite IHn by omega.
+ rewrite <- H0.
+ remember (nshiftr (size - S n) x) as y.
+ destruct y; simpl in H1; rewrite H1; auto.
+ Qed.
+
+ Lemma phi_inv_phi : forall x, phi_inv (phi x) = x.
+ Proof.
+ intros.
+ rewrite <- phibis_aux_equiv.
+ replace x with (nshiftr (size - size) x) by auto.
+ apply phi_inv_phi_aux; auto.
+ Qed.
+
+ (** The other composition [phi o phi_inv] is harder to prove correct.
+     In particular, an overflow can happen, so a modulo is needed.
+     For the moment, we proceed via several steps, the first one
+     being a detour to [positive_to_in63]. *)
+
+ (** * [positive_to_int63] *)
+
+ (** A variant of [p2i] with [twice] and [twice_plus_one] instead of
+     [2*i] and [2*i+1] *)
+
+ Fixpoint p2ibis n p : (N*int63)%type :=
+  match n with
+    | O => (Npos p, On)
+    | S n => match p with
+               | xO p => let (r,i) := p2ibis n p in (r, twice i)
+               | xI p => let (r,i) := p2ibis n p in (r, twice_plus_one i)
+               | xH => (N0, In)
+             end
+  end.
+
+ Lemma p2ibis_bounded : forall n p,
+  nshiftr n (snd (p2ibis n p)) = 0.
+ Proof.
+ induction n.
+ simpl; intros; auto.
+ simpl; intros.
+ destruct p; simpl.
+
+ specialize IHn with p.
+ destruct (p2ibis n p); simpl in *.
+ rewrite nshiftr_S_tail.
+ destruct (le_lt_dec size n).
+ rewrite nshiftr_above_size; auto.
+ assert (H:=nshiftr_0_firstl _ _ l IHn).
+ replace (shiftr (twice_plus_one i)) with i; auto.
+ destruct i; simpl in *; rewrite H; auto.
+
+ specialize IHn with p.
+ destruct (p2ibis n p); simpl in *.
+ rewrite nshiftr_S_tail.
+ destruct (le_lt_dec size n).
+ rewrite nshiftr_above_size; auto.
+ assert (H:=nshiftr_0_firstl _ _ l IHn).
+ replace (shiftr (twice i)) with i; auto.
+ destruct i; simpl in *; rewrite H; auto.
+
+ rewrite nshiftr_S_tail; auto.
+ replace (shiftr In) with 0; auto.
+ apply nshiftr_n_0.
+ Qed.
+
+ Local Open Scope Z_scope.
+
+ Lemma p2ibis_spec : forall n p, (n<=size)%nat ->
+    Zpos p = (Z.of_N (fst (p2ibis n p)))*2^(Z.of_nat n) +
+             phi (snd (p2ibis n p)).
+ Proof.
+ induction n; intros.
+ simpl; rewrite Pos.mul_1_r; auto.
+ replace (2^(Z.of_nat (S n)))%Z with (2*2^(Z.of_nat n))%Z by
+  (rewrite <- Z.pow_succ_r, <- Zpos_P_of_succ_nat;
+   auto with zarith).
+ rewrite (Z.mul_comm 2).
+ assert (n<=size)%nat by omega.
+ destruct p; simpl; [ | | auto];
+  specialize (IHn p H0);
+  generalize (p2ibis_bounded n p);
+  destruct (p2ibis n p) as (r,i); simpl in *; intros.
+
+ change (Zpos p~1) with (2*Zpos p + 1)%Z.
+ rewrite phi_twice_plus_one_firstl, Z.succ_double_spec.
+ rewrite IHn; ring.
+ apply (nshiftr_0_firstl n); auto; try omega.
+
+ change (Zpos p~0) with (2*Zpos p)%Z.
+ rewrite phi_twice_firstl.
+ change (Z.double (phi i)) with (2*(phi i))%Z.
+ rewrite IHn; ring.
+ apply (nshiftr_0_firstl n); auto; try omega.
+ Qed.
+
+ (** We now prove that this [p2ibis] is related to [phi_inv_positive] *)
+
+ Lemma phi_inv_positive_p2ibis : forall n p, (n<=size)%nat ->
+  EqShiftL (size-n) (phi_inv_positive p) (snd (p2ibis n p)).
+ Proof.
+ induction n.
+ intros.
+ apply EqShiftL_size; auto.
+ intros.
+ simpl p2ibis; destruct p; [ | | red; auto];
+  specialize IHn with p;
+  destruct (p2ibis n p); simpl snd in *; simpl phi_inv_positive;
+  rewrite ?EqShiftL_twice_plus_one, ?EqShiftL_twice;
+  replace (S (size - S n))%nat with (size - n)%nat by omega;
+  apply IHn; omega.
+ Qed.
+
+ (** This gives the expected result about [phi o phi_inv], at least
+     for the positive case. *)
+
+ Lemma phi_phi_inv_positive : forall p,
+  phi (phi_inv_positive p) = (Zpos p) mod (2^(Z.of_nat size)).
+ Proof.
+ intros.
+ replace (phi_inv_positive p) with (snd (p2ibis size p)).
+ rewrite (p2ibis_spec size p) by auto.
+ rewrite Z.add_comm, Z_mod_plus.
+ symmetry; apply Zmod_small.
+ apply phi_bounded.
+ auto with zarith.
+ symmetry.
+ rewrite <- EqShiftL_zero.
+ apply (phi_inv_positive_p2ibis size p); auto.
+ Qed.
+
+ (** Moreover, [p2ibis] is also related with [p2i] and hence with
+    [positive_to_int63]. *)
+
+ Lemma double_twice_firstl : forall x, firstl x = D0 ->
+  (Twon*x = twice x)%int.
+ Proof.
+ intros.
+ unfold mul63.
+ rewrite <- Z.double_spec, <- phi_twice_firstl, phi_inv_phi; auto.
+ Qed.
+
+ Lemma double_twice_plus_one_firstl : forall x, firstl x = D0 ->
+  (Twon*x+In = twice_plus_one x)%int.
+ Proof.
+ intros.
+ rewrite double_twice_firstl; auto.
+ unfold add63.
+ rewrite phi_twice_firstl, <- Z.succ_double_spec,
+   <- phi_twice_plus_one_firstl, phi_inv_phi; auto.
+ Qed.
+
+ Lemma p2i_p2ibis : forall n p, (n<=size)%nat ->
+  p2i n p = p2ibis n p.
+ Proof.
+ induction n; simpl; auto; intros.
+ destruct p; auto; specialize IHn with p;
+  generalize (p2ibis_bounded n p);
+  rewrite IHn; try omega; destruct (p2ibis n p); simpl; intros;
+  f_equal; auto.
+ apply double_twice_plus_one_firstl.
+ apply (nshiftr_0_firstl n); auto; omega.
+ apply double_twice_firstl.
+ apply (nshiftr_0_firstl n); auto; omega.
+ Qed.
+
+ Lemma positive_to_int63_phi_inv_positive : forall p,
+   snd (positive_to_int63 p) = phi_inv_positive p.
+ Proof.
+ intros; unfold positive_to_int63.
+ rewrite p2i_p2ibis; auto.
+ symmetry.
+ rewrite <- EqShiftL_zero.
+ apply (phi_inv_positive_p2ibis size); auto.
+ Qed.
+
+ Lemma positive_to_int63_spec : forall p,
+    Zpos p = (Z.of_N (fst (positive_to_int63 p)))*2^(Z.of_nat size) +
+               phi (snd (positive_to_int63 p)).
+ Proof.
+ unfold positive_to_int63.
+ intros; rewrite p2i_p2ibis; auto.
+ apply p2ibis_spec; auto.
+ Qed.
+
+ (** Thanks to the result about [phi o phi_inv_positive], we can
+     now establish easily the most general results about
+     [phi o twice] and so one. *)
+
+ Lemma phi_twice : forall x,
+   phi (twice x) = (Z.double (phi x)) mod 2^(Z.of_nat size).
+ Proof.
+ intros.
+ pattern x at 1; rewrite <- (phi_inv_phi x).
+ rewrite <- phi_inv_double.
+ assert (0 <= Z.double (phi x)).
+  rewrite Z.double_spec; generalize (phi_bounded x); omega.
+ destruct (Z.double (phi x)).
+ simpl; auto.
+ apply phi_phi_inv_positive.
+ compute in H; elim H; auto.
+ Qed.
+
+ Lemma phi_twice_plus_one : forall x,
+   phi (twice_plus_one x) = (Z.succ_double (phi x)) mod 2^(Z.of_nat size).
+ Proof.
+ intros.
+ pattern x at 1; rewrite <- (phi_inv_phi x).
+ rewrite <- phi_inv_double_plus_one.
+ assert (0 <= Z.succ_double (phi x)).
+  rewrite Z.succ_double_spec; generalize (phi_bounded x); omega.
+ destruct (Z.succ_double (phi x)).
+ simpl; auto.
+ apply phi_phi_inv_positive.
+ compute in H; elim H; auto.
+ Qed.
+
+ Lemma phi_incr : forall x,
+   phi (incr x) = (Z.succ (phi x)) mod 2^(Z.of_nat size).
+ Proof.
+ intros.
+ pattern x at 1; rewrite <- (phi_inv_phi x).
+ rewrite <- phi_inv_incr.
+ assert (0 <= Z.succ (phi x)).
+  change (Z.succ (phi x)) with ((phi x)+1)%Z;
+   generalize (phi_bounded x); omega.
+ destruct (Z.succ (phi x)).
+ simpl; auto.
+ apply phi_phi_inv_positive.
+ compute in H; elim H; auto.
+ Qed.
+
+ (** With the previous results, we can deal with [phi o phi_inv] even
+    in the negative case *)
+
+ Lemma phi_phi_inv_negative :
+  forall p, phi (incr (complement_negative p)) = (Zneg p) mod 2^(Z.of_nat size).
+ Proof.
+ induction p.
+
+ simpl complement_negative.
+ rewrite phi_incr in IHp.
+ rewrite incr_twice, phi_twice_plus_one.
+ remember (phi (complement_negative p)) as q.
+ rewrite Z.succ_double_spec.
+ replace (2*q+1) with (2*(Z.succ q)-1) by omega.
+ rewrite <- Zminus_mod_idemp_l, <- Zmult_mod_idemp_r, IHp.
+ rewrite Zmult_mod_idemp_r, Zminus_mod_idemp_l; auto with zarith.
+
+ simpl complement_negative.
+ rewrite incr_twice_plus_one, phi_twice.
+ remember (phi (incr (complement_negative p))) as q.
+ rewrite Z.double_spec, IHp, Zmult_mod_idemp_r; auto with zarith.
+
+ simpl; auto.
+ Qed.
+
+ Lemma phi_phi_inv :
+  forall z, phi (phi_inv z) = z mod 2 ^ (Z.of_nat size).
+ Proof.
+ destruct z.
+ simpl; auto.
+ apply phi_phi_inv_positive.
+ apply phi_phi_inv_negative.
+ Qed.
+
+End Basics.
+
+Definition zdigits := Eval vm_compute in (phi_inv 63).
+Notation "63" := zdigits : int63_scope.
+
+Instance int63_ops : ZnZ.Ops int63 :=
+{
+ digits      := 63%positive; (* number of digits *)
+ zdigits     := 63; (* number of digits *)
+ to_Z        := phi; (* conversion to Z *)
+ of_pos      := positive_to_int63; (* positive -> N*int63 :  p => N,i
+                                      where p = N*2^63+phi i *)
+ head0       := head063;  (* number of head 0 *)
+ tail0       := tail063;  (* number of tail 0 *)
+ zero        := 0;
+ one         := 1;
+ minus_one   := Tn; (* 2^63 - 1 *)
+ compare     := compare63;
+ eq0         := fun i => match i ?= 0 with Eq => true | _ => false end;
+ opp_c       := fun i => 0 -c i;
+ opp         := opp63;
+ opp_carry   := fun i => 0-i-1;
+ succ_c      := fun i => i +c 1;
+ add_c       := add63c;
+ add_carry_c := add63carryc;
+ succ        := fun i => i + 1;
+ add         := add63;
+ add_carry   := fun i j => i + j + 1;
+ pred_c      := fun i => i -c 1;
+ sub_c       := sub63c;
+ sub_carry_c := sub63carryc;
+ pred        := fun i => i - 1;
+ sub         := sub63;
+ sub_carry   := fun i j => i - j - 1;
+ mul_c       := mul63c;
+ mul         := mul63;
+ square_c    := fun x => x *c x;
+ div21       := div6321;
+ div_gt      := div63; (* this is supposed to be the special case of
+                         division a/b where a > b *)
+ div         := div63;
+ modulo_gt   := fun i j => let (_,r) := i/j in r;
+ modulo      := fun i j => let (_,r) := i/j in r;
+ gcd_gt      := gcd63;
+ gcd         := gcd63;
+ add_mul_div := addmuldiv63;
+ pos_mod     := (* modulo 2^p *)
+  fun p i =>
+  match p ?= 63 with
+    | Lt => addmuldiv63 p 0 (addmuldiv63 (63-p) i 0)
+    | _ => i
+  end;
+ is_even      :=
+  fun i => let (_,r) := i/2 in
+  match r ?= 0 with Eq => true | _ => false end;
+ sqrt2       := sqrt632;
+ sqrt        := sqrt63
+}.
+
+Section Int63_Specs.
+
+ Local Open Scope Z_scope.
+
+ Notation "[| x |]" := (phi x)  (at level 0, x at level 99).
+
+ Local Notation wB := (2 ^ (Z.of_nat size)).
+
+ Lemma wB_pos : wB > 0.
+ Proof.
+  auto with zarith.
+ Qed.
+
+ Notation "[+| c |]" :=
+   (interp_carry 1 wB phi c)  (at level 0, x at level 99).
+
+ Notation "[-| c |]" :=
+   (interp_carry (-1) wB phi c)  (at level 0, x at level 99).
+
+ Notation "[|| x ||]" :=
+   (zn2z_to_Z wB phi x)  (at level 0, x at level 99).
+
+ Lemma spec_zdigits : [| 63 |] = 63.
+ Proof.
+  reflexivity.
+ Qed.
+
+ Lemma spec_more_than_1_digit: 1 < 63.
+ Proof.
+  auto with zarith.
+ Qed.
+
+ Lemma spec_0   : [| 0 |] = 0.
+ Proof.
+  reflexivity.
+ Qed.
+
+ Lemma spec_1   : [| 1 |] = 1.
+ Proof.
+  reflexivity.
+ Qed.
+
+ Lemma spec_m1 : [| Tn |] = wB - 1.
+ Proof.
+  reflexivity.
+ Qed.
+
+ Lemma spec_compare : forall x y,
+   (x ?= y)%int = ([|x|] ?= [|y|]).
+ Proof. reflexivity. Qed.
+
+ (** Addition *)
+
+ Lemma spec_add_c  : forall x y, [+|add63c x y|] = [|x|] + [|y|].
+ Proof.
+ intros; unfold add63c, add63, interp_carry; rewrite phi_phi_inv.
+ generalize (phi_bounded x)(phi_bounded y); intros.
+ set (X:=[|x|]) in *; set (Y:=[|y|]) in *; clearbody X Y.
+
+ assert ((X+Y) mod wB ?= X+Y <> Eq -> [+|C1 (phi_inv (X+Y))|] = X+Y).
+  unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros.
+  destruct (Z_lt_le_dec (X+Y) wB).
+  contradict H1; auto using Zmod_small with zarith.
+  rewrite <- (Z_mod_plus_full (X+Y) (-1) wB).
+  rewrite Zmod_small; romega.
+
+ generalize (Z.compare_eq ((X+Y) mod wB) (X+Y)); intros Heq.
+ destruct Z.compare; intros;
+  [ rewrite phi_phi_inv; auto | now apply H1 | now apply H1].
+ Qed.
+
+ Lemma spec_succ_c : forall x, [+|add63c x 1|] = [|x|] + 1.
+ Proof.
+ intros; apply spec_add_c.
+ Qed.
+
+ Lemma spec_add_carry_c : forall x y, [+|add63carryc x y|] = [|x|] + [|y|] + 1.
+ Proof.
+ intros.
+ unfold add63carryc, interp_carry; rewrite phi_phi_inv.
+ generalize (phi_bounded x)(phi_bounded y); intros.
+ set (X:=[|x|]) in *; set (Y:=[|y|]) in *; clearbody X Y.
+
+ assert ((X+Y+1) mod wB ?= X+Y+1 <> Eq -> [+|C1 (phi_inv (X+Y+1))|] = X+Y+1).
+  unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros.
+  destruct (Z_lt_le_dec (X+Y+1) wB).
+  contradict H1; auto using Zmod_small with zarith.
+  rewrite <- (Z_mod_plus_full (X+Y+1) (-1) wB).
+  rewrite Zmod_small; romega.
+
+ generalize (Z.compare_eq ((X+Y+1) mod wB) (X+Y+1)); intros Heq.
+ destruct Z.compare; intros;
+  [ rewrite phi_phi_inv; auto | now apply H1 | now apply H1].
+ Qed.
+
+ Lemma spec_add : forall x y, [|x+y|] = ([|x|] + [|y|]) mod wB.
+ Proof.
+ intros; apply phi_phi_inv.
+ Qed.
+
+ Lemma spec_add_carry :
+	 forall x y, [|x+y+1|] = ([|x|] + [|y|] + 1) mod wB.
+ Proof.
+ unfold add63; intros.
+ repeat rewrite phi_phi_inv.
+ apply Zplus_mod_idemp_l.
+ Qed.
+
+ Lemma spec_succ : forall x, [|x+1|] = ([|x|] + 1) mod wB.
+ Proof.
+ intros; rewrite <- spec_1; apply spec_add.
+ Qed.
+
+ (** Substraction *)
+
+ Lemma spec_sub_c : forall x y, [-|sub63c x y|] = [|x|] - [|y|].
+ Proof.
+ unfold sub63c, sub63, interp_carry; intros.
+ rewrite phi_phi_inv.
+ generalize (phi_bounded x)(phi_bounded y); intros.
+ set (X:=[|x|]) in *; set (Y:=[|y|]) in *; clearbody X Y.
+
+ assert ((X-Y) mod wB ?= X-Y <> Eq -> [-|C1 (phi_inv (X-Y))|] = X-Y).
+  unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros.
+  destruct (Z_lt_le_dec (X-Y) 0).
+  rewrite <- (Z_mod_plus_full (X-Y) 1 wB).
+  rewrite Zmod_small; romega.
+  contradict H1; apply Zmod_small; romega.
+
+ generalize (Z.compare_eq ((X-Y) mod wB) (X-Y)); intros Heq.
+ destruct Z.compare; intros;
+  [ rewrite phi_phi_inv; auto | now apply H1 | now apply H1].
+ Qed.
+
+ Lemma spec_sub_carry_c : forall x y, [-|sub63carryc x y|] = [|x|] - [|y|] - 1.
+ Proof.
+ unfold sub63carryc, sub63, interp_carry; intros.
+ rewrite phi_phi_inv.
+ generalize (phi_bounded x)(phi_bounded y); intros.
+ set (X:=[|x|]) in *; set (Y:=[|y|]) in *; clearbody X Y.
+
+ assert ((X-Y-1) mod wB ?= X-Y-1 <> Eq -> [-|C1 (phi_inv (X-Y-1))|] = X-Y-1).
+  unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros.
+  destruct (Z_lt_le_dec (X-Y-1) 0).
+  rewrite <- (Z_mod_plus_full (X-Y-1) 1 wB).
+  rewrite Zmod_small; romega.
+  contradict H1; apply Zmod_small; romega.
+
+ generalize (Z.compare_eq ((X-Y-1) mod wB) (X-Y-1)); intros Heq.
+ destruct Z.compare; intros;
+  [ rewrite phi_phi_inv; auto | now apply H1 | now apply H1].
+ Qed.
+
+ Lemma spec_sub : forall x y, [|x-y|] = ([|x|] - [|y|]) mod wB.
+ Proof.
+ intros; apply phi_phi_inv.
+ Qed.
+
+ Lemma spec_sub_carry :
+   forall x y, [|x-y-1|] = ([|x|] - [|y|] - 1) mod wB.
+ Proof.
+ unfold sub63; intros.
+ repeat rewrite phi_phi_inv.
+ apply Zminus_mod_idemp_l.
+ Qed.
+
+ Lemma spec_opp_c : forall x, [-|sub63c 0 x|] = -[|x|].
+ Proof.
+ intros; apply spec_sub_c.
+ Qed.
+
+ Lemma spec_opp : forall x, [|0 - x|] = (-[|x|]) mod wB.
+ Proof.
+ intros; apply phi_phi_inv.
+ Qed.
+
+ Lemma spec_opp_carry : forall x, [|0 - x - 1|] = wB - [|x|] - 1.
+ Proof.
+ unfold sub63; intros.
+ repeat rewrite phi_phi_inv.
+ change [|1|] with 1; change [|0|] with 0.
+ rewrite <- (Z_mod_plus_full (0-[|x|]) 1 wB).
+ rewrite Zminus_mod_idemp_l.
+ rewrite Zmod_small; generalize (phi_bounded x); romega.
+ Qed.
+
+ Lemma spec_pred_c : forall x, [-|sub63c x 1|] = [|x|] - 1.
+ Proof.
+ intros; apply spec_sub_c.
+ Qed.
+
+ Lemma spec_pred : forall x, [|x-1|] = ([|x|] - 1) mod wB.
+ Proof.
+ intros; apply spec_sub.
+ Qed.
+
+ (** Multiplication *)
+
+ Lemma phi2_phi_inv2 : forall x, [||phi_inv2 x||] = x mod (wB^2).
+ Proof.
+ assert (forall z, (z / wB) mod wB * wB + z mod wB = z mod wB ^ 2).
+  intros.
+  assert ((z/wB) mod wB = z/wB - (z/wB/wB)*wB).
+   rewrite (Z_div_mod_eq (z/wB) wB wB_pos) at 2; ring.
+  assert (z mod wB = z - (z/wB)*wB).
+   rewrite (Z_div_mod_eq z wB wB_pos) at 2; ring.
+  rewrite H.
+  rewrite H0 at 1.
+  ring_simplify.
+  rewrite Zdiv_Zdiv; auto with zarith.
+  rewrite (Z_div_mod_eq z (wB*wB)) at 2; auto with zarith.
+  change (wB*wB) with (wB^2); ring.
+
+ unfold phi_inv2.
+ destruct x; unfold zn2z_to_Z; rewrite ?phi_phi_inv;
+  change base with wB; auto.
+ Qed.
+
+ Lemma spec_mul_c : forall x y, [|| mul63c x y ||] = [|x|] * [|y|].
+ Proof.
+ unfold mul63c; intros.
+ rewrite phi2_phi_inv2.
+ apply Zmod_small.
+ generalize (phi_bounded x)(phi_bounded y); intros.
+ change (wB^2) with (wB * wB).
+ auto using Z.mul_lt_mono_nonneg with zarith.
+ Qed.
+
+ Lemma spec_mul : forall x y, [|x*y|] = ([|x|] * [|y|]) mod wB.
+ Proof.
+ intros; apply phi_phi_inv.
+ Qed.
+
+ Lemma spec_square_c : forall x, [|| mul63c x x ||] = [|x|] * [|x|].
+ Proof.
+ intros; apply spec_mul_c.
+ Qed.
+
+ (** Division *)
+
+ Lemma spec_div21 : forall a1 a2 b,
+      wB/2 <= [|b|] ->
+      [|a1|] < [|b|] ->
+      let (q,r) := div6321 a1 a2 b in
+      [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\
+      0 <= [|r|] < [|b|].
+ Proof.
+ unfold div6321; intros.
+ generalize (phi_bounded a1)(phi_bounded a2)(phi_bounded b); intros.
+ assert ([|b|]>0) by (auto with zarith).
+ generalize (Z_div_mod (phi2 a1 a2) [|b|] H4) (Z_div_pos (phi2 a1 a2) [|b|] H4).
+ unfold Z.div; destruct (Z.div_eucl (phi2 a1 a2) [|b|]); simpl.
+ rewrite ?phi_phi_inv.
+ destruct 1; intros.
+ unfold phi2 in *.
+ change base with wB; change base with wB in H5.
+ change (Z.pow_pos 2 63) with wB; change (Z.pow_pos 2 63) with wB in H.
+ rewrite H5, Z.mul_comm.
+ replace (z0 mod wB) with z0 by (symmetry; apply Zmod_small; omega).
+ replace (z mod wB) with z; auto with zarith.
+  symmetry; apply Zmod_small.
+  split.
+  apply H7; change base with wB; auto with zarith.
+  apply Z.mul_lt_mono_pos_r with [|b|]; [omega| ].
+  rewrite Z.mul_comm.
+  apply Z.le_lt_trans with ([|b|]*z+z0); [omega| ].
+  rewrite <- H5.
+  apply Z.le_lt_trans with ([|a1|]*wB+(wB-1)); [omega | ].
+  replace ([|a1|]*wB+(wB-1)) with (wB*([|a1|]+1)-1) by ring.
+  assert (wB*([|a1|]+1) <= wB*[|b|]); try omega.
+  apply Z.mul_le_mono_nonneg; omega.
+ Qed.
+
+ Lemma spec_div : forall a b, 0 < [|b|] ->
+      let (q,r) := div63 a b in
+      [|a|] = [|q|] * [|b|] + [|r|] /\
+      0 <= [|r|] < [|b|].
+ Proof.
+ unfold div63; intros.
+ assert ([|b|]>0) by (auto with zarith).
+ generalize (Z_div_mod [|a|] [|b|] H0) (Z_div_pos [|a|] [|b|] H0).
+ unfold Z.div; destruct (Z.div_eucl [|a|] [|b|]); simpl.
+ rewrite ?phi_phi_inv.
+ destruct 1; intros.
+ rewrite H1, Z.mul_comm.
+ generalize (phi_bounded a)(phi_bounded b); intros.
+ replace (z0 mod wB) with z0 by (symmetry; apply Zmod_small; omega).
+ replace (z mod wB) with z; auto with zarith.
+  symmetry; apply Zmod_small.
+  split; auto with zarith.
+  apply Z.le_lt_trans with [|a|]; auto with zarith.
+  rewrite H1.
+  apply Z.le_trans with ([|b|]*z); try omega.
+  rewrite <- (Z.mul_1_l z) at 1.
+  apply Z.mul_le_mono_nonneg; auto with zarith.
+ Qed.
+
+ Lemma spec_mod :  forall a b, 0 < [|b|] ->
+      [|let (_,r) := (a/b)%int in r|] = [|a|] mod [|b|].
+ Proof.
+ unfold div63; intros.
+ assert ([|b|]>0) by (auto with zarith).
+ unfold Z.modulo.
+ generalize (Z_div_mod [|a|] [|b|] H0).
+ destruct (Z.div_eucl [|a|] [|b|]); simpl.
+ rewrite ?phi_phi_inv.
+ destruct 1; intros.
+ generalize (phi_bounded b); intros.
+ apply Zmod_small; omega.
+ Qed.
+
+ Lemma phi_gcd : forall i j,
+  [|gcd63 i j|] = Zgcdn (2*size) [|j|] [|i|].
+ Proof.
+  unfold gcd63.
+  induction (2*size)%nat; intros.
+  reflexivity.
+  simpl.
+  unfold compare63.
+  change [|On|] with 0.
+  generalize (phi_bounded j)(phi_bounded i); intros.
+  case_eq [|j|]; intros.
+  simpl; intros.
+  generalize (Zabs_spec [|i|]); omega.
+  simpl.
+  rewrite IHn, H1; f_equal.
+  rewrite spec_mod, H1; auto.
+  rewrite H1; compute; auto.
+  rewrite H1 in H; destruct H as [H _]; compute in H; elim H; auto.
+ Qed.
+
+ Lemma spec_gcd : forall a b, Zis_gcd [|a|] [|b|] [|gcd63 a b|].
+ Proof.
+ intros.
+ rewrite phi_gcd.
+ apply Zis_gcd_sym.
+ apply Zgcdn_is_gcd.
+ unfold Zgcd_bound.
+ generalize (phi_bounded b).
+ destruct [|b|].
+ unfold size; auto with zarith.
+ intros (_,H).
+ cut (Pos.size_nat p <= size)%nat; [ omega | rewrite <- Zpower2_Psize; auto].
+ intros (H,_); compute in H; elim H; auto.
+ Qed.
+
+ Lemma iter_int63_iter_nat : forall A f i a,
+  iter_int63 i A f a = iter_nat (Z.abs_nat [|i|]) A f a.
+ Proof.
+ intros.
+ unfold iter_int63.
+ rewrite <- recrbis_equiv; auto; unfold recrbis.
+ rewrite <- phibis_aux_equiv.
+
+ revert i a; induction size.
+ simpl; auto.
+ simpl; intros.
+ case_eq (firstr i); intros H; rewrite 2 IHn;
+  unfold phibis_aux; simpl; rewrite H; fold (phibis_aux n (shiftr i));
+  generalize (phibis_aux_pos n (shiftr i)); intros;
+  set (z := phibis_aux n (shiftr i)) in *; clearbody z;
+  rewrite <- iter_nat_plus.
+
+ f_equal.
+ rewrite Z.double_spec, <- Z.add_diag.
+ symmetry; apply Zabs2Nat.inj_add; auto with zarith.
+
+ change (iter_nat (S (Z.abs_nat z + Z.abs_nat z)) A f a =
+         iter_nat (Z.abs_nat (Z.succ_double z)) A f a); f_equal.
+ rewrite Z.succ_double_spec, <- Z.add_diag.
+ rewrite Zabs2Nat.inj_add; auto with zarith.
+ rewrite Zabs2Nat.inj_add; auto with zarith.
+ change (Z.abs_nat 1) with 1%nat; omega.
+ Qed.
+
+ Fixpoint addmuldiv63_alt n i j :=
+  match n with
+    | O => i
+    | S n => addmuldiv63_alt n (sneakl (firstl j) i) (shiftl j)
+  end.
+
+ Lemma addmuldiv63_equiv : forall p x y,
+  addmuldiv63 p x y = addmuldiv63_alt (Z.abs_nat [|p|]) x y.
+ Proof.
+ intros.
+ unfold addmuldiv63.
+ rewrite iter_int63_iter_nat.
+ set (n:=Z.abs_nat [|p|]); clearbody n; clear p.
+ revert x y; induction n.
+ simpl; auto.
+ intros.
+ simpl addmuldiv63_alt.
+ replace (S n) with (n+1)%nat by (rewrite plus_comm; auto).
+ rewrite iter_nat_plus; simpl; auto.
+ Qed.
+
+ Lemma spec_add_mul_div : forall x y p, [|p|] <= Zpos 63 ->
+   [| addmuldiv63 p x y |] =
+   ([|x|] * (2 ^ [|p|]) + [|y|] / (2 ^ ((Zpos 63) - [|p|]))) mod wB.
+ Proof.
+ intros.
+ rewrite addmuldiv63_equiv.
+ assert ([|p|] = Z.of_nat (Z.abs_nat [|p|])).
+  rewrite Zabs2Nat.id_abs; symmetry; apply Z.abs_eq.
+  destruct (phi_bounded p); auto.
+ rewrite H0; rewrite H0 in H; clear H0; rewrite Zabs2Nat.id.
+ set (n := Z.abs_nat [|p|]) in *; clearbody n.
+ assert (n <= 63)%nat.
+  rewrite Nat2Z.inj_le; auto with zarith.
+ clear p H; revert x y.
+
+ induction n.
+ simpl; intros.
+ change (Z.pow_pos 2 63) with (2^63).
+ rewrite Z.mul_1_r.
+ replace ([|y|] / 2^63) with 0.
+ rewrite Z.add_0_r.
+ symmetry; apply Zmod_small; apply phi_bounded.
+ symmetry; apply Zdiv_small; apply phi_bounded.
+
+ simpl addmuldiv63_alt; intros.
+ rewrite IHn; [ | omega ].
+ case_eq (firstl y); intros.
+
+ rewrite phi_twice, Z.double_spec.
+ rewrite phi_twice_firstl; auto.
+ change (Z.double [|y|]) with (2*[|y|]).
+ rewrite Nat2Z.inj_succ, Z.pow_succ_r; auto with zarith.
+ rewrite Zplus_mod; rewrite Zmult_mod_idemp_l; rewrite <- Zplus_mod.
+ f_equal.
+ f_equal.
+ ring.
+ replace (63-Z.of_nat n) with (Z.succ(63-Z.succ(Z.of_nat n))) by ring.
+ rewrite Z.pow_succ_r, <- Zdiv_Zdiv; auto with zarith.
+ rewrite Z.mul_comm, Z_div_mult; auto with zarith.
+
+ rewrite phi_twice_plus_one, Z.succ_double_spec.
+ rewrite phi_twice; auto.
+ change (Z.double [|y|]) with (2*[|y|]).
+ rewrite Nat2Z.inj_succ, Z.pow_succ_r; auto with zarith.
+ rewrite Zplus_mod; rewrite Zmult_mod_idemp_l; rewrite <- Zplus_mod.
+ rewrite Z.mul_add_distr_r, Z.mul_1_l, <- Z.add_assoc.
+ f_equal.
+ f_equal.
+ ring.
+ assert ((2*[|y|]) mod wB = 2*[|y|] - wB).
+  clear - H. symmetry. apply Zmod_unique with 1; [ | ring ].
+  generalize (phi_lowerbound  _ H) (phi_bounded y).
+  set (wB' := 2^Z.of_nat (pred size)).
+  replace wB with (2*wB'); [ omega | ].
+  unfold wB'. rewrite <- Z.pow_succ_r, <- Nat2Z.inj_succ by (auto with zarith).
+  f_equal.
+ rewrite H1.
+ replace wB with (2^(Z.of_nat n)*2^(63-Z.of_nat n)) by
+  (rewrite <- Zpower_exp; auto with zarith; f_equal; unfold size; ring).
+ unfold Z.sub; rewrite <- Z.mul_opp_l.
+ rewrite Z_div_plus; auto with zarith.
+ ring_simplify.
+ replace (63+-Z.of_nat n) with (Z.succ(63-Z.succ(Z.of_nat n))) by ring.
+ rewrite Z.pow_succ_r, <- Zdiv_Zdiv; auto with zarith.
+ rewrite Z.mul_comm, Z_div_mult; auto with zarith.
+ Qed.
+
+ Lemma spec_pos_mod : forall w p,
+       [|ZnZ.pos_mod p w|] = [|w|] mod (2 ^ [|p|]).
+ Proof.
+ unfold ZnZ.pos_mod, int63_ops, compare63.
+ change [|63|] with 63%Z.
+ assert (forall w p, 63<=p -> [|w|] = [|w|] mod 2^p).
+  intros.
+  generalize (phi_bounded w).
+  symmetry; apply Zmod_small.
+  split; auto with zarith.
+  apply Z.lt_le_trans with wB; auto with zarith.
+  apply Zpower_le_monotone; auto with zarith.
+ intros.
+ case_eq ([|p|] ?= 63); intros;
+  [ apply H; rewrite (Z.compare_eq _ _ H0); auto with zarith | |
+    apply H; change ([|p|]>63)%Z in H0; auto with zarith ].
+ change ([|p|]<63) in H0.
+ rewrite spec_add_mul_div by auto with zarith.
+ change [|0|] with 0%Z; rewrite Z.mul_0_l, Z.add_0_l.
+ generalize (phi_bounded p)(phi_bounded w); intros.
+ assert (63-[|p|]<wB).
+  apply Z.le_lt_trans with 63%Z; auto with zarith.
+  compute; auto.
+ assert ([|63-p|]=63-[|p|]).
+  unfold sub63; rewrite phi_phi_inv.
+  change [|63|] with 63%Z.
+  apply Zmod_small; auto with zarith.
+ rewrite spec_add_mul_div by (rewrite H4; auto with zarith).
+ change [|0|] with 0%Z; rewrite Zdiv_0_l, Z.add_0_r.
+ rewrite H4.
+ apply shift_unshift_mod_2; auto with zarith.
+ Qed.
+
+
+ (** Shift operations *)
+
+ Lemma spec_head00:  forall x, [|x|] = 0 -> [|head063 x|] = Zpos 63.
+ Proof.
+  intros.
+  generalize (phi_inv_phi x).
+  rewrite H; simpl.
+  intros H'; rewrite <- H'.
+  simpl; auto.
+ Qed.
+
+ Fixpoint head063_alt n x :=
+  match n with
+    | O => 0%nat
+    | S n => match firstl x with
+               | D0 => S (head063_alt n (shiftl x))
+               | D1 => 0%nat
+             end
+  end.
+
+ Lemma head063_equiv :
+   forall x, [|head063 x|] = Z.of_nat (head063_alt size x).
+ Proof.
+ intros.
+ case_eq (iszero x); intros.
+ rewrite (iszero_eq0 _ H).
+ simpl; auto.
+
+ unfold head063, recl.
+ change On with (phi_inv (Z.of_nat (63-size))).
+ replace (head063_alt size x) with
+   (head063_alt size x + (63 - size))%nat by auto.
+ assert (size <= 63)%nat by auto with arith.
+
+ revert x H; induction size; intros.
+ simpl; auto.
+ unfold recl_aux; fold recl_aux.
+ unfold head063_alt; fold head063_alt.
+ rewrite H.
+ assert ([|phi_inv (Z.of_nat (63-S n))|] = Z.of_nat (63 - S n)).
+  rewrite phi_phi_inv.
+  apply Zmod_small.
+  split.
+  change 0 with (Z.of_nat O); apply inj_le; omega.
+  apply Z.le_lt_trans with (Z.of_nat 63).
+  apply inj_le; omega.
+  compute; auto.
+ case_eq (firstl x); intros; auto.
+ rewrite plus_Sn_m, plus_n_Sm.
+ replace (S (63 - S n)) with (63 - n)%nat by omega.
+ rewrite <- IHn; [ | omega | ].
+ f_equal; f_equal.
+ unfold add63.
+ rewrite H1.
+ f_equal.
+ change [|In|] with 1.
+ replace (63-n)%nat with (S (63 - S n))%nat by omega.
+ rewrite Nat2Z.inj_succ; ring.
+
+ clear - H H2.
+ rewrite (sneakr_shiftl x) in H.
+ rewrite H2 in H.
+ case_eq (iszero (shiftl x)); intros; auto.
+ rewrite (iszero_eq0 _ H0) in H; discriminate.
+ Qed.
+
+ Lemma phi_nz : forall x, 0 < [|x|] <-> x <> 0%int.
+ Proof.
+ split; intros.
+ red; intro; subst x; discriminate.
+ assert ([|x|]<>0%Z).
+ contradict H.
+ rewrite <- (phi_inv_phi x); rewrite H; auto.
+ generalize (phi_bounded x); auto with zarith.
+ Qed.
+
+ Lemma spec_head0  : forall x,  0 < [|x|] ->
+	 wB/ 2 <= 2 ^ ([|head063 x|]) * [|x|] < wB.
+ Proof.
+ intros.
+ rewrite head063_equiv.
+ assert (nshiftl size x = 0%int).
+  apply nshiftl_size.
+ revert x H H0.
+ unfold size at 2 5.
+ induction size.
+ simpl Z.of_nat.
+ intros.
+ compute in H0; rewrite H0 in H; discriminate.
+
+ intros.
+ simpl head063_alt.
+ case_eq (firstl x); intros.
+ rewrite (Nat2Z.inj_succ (head063_alt n (shiftl x))), Z.pow_succ_r; auto with zarith.
+ rewrite <- Z.mul_assoc, Z.mul_comm, <- Z.mul_assoc, <-(Z.mul_comm 2).
+ rewrite <- Z.double_spec, <- (phi_twice_firstl _ H1).
+ apply IHn.
+
+ rewrite phi_nz; rewrite phi_nz in H; contradict H.
+ change twice with shiftl in H.
+ rewrite (sneakr_shiftl x), H1, H; auto.
+
+ rewrite <- nshiftl_S_tail; auto.
+
+ change (2^(Z.of_nat 0)) with 1; rewrite Z.mul_1_l.
+ generalize (phi_bounded x); unfold size; split; auto with zarith.
+ change (2^(Z.of_nat 63)/2) with (2^(Z.of_nat (pred size))).
+ apply phi_lowerbound; auto.
+ Qed.
+
+ Lemma spec_tail00:  forall x, [|x|] = 0 -> [|tail063 x|] = Zpos 63.
+ Proof.
+  intros.
+  generalize (phi_inv_phi x).
+  rewrite H; simpl.
+  intros H'; rewrite <- H'.
+  simpl; auto.
+ Qed.
+
+ Fixpoint tail063_alt n x :=
+  match n with
+    | O => 0%nat
+    | S n => match firstr x with
+               | D0 => S (tail063_alt n (shiftr x))
+               | D1 => 0%nat
+             end
+  end.
+
+ Lemma tail063_equiv :
+   forall x, [|tail063 x|] = Z.of_nat (tail063_alt size x).
+ Proof.
+ intros.
+ case_eq (iszero x); intros.
+ rewrite (iszero_eq0 _ H).
+ simpl; auto.
+
+ unfold tail063, recr.
+ change On with (phi_inv (Z.of_nat (63-size))).
+ replace (tail063_alt size x) with
+   (tail063_alt size x + (63 - size))%nat by auto.
+ assert (size <= 63)%nat by auto with arith.
+
+ revert x H; induction size; intros.
+ simpl; auto.
+ unfold recr_aux; fold recr_aux.
+ unfold tail063_alt; fold tail063_alt.
+ rewrite H.
+ assert ([|phi_inv (Z.of_nat (63-S n))|] = Z.of_nat (63 - S n)).
+  rewrite phi_phi_inv.
+  apply Zmod_small.
+  split.
+  change 0 with (Z.of_nat O); apply inj_le; omega.
+  apply Z.le_lt_trans with (Z.of_nat 63).
+  apply inj_le; omega.
+  compute; auto.
+ case_eq (firstr x); intros; auto.
+ rewrite plus_Sn_m, plus_n_Sm.
+ replace (S (63 - S n)) with (63 - n)%nat by omega.
+ rewrite <- IHn; [ | omega | ].
+ f_equal; f_equal.
+ unfold add63.
+ rewrite H1.
+ f_equal.
+ change [|In|] with 1.
+ replace (63-n)%nat with (S (63 - S n))%nat by omega.
+ rewrite Nat2Z.inj_succ; ring.
+
+ clear - H H2.
+ rewrite (sneakl_shiftr x) in H.
+ rewrite H2 in H.
+ case_eq (iszero (shiftr x)); intros; auto.
+ rewrite (iszero_eq0 _ H0) in H; discriminate.
+ Qed.
+
+ Lemma spec_tail0  : forall x, 0 < [|x|] ->
+         exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|tail063 x|]).
+ Proof.
+ intros.
+ rewrite tail063_equiv.
+ assert (nshiftr size x = 0%int).
+  apply nshiftr_size.
+ revert x H H0.
+ induction size.
+ simpl Z.of_nat.
+ intros.
+ compute in H0; rewrite H0 in H; discriminate.
+
+ intros.
+ simpl tail063_alt.
+ case_eq (firstr x); intros.
+ rewrite (Nat2Z.inj_succ (tail063_alt n (shiftr x))), Z.pow_succ_r; auto with zarith.
+ destruct (IHn (shiftr x)) as (y & Hy1 & Hy2).
+
+ rewrite phi_nz; rewrite phi_nz in H; contradict H.
+ rewrite (sneakl_shiftr x), H1, H; auto.
+
+ rewrite <- nshiftr_S_tail; auto.
+
+ exists y; split; auto.
+ rewrite phi_eqn1; auto.
+ rewrite Z.double_spec, Hy2; ring.
+
+ exists [|shiftr x|].
+ split.
+ generalize (phi_bounded (shiftr x)); auto with zarith.
+ rewrite phi_eqn2; auto.
+ rewrite Z.succ_double_spec; simpl; ring.
+ Qed.
+
+ (* Sqrt *)
+
+ (* Direct transcription of an old proof
+     of a fortran program in boyer-moore *)
+
+ Lemma quotient_by_2 a: a - 1 <= (a/2) + (a/2).
+ Proof.
+ case (Z_mod_lt a 2); auto with zarith.
+ intros H1; rewrite Zmod_eq_full; auto with zarith.
+ Qed.
+
+ Lemma sqrt_main_trick j k: 0 <= j -> 0 <= k ->
+   (j * k) + j <= ((j + k)/2 + 1)  ^ 2.
+ Proof.
+ intros Hj; generalize Hj k; pattern j; apply natlike_ind;
+   auto; clear k j Hj.
+ intros _ k Hk; repeat rewrite Z.add_0_l.
+ apply  Z.mul_nonneg_nonneg; generalize (Z_div_pos k 2); auto with zarith.
+ intros j Hj Hrec _ k Hk; pattern k; apply natlike_ind; auto; clear k Hk.
+ rewrite Z.mul_0_r, Z.add_0_r, Z.add_0_l.
+ generalize (sqr_pos (Z.succ j / 2)) (quotient_by_2 (Z.succ j));
+   unfold Z.succ.
+ rewrite Z.pow_2_r, Z.mul_add_distr_r; repeat rewrite Z.mul_add_distr_l.
+ auto with zarith.
+ intros k Hk _.
+ replace ((Z.succ j + Z.succ k) / 2) with ((j + k)/2 + 1).
+ generalize (Hrec Hj k Hk) (quotient_by_2 (j + k)).
+ unfold Z.succ; repeat rewrite Z.pow_2_r;
+   repeat rewrite Z.mul_add_distr_r; repeat rewrite Z.mul_add_distr_l.
+ repeat rewrite Z.mul_1_l; repeat rewrite Z.mul_1_r.
+ auto with zarith.
+ rewrite Z.add_comm, <- Z_div_plus_full_l; auto with zarith.
+ apply f_equal2 with (f := Z.div); auto with zarith.
+ Qed.
+
+ Lemma sqrt_main i j: 0 <= i -> 0 < j -> i < ((j + (i/j))/2 + 1) ^ 2.
+ Proof.
+ intros Hi Hj.
+ assert (Hij: 0 <= i/j) by (apply Z_div_pos; auto with zarith).
+ apply Z.lt_le_trans with (2 := sqrt_main_trick _ _ (Z.lt_le_incl _ _ Hj) Hij).
+ pattern i at 1; rewrite (Z_div_mod_eq i j); case (Z_mod_lt i j); auto with zarith.
+ Qed.
+
+ Lemma sqrt_init i: 1 < i -> i < (i/2 + 1) ^ 2.
+ Proof.
+ intros Hi.
+ assert (H1: 0 <= i - 2) by auto with zarith.
+ assert (H2: 1 <= (i / 2) ^ 2); auto with zarith.
+   replace i with (1* 2 + (i - 2)); auto with zarith.
+   rewrite Z.pow_2_r, Z_div_plus_full_l; auto with zarith.
+   generalize (sqr_pos ((i - 2)/ 2)) (Z_div_pos (i - 2) 2).
+   rewrite Z.mul_add_distr_r; repeat rewrite Z.mul_add_distr_l.
+   auto with zarith.
+ generalize (quotient_by_2 i).
+ rewrite Z.pow_2_r in H2 |- *;
+   repeat (rewrite Z.mul_add_distr_r ||
+           rewrite Z.mul_add_distr_l ||
+           rewrite Z.mul_1_l || rewrite Z.mul_1_r).
+   auto with zarith.
+ Qed.
+
+ Lemma sqrt_test_true i j: 0 <= i -> 0 < j -> i/j >= j -> j ^ 2 <= i.
+ Proof.
+ intros Hi Hj Hd; rewrite Z.pow_2_r.
+ apply Z.le_trans with (j * (i/j)); auto with zarith.
+ apply Z_mult_div_ge; auto with zarith.
+ Qed.
+
+ Lemma sqrt_test_false i j: 0 <= i -> 0 < j -> i/j < j ->  (j + (i/j))/2 < j.
+ Proof.
+ intros Hi Hj H; case (Z.le_gt_cases j ((j + (i/j))/2)); auto.
+ intros H1; contradict H; apply Z.le_ngt.
+ assert (2 * j <= j + (i/j)); auto with zarith.
+ apply Z.le_trans with (2 * ((j + (i/j))/2)); auto with zarith.
+ apply Z_mult_div_ge; auto with zarith.
+ Qed.
+
+ Lemma sqrt63_step_def rec i j:
+   sqrt63_step rec i j =
+   match (fst (i/j) ?= j)%int with
+     Lt => rec i (fst ((j + fst(i/j))/2))%int
+   | _ =>  j
+   end.
+ Proof.
+ unfold sqrt63_step; case div63; intros.
+ simpl; case compare63; auto.
+ Qed.
+
+ Lemma div63_phi i j: 0 < [|j|] -> [|fst (i/j)%int|] = [|i|]/[|j|].
+ intros Hj; generalize (spec_div i j Hj).
+ case div63; intros q r; simpl fst.
+ intros (H1,H2); apply Zdiv_unique with [|r|]; auto with zarith.
+ rewrite H1; ring.
+ Qed.
+
+ Lemma sqrt63_step_correct rec i j:
+  0 < [|i|] -> 0 < [|j|] -> [|i|] < ([|j|] + 1) ^ 2 ->
+   2 * [|j|] < wB ->
+  (forall j1 : int63,
+    0 < [|j1|] < [|j|] -> [|i|] < ([|j1|] + 1) ^ 2 ->
+    [|rec i j1|] ^ 2 <= [|i|] < ([|rec i j1|] + 1) ^ 2) ->
+  [|sqrt63_step rec i j|] ^ 2 <= [|i|] < ([|sqrt63_step rec i j|] + 1) ^ 2.
+ Proof.
+ assert (Hp2: 0 < [|2|]) by exact (eq_refl Lt).
+ intros Hi Hj Hij H63 Hrec; rewrite sqrt63_step_def.
+ rewrite spec_compare, div63_phi; auto.
+   case Z.compare_spec; auto; intros Hc;
+   try (split; auto; apply sqrt_test_true; auto with zarith; fail).
+ apply Hrec; repeat rewrite div63_phi; auto with zarith.
+ replace [|(j + fst (i / j)%int)|] with ([|j|] + [|i|] / [|j|]).
+ split.
+ apply Z.le_succ_l in Hj. change (1 <= [|j|]) in Hj.
+ Z.le_elim Hj.
+ replace ([|j|] + [|i|]/[|j|]) with
+        (1 * 2 + (([|j|] - 2) + [|i|] / [|j|])); try ring.
+ rewrite Z_div_plus_full_l; auto with zarith.
+ assert (0 <= [|i|]/ [|j|]) by (apply Z_div_pos; auto with zarith).
+ assert (0 <= ([|j|] - 2 + [|i|] / [|j|]) / [|2|]) ; auto with zarith.
+ rewrite <- Hj, Zdiv_1_r.
+ replace (1 + [|i|])%Z with (1 * 2 + ([|i|] - 1))%Z; try ring.
+ rewrite Z_div_plus_full_l; auto with zarith.
+ assert (0 <= ([|i|] - 1) /2)%Z by (apply Z_div_pos; auto with zarith).
+ change ([|2|]) with 2%Z; auto with zarith.
+ apply sqrt_test_false; auto with zarith.
+ rewrite spec_add, div63_phi; auto.
+ symmetry; apply Zmod_small.
+ split; auto with zarith.
+ replace [|j + fst (i / j)%int|] with ([|j|] + [|i|] / [|j|]).
+ apply sqrt_main; auto with zarith.
+ rewrite spec_add, div63_phi; auto.
+ symmetry; apply Zmod_small.
+ split; auto with zarith.
+ Qed.
+
+ Lemma iter63_sqrt_correct n rec i j: 0 < [|i|] -> 0 < [|j|] ->
+  [|i|] < ([|j|] + 1) ^ 2 -> 2 * [|j|] < 2 ^ (Z.of_nat size) ->
+  (forall j1, 0 < [|j1|] -> 2^(Z.of_nat n) + [|j1|] <= [|j|] ->
+      [|i|] < ([|j1|] + 1) ^ 2 -> 2 * [|j1|] < 2 ^ (Z.of_nat size) ->
+       [|rec i j1|] ^ 2 <= [|i|] < ([|rec i j1|] + 1) ^ 2) ->
+  [|iter63_sqrt n rec i j|] ^ 2 <= [|i|] < ([|iter63_sqrt n rec i j|] + 1) ^ 2.
+ Proof.
+ revert rec i j; elim n; unfold iter63_sqrt; fold iter63_sqrt; clear n.
+ intros rec i j Hi Hj Hij H63 Hrec; apply sqrt63_step_correct; auto with zarith.
+ intros; apply Hrec; auto with zarith.
+ rewrite Z.pow_0_r; auto with zarith.
+ intros n Hrec rec i j Hi Hj Hij H63 HHrec.
+ apply sqrt63_step_correct; auto.
+ intros j1 Hj1  Hjp1; apply Hrec; auto with zarith.
+ intros j2 Hj2 H2j2 Hjp2 Hj63; apply Hrec; auto with zarith.
+ intros j3 Hj3 Hpj3.
+ apply HHrec; auto.
+ rewrite Nat2Z.inj_succ, Z.pow_succ_r.
+ apply Z.le_trans with (2 ^Z.of_nat n + [|j2|]); auto with zarith.
+ apply Nat2Z.is_nonneg.
+ Qed.
+
+ Lemma spec_sqrt : forall x,
+       [|sqrt63 x|] ^ 2 <= [|x|] < ([|sqrt63 x|] + 1) ^ 2.
+ Proof.
+ intros i; unfold sqrt63.
+ fold On In Twon.
+ rewrite spec_compare. case Z.compare_spec; change [|1|] with 1;
+   intros Hi; auto with zarith.
+ repeat rewrite Z.pow_2_r; auto with zarith.
+ apply iter63_sqrt_correct; auto with zarith.
+  rewrite div63_phi; change ([|2|]) with 2;  auto with zarith.
+  replace ([|i|]) with (1 * 2 + ([|i|] - 2))%Z; try ring.
+  assert (0 <= ([|i|] - 2)/2)%Z by (apply Z_div_pos; auto with zarith).
+  rewrite Z_div_plus_full_l; auto with zarith.
+  rewrite div63_phi; change ([|2|]) with 2; auto with zarith.
+  apply sqrt_init; auto.
+ rewrite div63_phi; change ([|2|]) with 2; auto with zarith.
+ apply Z.le_lt_trans with ([|i|]).
+ apply Z_mult_div_ge; auto with zarith.
+ case (phi_bounded i); auto.
+ intros j2 H1 H2; contradict H2; apply Z.lt_nge.
+ rewrite div63_phi; change ([|2|]) with 2; auto with zarith.
+ apply Z.le_lt_trans with ([|i|]); auto with zarith.
+ assert (0 <= [|i|]/2)%Z by (apply Z_div_pos; auto with zarith).
+ apply Z.le_trans with (2 * ([|i|]/2)); auto with zarith.
+ apply Z_mult_div_ge; auto with zarith.
+ case (phi_bounded i); unfold size; auto with zarith.
+ change [|0|] with 0; auto with zarith.
+ case (phi_bounded i); repeat rewrite Z.pow_2_r; auto with zarith.
+ Qed.
+
+ Lemma sqrt632_step_def rec ih il j:
+   sqrt632_step rec ih il j =
+   match (ih ?= j)%int with
+      Eq => j
+    | Gt => j
+    | _ =>
+       match (fst (div6321 ih il j) ?= j)%int with
+         Lt => let m := match j +c fst (div6321 ih il j) with
+                       C0 m1 => fst (m1/2)%int
+                     | C1 m1 => (fst (m1/2) + v30)%int
+                     end in rec ih il m
+       | _ =>  j
+       end
+   end.
+ Proof.
+ unfold sqrt632_step; case div6321; intros.
+ simpl; case compare63; auto.
+ Qed.
+
+ Lemma sqrt632_lower_bound ih il j:
+   phi2 ih  il  < ([|j|] + 1) ^ 2 -> [|ih|] <= [|j|].
+ Proof.
+ intros H1.
+ case (phi_bounded j); intros Hbj _.
+ case (phi_bounded il); intros Hbil _.
+ case (phi_bounded ih); intros Hbih Hbih1.
+ assert (([|ih|] < [|j|] + 1)%Z); auto with zarith.
+ apply Z.square_lt_simpl_nonneg; auto with zarith.
+ repeat rewrite <-Z.pow_2_r; apply Z.le_lt_trans with (2 := H1).
+ apply Z.le_trans with ([|ih|] * base)%Z; unfold phi2, base;
+  try rewrite Z.pow_2_r; auto with zarith.
+ Qed.
+
+ Lemma div632_phi ih il j: (2^62 <= [|j|] -> [|ih|] < [|j|] ->
+  [|fst (div6321 ih il j)|] = phi2 ih il/[|j|])%Z.
+ Proof.
+ intros Hj Hj1.
+ generalize (spec_div21 ih il j Hj Hj1).
+ case div6321; intros q r (Hq, Hr).
+ apply Zdiv_unique with (phi r); auto with zarith.
+ simpl fst; apply eq_trans with (1 := Hq); ring.
+ Qed.
+
+ Lemma sqrt632_step_correct rec ih il j:
+  2 ^ 61 <= [|ih|] -> 0 < [|j|] -> phi2 ih il < ([|j|] + 1) ^ 2 ->
+  (forall j1, 0 < [|j1|] < [|j|] ->  phi2 ih il < ([|j1|] + 1) ^ 2 ->
+     [|rec ih il j1|] ^ 2 <= phi2 ih il < ([|rec ih il j1|] + 1) ^ 2) ->
+  [|sqrt632_step rec ih il  j|] ^ 2 <= phi2 ih il
+      < ([|sqrt632_step rec ih il j|] + 1) ^  2.
+ Proof.
+ assert (Hp2: (0 < [|2|])%Z) by exact (eq_refl Lt).
+ intros Hih Hj Hij Hrec; rewrite sqrt632_step_def.
+ assert (H1: ([|ih|] <= [|j|])%Z) by (apply sqrt632_lower_bound with il; auto).
+ case (phi_bounded ih); intros Hih1 _.
+ case (phi_bounded il); intros Hil1 _.
+ case (phi_bounded j); intros _ Hj1.
+ assert (Hp3: (0 < phi2 ih il)).
+ unfold phi2; apply Z.lt_le_trans with ([|ih|] * base)%Z; auto with zarith.
+ apply Z.mul_pos_pos; auto with zarith.
+ apply Z.lt_le_trans with (2:= Hih); auto with zarith.
+ rewrite spec_compare. case Z.compare_spec; intros Hc1.
+ split; auto.
+ apply sqrt_test_true; auto.
+ unfold phi2, base; auto with zarith.
+ unfold phi2; rewrite Hc1.
+ assert (0 <= [|il|]/[|j|]) by (apply Z_div_pos; auto with zarith).
+ rewrite Z.mul_comm, Z_div_plus_full_l; unfold base; auto with zarith.
+ unfold Z.pow, Z.pow_pos in Hj1; simpl in Hj1; auto with zarith.
+ case (Z.le_gt_cases (2 ^ 62) [|j|]); intros Hjj.
+ rewrite spec_compare; case Z.compare_spec;
+  rewrite div632_phi; auto; intros Hc;
+  try (split; auto; apply sqrt_test_true; auto with zarith; fail).
+ apply Hrec.
+ assert (Hf1: 0 <= phi2 ih il/ [|j|]) by (apply Z_div_pos; auto with zarith).
+ apply Z.le_succ_l in Hj. change (1 <= [|j|]) in Hj.
+ Z.le_elim Hj.
+ 2: contradict Hc; apply Z.le_ngt; rewrite <- Hj, Zdiv_1_r; auto with zarith.
+ assert (Hf3: 0 < ([|j|] + phi2 ih il / [|j|]) / 2).
+ replace ([|j|] + phi2 ih il/ [|j|])%Z with
+        (1 * 2 + (([|j|] - 2) + phi2 ih il / [|j|])); try ring.
+ rewrite Z_div_plus_full_l; auto with zarith.
+ assert (0 <= ([|j|] - 2 + phi2 ih il / [|j|]) / 2) ; auto with zarith.
+ assert (Hf4: ([|j|] + phi2 ih il / [|j|]) / 2 < [|j|]).
+ apply sqrt_test_false; auto with zarith.
+ generalize (spec_add_c j (fst (div6321 ih il j))).
+ unfold interp_carry;  case add63c; intros r;
+  rewrite div632_phi; auto with zarith.
+ rewrite div63_phi; change [|2|] with 2%Z; auto with zarith.
+ intros HH; rewrite HH; clear HH; auto with zarith.
+ rewrite spec_add, div63_phi; change [|2|] with 2%Z; auto.
+ rewrite Z.mul_1_l; intros HH.
+ rewrite Z.add_comm, <- Z_div_plus_full_l; auto with zarith.
+ change (phi v30 * 2) with (2 ^ Z.of_nat size).
+ rewrite HH, Zmod_small; auto with zarith.
+ replace (phi
+    match j +c fst (div6321 ih il j) with
+    | C0 m1 => fst (m1 / 2)%int
+    | C1 m1 => fst (m1 / 2)%int + v30
+    end) with ((([|j|] + (phi2 ih il)/([|j|]))/2)).
+ apply sqrt_main; auto with zarith.
+ generalize (spec_add_c j (fst (div6321 ih il j))).
+ unfold interp_carry;  case add63c; intros r;
+  rewrite div632_phi; auto with zarith.
+ rewrite div63_phi; auto with zarith.
+ intros HH; rewrite HH; auto with zarith.
+ intros HH; rewrite <- HH.
+ change (1 * 2 ^ Z.of_nat size) with (phi (v30) * 2).
+ rewrite Z_div_plus_full_l; auto with zarith.
+ rewrite Z.add_comm.
+ rewrite spec_add, Zmod_small.
+ rewrite div63_phi; auto.
+ split; auto with zarith.
+ case (phi_bounded (fst (r/2)%int));
+   case (phi_bounded v30); auto with zarith.
+ rewrite div63_phi; change (phi 2) with 2%Z; auto.
+ change (2 ^Z.of_nat size) with (base/2 + phi v30).
+ assert (phi r / 2 < base/2); auto with zarith.
+ apply Z.mul_lt_mono_pos_r with 2; auto with zarith.
+ change (base/2 * 2) with base.
+ apply Z.le_lt_trans with (phi r).
+ rewrite Z.mul_comm; apply Z_mult_div_ge; auto with zarith.
+ case (phi_bounded r); auto with zarith.
+ contradict Hij; apply Z.le_ngt.
+ assert ((1 + [|j|]) <= 2 ^ 62); auto with zarith.
+ apply Z.le_trans with ((2 ^ 62) * (2 ^ 62)); auto with zarith.
+ assert (0 <= 1 + [|j|]); auto with zarith.
+ apply Z.mul_le_mono_nonneg; auto with zarith.
+ change ((2 ^ 62) * (2 ^ 62)) with ((2 ^ 61) * base).
+ apply Z.le_trans with ([|ih|] * base); auto with zarith.
+ unfold phi2, base; auto with zarith.
+ split; auto.
+ apply sqrt_test_true; auto.
+ unfold phi2, base; auto with zarith.
+ apply Z.le_ge; apply Z.le_trans with (([|j|] * base)/[|j|]).
+ rewrite Z.mul_comm, Z_div_mult; auto with zarith.
+ apply Z.ge_le; apply Z_div_ge; auto with zarith.
+ Qed.
+
+ Lemma iter632_sqrt_correct n rec ih il j:
+  2^61 <= [|ih|] ->  0 < [|j|] -> phi2 ih il < ([|j|] + 1) ^ 2 ->
+  (forall j1, 0 < [|j1|] -> 2^(Z.of_nat n) + [|j1|] <= [|j|] ->
+      phi2 ih il < ([|j1|] + 1) ^ 2 ->
+       [|rec ih il j1|] ^ 2 <= phi2 ih il < ([|rec ih il j1|] + 1) ^ 2)  ->
+  [|iter632_sqrt n rec ih il j|] ^ 2 <= phi2 ih il
+      < ([|iter632_sqrt n rec ih il j|] + 1) ^ 2.
+ Proof.
+ revert rec ih il j; elim n; unfold iter632_sqrt; fold iter632_sqrt; clear n.
+ intros rec ih il j Hi Hj Hij Hrec; apply sqrt632_step_correct; auto with zarith.
+ intros; apply Hrec; auto with zarith.
+ rewrite Z.pow_0_r; auto with zarith.
+ intros n Hrec rec ih il j Hi Hj Hij HHrec.
+ apply sqrt632_step_correct; auto.
+ intros j1 Hj1  Hjp1; apply Hrec; auto with zarith.
+ intros j2 Hj2 H2j2 Hjp2; apply Hrec; auto with zarith.
+ intros j3 Hj3 Hpj3.
+ apply HHrec; auto.
+ rewrite Nat2Z.inj_succ, Z.pow_succ_r.
+ apply Z.le_trans with (2 ^Z.of_nat n + [|j2|])%Z; auto with zarith.
+ apply Nat2Z.is_nonneg.
+ Qed.
+
+ Lemma spec_sqrt2 : forall x y,
+       wB/ 4 <= [|x|] ->
+       let (s,r) := sqrt632 x y in
+          [||WW x y||] = [|s|] ^ 2 + [+|r|] /\
+          [+|r|] <= 2 * [|s|].
+ Proof.
+ intros ih il Hih; unfold sqrt632.
+ fold On In.
+ change [||WW ih il||] with (phi2 ih il).
+ assert (Hbin: forall s, s * s + 2* s + 1 = (s + 1) ^ 2) by
+  (intros s; ring).
+ assert (Hb: 0 <= base) by (red; intros HH; discriminate).
+ assert (Hi2: phi2 ih il < (phi Tn + 1) ^ 2).
+ { change ((phi Tn + 1) ^ 2) with (2^126).
+   apply Z.le_lt_trans with ((2^63 -1) * base + (2^63 - 1)); auto with zarith.
+   2: simpl; unfold Z.pow_pos; simpl; auto with zarith.
+   case (phi_bounded ih); case (phi_bounded il); intros H1 H2 H3 H4.
+   unfold base, Z.pow, Z.pow_pos in H2,H4; simpl in H2,H4.
+   unfold phi2,Z.pow, Z.pow_pos. simpl Pos.iter; auto with zarith. }
+ case (iter632_sqrt_correct 63 (fun _ _ j => j) ih il Tn); auto with zarith.
+ change [|Tn|] with 9223372036854775807; auto with zarith.
+ intros j1 _ HH; contradict HH.
+ apply Z.lt_nge.
+ change [|Tn|] with 9223372036854775807; auto with zarith.
+ change (2 ^ Z.of_nat 63) with 9223372036854775808; auto with zarith.
+ case (phi_bounded j1); auto with zarith.
+ set (s := iter632_sqrt 63 (fun _ _ j : int63 => j) ih il Tn).
+ intros Hs1 Hs2.
+ generalize (spec_mul_c s s); case mul63c.
+ simpl zn2z_to_Z; intros HH.
+ assert ([|s|] = 0).
+ { symmetry in HH. rewrite Z.mul_eq_0 in HH. destruct HH; auto. }
+ contradict Hs2; apply Z.le_ngt; rewrite H.
+ change ((0 + 1) ^ 2) with 1.
+ apply Z.le_trans with (2 ^ Z.of_nat size / 4 * base).
+ simpl; auto with zarith.
+ apply Z.le_trans with ([|ih|] * base); auto with zarith.
+ unfold phi2; case (phi_bounded il); auto with zarith.
+ intros ih1 il1.
+ change [||WW ih1 il1||] with (phi2 ih1 il1).
+ intros Hihl1.
+ generalize (spec_sub_c il il1).
+ case sub63c; intros il2 Hil2.
+ simpl interp_carry in Hil2.
+ rewrite spec_compare; case Z.compare_spec.
+ unfold interp_carry.
+ intros H1; split.
+ rewrite Z.pow_2_r, <- Hihl1.
+ unfold phi2; ring[Hil2 H1].
+ replace [|il2|] with (phi2 ih il - phi2 ih1 il1).
+ rewrite Hihl1.
+ rewrite <-Hbin in Hs2; auto with zarith.
+ unfold phi2; rewrite H1, Hil2; ring.
+ unfold interp_carry.
+ intros H1; contradict Hs1.
+ apply Z.lt_nge; rewrite Z.pow_2_r, <-Hihl1.
+ unfold phi2.
+ case (phi_bounded il); intros _ H2.
+ apply Z.lt_le_trans with (([|ih|] + 1) * base + 0).
+ rewrite Z.mul_add_distr_r, Z.add_0_r; auto with zarith.
+ case (phi_bounded il1); intros H3 _.
+ apply Z.add_le_mono; auto with zarith.
+ unfold interp_carry; change (1 * 2 ^ Z.of_nat size) with base.
+ rewrite Z.pow_2_r, <- Hihl1, Hil2.
+ intros H1.
+ rewrite <- Z.le_succ_l, <- Z.add_1_r in H1.
+ Z.le_elim H1.
+ contradict Hs2; apply Z.le_ngt.
+ replace (([|s|] + 1) ^ 2) with (phi2 ih1 il1 + 2 * [|s|] + 1).
+ unfold phi2.
+ case (phi_bounded il); intros Hpil _.
+ assert (Hl1l: [|il1|] <= [|il|]).
+ { case (phi_bounded il2); rewrite Hil2; auto with zarith. }
+ assert ([|ih1|] * base + 2 * [|s|] + 1 <= [|ih|] * base); auto with zarith.
+ case (phi_bounded s);  change (2 ^ Z.of_nat size) with base; intros _ Hps.
+ case (phi_bounded ih1); intros Hpih1 _; auto with zarith.
+ apply Z.le_trans with (([|ih1|] + 2) * base); auto with zarith.
+ rewrite Z.mul_add_distr_r.
+ assert (2 * [|s|] + 1 <= 2 * base); auto with zarith.
+ rewrite Hihl1, Hbin; auto.
+ split.
+ unfold phi2; rewrite <- H1; ring.
+ replace (base + ([|il|] - [|il1|])) with (phi2 ih il - ([|s|] * [|s|])).
+ rewrite <-Hbin in Hs2; auto with zarith.
+ rewrite <- Hihl1; unfold phi2; rewrite <- H1; ring.
+ unfold interp_carry in Hil2 |- *.
+ unfold interp_carry; change (1 * 2 ^ Z.of_nat size) with base.
+ assert (Hsih: [|ih - 1|] = [|ih|] - 1).
+ { rewrite spec_sub, Zmod_small; auto; change [|1|] with 1.
+   case (phi_bounded ih); intros H1 H2.
+   generalize Hih; change (2 ^ Z.of_nat size / 4) with 2305843009213693952.
+   split; auto with zarith. }
+ rewrite spec_compare; case Z.compare_spec.
+ rewrite Hsih.
+ intros H1; split.
+ rewrite Z.pow_2_r, <- Hihl1.
+ unfold phi2; rewrite <-H1.
+ transitivity ([|ih|] * base + [|il1|] + ([|il|] - [|il1|])).
+ ring.
+ rewrite <-Hil2.
+ change (2 ^ Z.of_nat size) with base; ring.
+ replace [|il2|] with (phi2 ih il - phi2 ih1 il1).
+ rewrite Hihl1.
+ rewrite <-Hbin in Hs2; auto with zarith.
+ unfold phi2.
+ rewrite <-H1.
+ ring_simplify.
+ transitivity (base + ([|il|] - [|il1|])).
+ ring.
+ rewrite <-Hil2.
+ change (2 ^ Z.of_nat size) with base; ring.
+ rewrite Hsih; intros H1.
+ assert (He: [|ih|] = [|ih1|]).
+ { apply Z.le_antisymm; auto with zarith.
+   case (Z.le_gt_cases [|ih1|] [|ih|]); auto; intros H2.
+   contradict Hs1; apply Z.lt_nge; rewrite Z.pow_2_r, <-Hihl1.
+   unfold phi2.
+   case (phi_bounded il); change (2 ^ Z.of_nat size) with base;
+    intros _ Hpil1.
+   apply Z.lt_le_trans with (([|ih|] + 1) * base).
+   rewrite Z.mul_add_distr_r, Z.mul_1_l; auto with zarith.
+   case (phi_bounded il1); intros Hpil2 _.
+   apply Z.le_trans with (([|ih1|]) * base); auto with zarith. }
+ rewrite Z.pow_2_r, <-Hihl1; unfold phi2; rewrite <-He.
+ contradict Hs1; apply Z.lt_nge; rewrite Z.pow_2_r, <-Hihl1.
+ unfold phi2; rewrite He.
+ assert (phi il - phi il1 < 0); auto with zarith.
+ rewrite <-Hil2.
+ case (phi_bounded il2); auto with zarith.
+ intros H1.
+ rewrite Z.pow_2_r, <-Hihl1.
+ assert (H2 : [|ih1|]+2 <= [|ih|]); auto with zarith.
+ Z.le_elim H2.
+ contradict Hs2; apply Z.le_ngt.
+ replace (([|s|] + 1) ^ 2) with (phi2 ih1 il1 + 2 * [|s|] + 1).
+ unfold phi2.
+ assert ([|ih1|] * base + 2 * phi s + 1 <= [|ih|] * base + ([|il|] - [|il1|]));
+  auto with zarith.
+ rewrite <-Hil2.
+ change (-1 * 2 ^ Z.of_nat size) with (-base).
+ case (phi_bounded il2); intros Hpil2 _.
+ apply Z.le_trans with ([|ih|] * base + - base); auto with zarith.
+ case (phi_bounded s);  change (2 ^ Z.of_nat size) with base; intros _ Hps.
+ assert (2 * [|s|] + 1 <= 2 * base); auto with zarith.
+ apply Z.le_trans with ([|ih1|] * base + 2 * base); auto with zarith.
+ assert (Hi: ([|ih1|] + 3) * base <= [|ih|] * base); auto with zarith.
+ rewrite Z.mul_add_distr_r in Hi; auto with zarith.
+ rewrite Hihl1, Hbin; auto.
+ unfold phi2; rewrite <-H2.
+ split.
+ replace [|il|] with (([|il|] - [|il1|]) + [|il1|]); try ring.
+ rewrite <-Hil2.
+ change (-1 * 2 ^ Z.of_nat size) with (-base); ring.
+ replace (base + [|il2|]) with (phi2 ih il - phi2 ih1 il1).
+ rewrite Hihl1.
+ rewrite <-Hbin in Hs2; auto with zarith.
+ unfold phi2; rewrite <-H2.
+ replace [|il|] with (([|il|] - [|il1|]) + [|il1|]); try ring.
+ rewrite <-Hil2.
+ change (-1 * 2 ^ Z.of_nat size) with (-base); ring.
+Qed.
+
+ (** [iszero] *)
+
+ Lemma spec_eq0 : forall x, ZnZ.eq0 x = true -> [|x|] = 0.
+ Proof.
+ clear; unfold ZnZ.eq0; simpl.
+ unfold compare63; simpl; intros.
+ change [|0|] with 0 in H.
+ apply Z.compare_eq.
+ now destruct ([|x|] ?= 0).
+ Qed.
+
+ (* Even *)
+
+ Lemma spec_is_even : forall x,
+      if ZnZ.is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1.
+ Proof.
+ unfold ZnZ.is_even; simpl; intros.
+ generalize (spec_div x 2).
+ destruct (x/2)%int as (q,r); intros.
+ unfold compare63.
+ change [|2|] with 2 in H.
+ change [|0|] with 0.
+ destruct H; auto with zarith.
+ replace ([|x|] mod 2) with [|r|].
+ destruct H; auto with zarith.
+ case Z.compare_spec; auto with zarith.
+ apply Zmod_unique with [|q|]; auto with zarith.
+ Qed.
+
+ Global Instance int63_specs : ZnZ.Specs int63_ops := {
+    spec_to_Z   := phi_bounded;
+    spec_of_pos := positive_to_int63_spec;
+    spec_zdigits := spec_zdigits;
+    spec_more_than_1_digit := spec_more_than_1_digit;
+    spec_0   := spec_0;
+    spec_1   := spec_1;
+    spec_m1  := spec_m1;
+    spec_compare := spec_compare;
+    spec_eq0 := spec_eq0;
+    spec_opp_c := spec_opp_c;
+    spec_opp := spec_opp;
+    spec_opp_carry := spec_opp_carry;
+    spec_succ_c := spec_succ_c;
+    spec_add_c := spec_add_c;
+    spec_add_carry_c := spec_add_carry_c;
+    spec_succ := spec_succ;
+    spec_add := spec_add;
+    spec_add_carry := spec_add_carry;
+    spec_pred_c := spec_pred_c;
+    spec_sub_c := spec_sub_c;
+    spec_sub_carry_c := spec_sub_carry_c;
+    spec_pred := spec_pred;
+    spec_sub := spec_sub;
+    spec_sub_carry := spec_sub_carry;
+    spec_mul_c := spec_mul_c;
+    spec_mul := spec_mul;
+    spec_square_c := spec_square_c;
+    spec_div21 := spec_div21;
+    spec_div_gt := fun a b _ => spec_div a b;
+    spec_div := spec_div;
+    spec_modulo_gt := fun a b _ => spec_mod a b;
+    spec_modulo := spec_mod;
+    spec_gcd_gt := fun a b _ => spec_gcd a b;
+    spec_gcd := spec_gcd;
+    spec_head00 := spec_head00;
+    spec_head0 := spec_head0;
+    spec_tail00 := spec_tail00;
+    spec_tail0 := spec_tail0;
+    spec_add_mul_div := spec_add_mul_div;
+    spec_pos_mod := spec_pos_mod;
+    spec_is_even := spec_is_even;
+    spec_sqrt2 := spec_sqrt2;
+    spec_sqrt := spec_sqrt }.
+
+End Int63_Specs.
+
+
+Module Int63Cyclic <: CyclicType.
+  Definition t := int63.
+  Definition ops := int63_ops.
+  Definition specs := int63_specs.
+End Int63Cyclic.
diff --git a/src/versions/standard/Int63/Int63Axioms_standard.v b/src/versions/standard/Int63/Int63Axioms_standard.v
index 6bc1b3c..6a002ea 100644
--- a/src/versions/standard/Int63/Int63Axioms_standard.v
+++ b/src/versions/standard/Int63/Int63Axioms_standard.v
@@ -17,6 +17,7 @@
 
 Require Import Bvector.
 Require Export BigNumPrelude.
+Require Import Int63Lib.
 Require Export Int63Native.
 Require Export Int63Op.
 
@@ -73,34 +74,34 @@ Axiom div_spec : forall x y, [|x / y|] = [|x|] / [|y|].
 Axiom mod_spec : forall x y, [|x \% y|] = [|x|] mod [|y|].
 
 (* Comparisons *)
-Axiom eqb_refl : forall x, (x == x)%int63 = true.
+Axiom eqb_refl : forall x, (x == x)%int = true.
 
-Axiom ltb_spec : forall x y, (x < y)%int63 = true <-> [|x|] < [|y|].
+Axiom ltb_spec : forall x y, (x < y)%int = true <-> [|x|] < [|y|].
 
-Axiom leb_spec : forall x y, (x <= y)%int63 = true <-> [|x|] <= [|y|].
+Axiom leb_spec : forall x y, (x <= y)%int = true <-> [|x|] <= [|y|].
 
 (** Iterators *)
 
 Axiom foldi_cont_gt : forall A B f from to cont,
-  (to < from)%int63 = true -> foldi_cont (A:=A) (B:=B) f from to cont = cont.
+  (to < from)%int = true -> foldi_cont (A:=A) (B:=B) f from to cont = cont.
 
 Axiom foldi_cont_eq : forall A B f from to cont,
   from = to -> foldi_cont (A:=A) (B:=B) f from to cont = f from cont.
 
 Axiom foldi_cont_lt : forall A B f from to cont,
-  (from < to)%int63 = true-> 
-  foldi_cont (A:=A) (B:=B) f from to cont = 
-  f from (fun a' => foldi_cont f (from+1) to cont a').
+  (from < to)%int = true->
+  foldi_cont (A:=A) (B:=B) f from to cont =
+  f from (fun a' => foldi_cont f (from + 1%int) to cont a').
 
 Axiom foldi_down_cont_lt : forall A B f from downto cont,
-  (from < downto)%int63 = true -> foldi_down_cont (A:=A) (B:=B) f from downto cont = cont.
+  (from < downto)%int = true -> foldi_down_cont (A:=A) (B:=B) f from downto cont = cont.
 
 Axiom foldi_down_cont_eq : forall A B f from downto cont,
   from = downto -> foldi_down_cont (A:=A) (B:=B) f from downto cont = f from cont.
 
 Axiom foldi_down_cont_gt : forall A B f from downto cont,
-  (downto < from)%int63 = true-> 
-  foldi_down_cont (A:=A) (B:=B) f from downto cont = 
+  (downto < from)%int = true->
+  foldi_down_cont (A:=A) (B:=B) f from downto cont =
   f from (fun a' => foldi_down_cont f (from-1) downto cont a').
 
 (** Print *)
@@ -117,11 +118,11 @@ Axiom head0_spec  : forall x,  0 < [|x|] ->
 Axiom tail0_spec  : forall x, 0 < [|x|] ->
          (exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|tail0 x|]))%Z.
 
-Axiom addc_def_spec : forall x y, (x +c y)%int63 = addc_def x y.
+Axiom addc_def_spec : forall x y, (x +c y)%int = addc_def x y.
 
 Axiom addcarryc_def_spec : forall x y, addcarryc x y = addcarryc_def x y.
 
-Axiom subc_def_spec : forall x y, (x -c y)%int63 = subc_def x y.
+Axiom subc_def_spec : forall x y, (x -c y)%int = subc_def x y.
 
 Axiom subcarryc_def_spec : forall x y, subcarryc x y = subcarryc_def x y.
 
diff --git a/src/versions/standard/Int63/Int63Lib_standard.v b/src/versions/standard/Int63/Int63Lib_standard.v
new file mode 100644
index 0000000..9f10adb
--- /dev/null
+++ b/src/versions/standard/Int63/Int63Lib_standard.v
@@ -0,0 +1,454 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
+
+Require Import NaryFunctions.
+Require Import Wf_nat.
+Require Export ZArith.
+Require Export DoubleType.
+
+(** * 63-bit integers *)
+
+(** This file contains basic definitions of a 63-bit integer arithmetic.
+  It is based on the Int31 library, using its genericity. *)
+
+Definition size := 63%nat.
+
+(** Digits *)
+
+Inductive digits : Type := D0 | D1.
+
+(** The type of 63-bit integers *)
+
+(** The type [int63] has a unique constructor [I63] that expects
+   63 arguments of type [digits]. *)
+
+Definition digits63 t := Eval compute in nfun digits size t.
+
+Inductive int63 : Type := I63 : digits63 int63.
+
+Notation int := int63.
+
+(* spiwack: Registration of the type of integers, so that the matchs in
+   the functions below perform dynamic decompilation (otherwise some segfault
+   occur when they are applied to one non-closed term and one closed term). *)
+
+Delimit Scope int63_scope with int.
+Bind Scope int63_scope with int.
+Local Open Scope int63_scope.
+
+(** * Constants *)
+
+(** Zero is [I63 D0 ... D0] *)
+Definition On : int63 := Eval compute in napply_cst _ _ D0 size I63.
+Notation "0" := On : int63_scope.
+
+(** One is [I63 D0 ... D0 D1] *)
+Definition In : int63 := Eval compute in (napply_cst _ _ D0 (size-1) I63) D1.
+Notation "1" := In : int63_scope.
+
+(** The biggest integer is [I63 D1 ... D1], corresponding to [(2^size)-1] *)
+Definition Tn : int63 := Eval compute in napply_cst _ _ D1 size I63.
+
+(** Two is [I63 D0 ... D0 D1 D0] *)
+Definition Twon : int63 := Eval compute in (napply_cst _ _ D0 (size-2) I63) D1 D0.
+Notation "2" := Twon : int63_scope.
+
+(** * Bits manipulation *)
+
+
+(** [sneakr b x] shifts [x] to the right by one bit.
+   Rightmost digit is lost while leftmost digit becomes [b].
+   Pseudo-code is
+    [ match x with (I63 d0 ... dN) => I63 b d0 ... d(N-1) end ]
+*)
+
+Definition sneakr : digits -> int63 -> int63 := Eval compute in
+ fun b => int63_rect _ (napply_except_last _ _ (size-1) (I63 b)).
+
+(** [sneakl b x] shifts [x] to the left by one bit.
+   Leftmost digit is lost while rightmost digit becomes [b].
+   Pseudo-code is
+    [ match x with (I63 d0 ... dN) => I63 d1 ... dN b end ]
+*)
+
+Definition sneakl : digits -> int63 -> int63 := Eval compute in
+ fun b => int63_rect _ (fun _ => napply_then_last _ _ b (size-1) I63).
+
+
+(** [shiftl], [shiftr], [twice] and [twice_plus_one] are direct
+    consequences of [sneakl] and [sneakr]. *)
+
+Definition shiftl := sneakl D0.
+Definition shiftr := sneakr D0.
+Definition twice := sneakl D0.
+Definition twice_plus_one := sneakl D1.
+
+(** [firstl x] returns the leftmost digit of number [x].
+    Pseudo-code is [ match x with (I63 d0 ... dN) => d0 end ] *)
+
+Definition firstl : int63 -> digits := Eval compute in
+ int63_rect _ (fun d => napply_discard _ _ d (size-1)).
+
+(** [firstr x] returns the rightmost digit of number [x].
+    Pseudo-code is [ match x with (I63 d0 ... dN) => dN end ] *)
+
+Definition firstr : int63 -> digits := Eval compute in
+ int63_rect _ (napply_discard _ _ (fun d=>d) (size-1)).
+
+(** [iszero x] is true iff [x = I63 D0 ... D0]. Pseudo-code is
+    [ match x with (I63 D0 ... D0) => true | _ => false end ] *)
+
+Definition iszero : int63 -> bool := Eval compute in
+ let f d b := match d with D0 => b | D1 => false end
+ in int63_rect _ (nfold_bis _ _ f true size).
+
+(* NB: DO NOT transform the above match in a nicer (if then else).
+   It seems to work, but later "unfold iszero" takes forever. *)
+
+
+(** [base] is [2^63], obtained via iterations of [Z.double].
+   It can also be seen as the smallest b > 0 s.t. phi_inv b = 0
+   (see below) *)
+
+Definition base := Eval compute in
+ iter_nat size Z Z.double 1%Z.
+
+(** * Recursors *)
+
+Fixpoint recl_aux (n:nat)(A:Type)(case0:A)(caserec:digits->int63->A->A)
+ (i:int63) : A :=
+  match n with
+  | O => case0
+  | S next =>
+          if iszero i then
+             case0
+          else
+             let si := shiftl i in
+             caserec (firstl i) si (recl_aux next A case0 caserec si)
+  end.
+
+Fixpoint recr_aux (n:nat)(A:Type)(case0:A)(caserec:digits->int63->A->A)
+ (i:int63) : A :=
+  match n with
+  | O => case0
+  | S next =>
+          if iszero i then
+             case0
+          else
+             let si := shiftr i in
+             caserec (firstr i) si (recr_aux next A case0 caserec si)
+  end.
+
+Definition recl := recl_aux size.
+Definition recr := recr_aux size.
+
+(** * Conversions *)
+
+(** From int63 to Z, we simply iterates [Z.double] or [Z.succ_double]. *)
+
+Definition phi : int63 -> Z :=
+ recr Z (0%Z)
+  (fun b _ => match b with D0 => Z.double | D1 => Z.succ_double end).
+
+(** From positive to int63. An abstract definition could be :
+      [ phi_inv (2n) = 2*(phi_inv n) /\
+        phi_inv 2n+1 = 2*(phi_inv n) + 1 ] *)
+
+Fixpoint phi_inv_positive p :=
+  match p with
+    | xI q => twice_plus_one (phi_inv_positive q)
+    | xO q => twice (phi_inv_positive q)
+    | xH => In
+  end.
+
+(** The negative part : 2-complement  *)
+
+Fixpoint complement_negative p :=
+  match p with
+    | xI q => twice (complement_negative q)
+    | xO q => twice_plus_one (complement_negative q)
+    | xH => twice Tn
+  end.
+
+(** A simple incrementation function *)
+
+Definition incr : int63 -> int63 :=
+ recr int63 In
+   (fun b si rec => match b with
+     | D0 => sneakl D1 si
+     | D1 => sneakl D0 rec end).
+
+(** We can now define the conversion from Z to int63. *)
+
+Definition phi_inv : Z -> int63 := fun n =>
+ match n with
+ | Z0 => On
+ | Zpos p => phi_inv_positive p
+ | Zneg p => incr (complement_negative p)
+ end.
+
+(** [phi_inv2] is similar to [phi_inv] but returns a double word
+    [zn2z int63] *)
+
+Definition phi_inv2 n :=
+  match n with
+  | Z0 => W0
+  | _ => WW (phi_inv (n/base)%Z) (phi_inv n)
+  end.
+
+(** [phi2] is similar to [phi] but takes a double word (two args) *)
+
+Definition phi2 nh nl :=
+  ((phi nh)*base+(phi nl))%Z.
+
+(** * Addition *)
+
+(** Addition modulo [2^63] *)
+
+Definition add63 (n m : int63) := phi_inv ((phi n)+(phi m)).
+Notation "n + m" := (add63 n m) : int63_scope.
+
+(** Addition with carry (the result is thus exact) *)
+
+(* spiwack : when executed in non-compiled*)
+(* mode, (phi n)+(phi m) is computed twice*)
+(* it may be considered to optimize it *)
+
+Definition add63c (n m : int63) :=
+  let npm := n+m in
+  match (phi npm ?= (phi n)+(phi m))%Z with
+  | Eq => C0 npm
+  | _ => C1 npm
+  end.
+Notation "n '+c' m" := (add63c n m) (at level 50, no associativity) : int63_scope.
+
+(**  Addition plus one with carry (the result is thus exact) *)
+
+Definition add63carryc (n m : int63) :=
+  let npmpone_exact := ((phi n)+(phi m)+1)%Z in
+  let npmpone := phi_inv npmpone_exact in
+  match (phi npmpone ?= npmpone_exact)%Z with
+  | Eq => C0 npmpone
+  | _ => C1 npmpone
+  end.
+
+(** * Substraction *)
+
+(** Subtraction modulo [2^63] *)
+
+Definition sub63 (n m : int63) := phi_inv ((phi n)-(phi m)).
+Notation "n - m" := (sub63 n m) : int63_scope.
+
+(** Subtraction with carry (thus exact) *)
+
+Definition sub63c (n m : int63) :=
+  let nmm := n-m in
+  match (phi nmm ?= (phi n)-(phi m))%Z with
+  | Eq => C0 nmm
+  | _ => C1 nmm
+  end.
+Notation "n '-c' m" := (sub63c n m) (at level 50, no associativity) : int63_scope.
+
+(** subtraction minus one with carry (thus exact) *)
+
+Definition sub63carryc (n m : int63) :=
+  let nmmmone_exact := ((phi n)-(phi m)-1)%Z in
+  let nmmmone := phi_inv nmmmone_exact in
+  match (phi nmmmone ?= nmmmone_exact)%Z with
+  | Eq => C0 nmmmone
+  | _ => C1 nmmmone
+  end.
+
+(** Opposite *)
+
+Definition opp63 x := On - x.
+Notation "- x" := (opp63 x) : int63_scope.
+
+(** Multiplication *)
+
+(** multiplication modulo [2^63] *)
+
+Definition mul63 (n m : int63) := phi_inv ((phi n)*(phi m)).
+Notation "n * m" := (mul63 n m) : int63_scope.
+
+(** multiplication with double word result (thus exact) *)
+
+Definition mul63c (n m : int63) := phi_inv2 ((phi n)*(phi m)).
+Notation "n '*c' m" := (mul63c n m) (at level 40, no associativity) : int63_scope.
+
+
+(** * Division *)
+
+(** Division of a double size word modulo [2^63] *)
+
+Definition div6321 (nh nl m : int63) :=
+  let (q,r) := Z.div_eucl (phi2 nh nl) (phi m) in
+  (phi_inv q, phi_inv r).
+
+(** Division modulo [2^63] *)
+
+Definition div63 (n m : int63) :=
+  let (q,r) := Z.div_eucl (phi n) (phi m) in
+  (phi_inv q, phi_inv r).
+Notation "n / m" := (div63 n m) : int63_scope.
+
+
+(** * Unsigned comparison *)
+
+Definition compare63 (n m : int63) := ((phi n)?=(phi m))%Z.
+Notation "n ?= m" := (compare63 n m) (at level 70, no associativity) : int63_scope.
+
+Definition eqb63 (n m : int63) :=
+ match n ?= m with Eq => true | _ => false end.
+
+
+(** Computing the [i]-th iterate of a function:
+    [iter_int63 i A f = f^i] *)
+
+Definition iter_int63 i A f :=
+  recr (A->A) (fun x => x)
+   (fun b si rec => match b with
+      | D0 => fun x => rec (rec x)
+      | D1 => fun x => f (rec (rec x))
+    end)
+    i.
+
+(** Combining the [(63-p)] low bits of [i] above the [p] high bits of [j]:
+    [addmuldiv63 p i j = i*2^p+j/2^(63-p)]  (modulo [2^63]) *)
+
+Definition addmuldiv63 p i j :=
+ let (res, _ ) :=
+ iter_int63 p (int63*int63)
+  (fun ij => let (i,j) := ij in (sneakl (firstl j) i, shiftl j))
+  (i,j)
+ in
+ res.
+
+
+Fixpoint euler (guard:nat) (i j:int63) {struct guard} :=
+  match guard with
+    | O => In
+    | S p => match j ?= On with
+               | Eq => i
+               | _ => euler p j (let (_, r ) := i/j in r)
+             end
+  end.
+
+Definition gcd63 (i j:int63) := euler (2*size)%nat i j.
+
+(** Square root functions using newton iteration
+    we use a very naive upper-bound on the iteration
+    2^63 instead of the usual 63.
+**)
+
+
+
+Definition sqrt63_step (rec: int63 -> int63 -> int63) (i j: int63)  :=
+Eval lazy delta [Twon] in
+  let (quo,_) := i/j in
+  match quo ?= j with
+    Lt => rec i (fst ((j + quo)/Twon))
+  | _ =>  j
+  end.
+
+Fixpoint iter63_sqrt (n: nat) (rec: int63 -> int63 -> int63)
+          (i j: int63) {struct n} : int63 :=
+  sqrt63_step
+   (match n with
+      O =>  rec
+   | S n => (iter63_sqrt n (iter63_sqrt n rec))
+   end) i j.
+
+Definition sqrt63 i :=
+Eval lazy delta [On In Twon] in
+  match compare63 In i with
+    Gt => On
+  | Eq => In
+  | Lt => iter63_sqrt 63 (fun i j => j) i (fst (i/Twon))
+  end.
+
+Definition v30 := Eval compute in (addmuldiv63 (phi_inv (Z.of_nat size - 1)) In On).
+
+Definition sqrt632_step (rec: int63 -> int63 -> int63 -> int63)
+   (ih il j: int63)  :=
+Eval lazy delta [Twon v30] in
+  match ih ?= j with Eq => j | Gt => j | _ =>
+  let (quo,_) := div6321 ih il j in
+  match quo ?= j with
+    Lt => let m := match j +c quo with
+                    C0 m1 => fst (m1/Twon)
+                  | C1 m1 => fst (m1/Twon) + v30
+                  end in rec ih il m
+  | _ =>  j
+  end end.
+
+Fixpoint iter632_sqrt (n: nat)
+          (rec: int63  -> int63 -> int63 -> int63)
+          (ih il j: int63) {struct n} : int63 :=
+  sqrt632_step
+   (match n with
+      O =>  rec
+   | S n => (iter632_sqrt n (iter632_sqrt n rec))
+   end) ih il j.
+
+Definition sqrt632 ih il :=
+Eval lazy delta [On In] in
+  let s := iter632_sqrt 63 (fun ih il j => j) ih il Tn in
+           match s *c s with
+            W0 => (On, C0 On) (* impossible *)
+          | WW ih1 il1 =>
+             match il -c il1 with
+                C0 il2 =>
+                  match ih ?= ih1 with
+                    Gt => (s, C1 il2)
+                  | _  => (s, C0 il2)
+                  end
+              | C1 il2 =>
+                  match (ih - In) ?= ih1 with (* we could parametrize ih - 1 *)
+                    Gt => (s, C1 il2)
+                  | _  => (s, C0 il2)
+                  end
+              end
+          end.
+
+
+Fixpoint p2i n p : (N*int63)%type :=
+  match n with
+    | O => (Npos p, On)
+    | S n => match p with
+               | xO p => let (r,i) := p2i n p in (r, Twon*i)
+               | xI p => let (r,i) := p2i n p in (r, Twon*i+In)
+               | xH => (N0, In)
+             end
+  end.
+
+Definition positive_to_int63 (p:positive) := p2i size p.
+
+(** Constant 63 converted into type int63.
+    It is used as default answer for numbers of zeros
+    in [head0] and [tail0] *)
+
+Definition T63 : int63 := Eval compute in phi_inv (Z.of_nat size).
+
+Definition head063 (i:int63) :=
+  recl _ (fun _ => T63)
+   (fun b si rec n => match b with
+     | D0 => rec (add63 n In)
+     | D1 => n
+    end)
+   i On.
+
+Definition tail063 (i:int63) :=
+  recr _ (fun _ => T63)
+   (fun b si rec n => match b with
+     | D0 => rec (add63 n In)
+     | D1 => n
+    end)
+   i On.
diff --git a/src/versions/standard/Int63/Int63Native_standard.v b/src/versions/standard/Int63/Int63Native_standard.v
index 3a263d2..ada4821 100644
--- a/src/versions/standard/Int63/Int63Native_standard.v
+++ b/src/versions/standard/Int63/Int63Native_standard.v
@@ -15,92 +15,162 @@
 (**************************************************************************)
 
 
+(* Add LoadPath "." as SMTCoq.Int63.standard.versions. *)
 Require Export DoubleType.
+Require Import Int63Lib Cyclic63 Ring63.
+Require Import ZArith.
+Require Import Bool.
 
-RegisterInd bool as ind_bool.
-RegisterInd prod as ind_pair. 
-RegisterInd carry as ind_carry.
-RegisterInd comparison as ind_cmp.
-RegisterInd eq as ind_eq.
 
-Definition size := 63%nat.
+Definition size := size.
 
-Register int : Set as int63_type.
+Notation int := int63.
 
-Delimit Scope int63_scope with int63.
+Delimit Scope int63_scope with int.
 Bind Scope int63_scope with int.
 
+(* Some constants *)
+Notation "0" := On : int63_scope.
+Notation "1" := In : int63_scope.
+Notation "2" := Twon : int63_scope.
+
 (* Logical operations *)
-Register lsl  : int -> int -> int as int63_lsl.
+Definition lsl : int -> int -> int :=
+  fun i j => nshiftl (N.to_nat (Z.to_N (phi j))) i.
 Infix "<<" := lsl (at level 30, no associativity) : int63_scope.
 
-Register lsr  : int -> int -> int as int63_lsr.
+Definition lsr : int -> int -> int :=
+  fun i j => nshiftr (N.to_nat (Z.to_N (phi j))) i.
 Infix ">>" := lsr (at level 30, no associativity) : int63_scope.
 
-Register land : int -> int -> int as int63_land.
+Definition land : int -> int -> int :=
+  fun i j =>
+    recrter _ j (fun d _ acc =>
+                   let r := acc in
+                   let d' := firstl r in
+                   let dr := match d, d' with | D1, D1 => D1 | _, _ => D0 end in
+                   sneakl dr r
+                ) i.
 Infix "land" := land (at level 40, left associativity) : int63_scope.
 
-Register lor  : int -> int -> int as int63_lor.
+Definition lor : int -> int -> int :=
+  fun i j =>
+    recrter _ j (fun d _ acc =>
+                   let r := acc in
+                   let d' := firstl r in
+                   let dr := match d, d' with | D0, D0 => D0 | _, _ => D1 end in
+                   sneakl dr r
+                ) i.
 Infix "lor" := lor (at level 40, left associativity) : int63_scope.
 
-Register lxor : int -> int -> int as int63_lxor.
+Definition lxor : int -> int -> int :=
+  fun i j =>
+    recrter _ j (fun d _ acc =>
+                   let r := acc in
+                   let d' := firstl r in
+                   let dr := match d, d' with | D0, D0 | D1, D1 => D0 | _, _ => D1 end in
+                   sneakl dr r
+                ) i.
 Infix "lxor" := lxor (at level 40, left associativity) : int63_scope.
 
 (* Arithmetic modulo operations *)
-Register add : int -> int -> int as int63_add.
-Notation "n + m" := (add n m) : int63_scope.
-
-Register sub : int -> int -> int as int63_sub.
-Notation "n - m" := (sub n m) : int63_scope.
-
-Register mul : int -> int -> int as int63_mul.
-Notation "n * m" := (mul n m) : int63_scope.
-
-Register mulc : int -> int -> int * int as int63_mulc.
-
-Register div : int -> int -> int as int63_div.
+(* Definition add : int -> int -> int := add63. *)
+(* Notation "n + m" := (add n m) : int63_scope. *)
+Notation "n + m" := (add63 n m) : int63_scope.
+
+(* Definition sub : int -> int -> int := sub63. *)
+(* Notation "n - m" := (sub n m) : int63_scope. *)
+Notation "n - m" := (sub63 n m) : int63_scope.
+
+(* Definition mul : int -> int -> int := mul63. *)
+(* Notation "n * m" := (mul n m) : int63_scope. *)
+Notation "n * m" := (mul63 n m) : int63_scope.
+
+Definition mulc : int -> int -> int * int :=
+  fun i j => match mul63c i j with
+               | W0 => (0%int, 0%int)
+               | WW h l => (h, l)
+             end.
+
+Definition div : int -> int -> int :=
+  fun i j => let (q,_) := div63 i j in q.
 Notation "n / m" := (div n m) : int63_scope.
 
-Register mod : int -> int -> int as int63_mod.
-Notation "n '\%' m" := (mod n m) (at level 40, left associativity) : int63_scope.
+Definition modulo : int -> int -> int :=
+  fun i j => let (_,r) := div63 i j in r.
+Notation "n '\%' m" := (modulo n m) (at level 40, left associativity) : int63_scope.
 
 (* Comparisons *)
-Register eqb : int -> int -> bool as int63_eq.
+(* We do not use eqb63 to be able to easily prove eqb_correct *)
+(* Definition eqb_digits d1 d2 := *)
+(*   match d1, d2 with *)
+(*     | D0, D0 | D1, D1 => true *)
+(*     | _, _ => false *)
+(*   end. *)
+
+(* Definition eqb i j := *)
+(*   match i, j with *)
+(*     | I63 d0 d1 d2 d3 d4 d5 d6 d7 d8 d9 d10 d11 d12 d13 d14 d15 d16 d17 d18 d19 d20 d21 d22 d23 d24 d25 d26 d27 d28 d29 d30 d31 d32 d33 d34 d35 d36 d37 d38 d39 d40 d41 d42 d43 d44 d45 d46 d47 d48 d49 d50 d51 d52 d53 d54 d55 d56 d57 d58 d59 d60 d61 d62, I63 d'0 d'1 d'2 d'3 d'4 d'5 d'6 d'7 d'8 d'9 d'10 d'11 d'12 d'13 d'14 d'15 d'16 d'17 d'18 d'19 d'20 d'21 d'22 d'23 d'24 d'25 d'26 d'27 d'28 d'29 d'30 d'31 d'32 d'33 d'34 d'35 d'36 d'37 d'38 d'39 d'40 d'41 d'42 d'43 d'44 d'45 d'46 d'47 d'48 d'49 d'50 d'51 d'52 d'53 d'54 d'55 d'56 d'57 d'58 d'59 d'60 d'61 d'62 => *)
+(*       (eqb_digits d0 d'0) && (eqb_digits d1 d'1) && (eqb_digits d2 d'2) && (eqb_digits d3 d'3) && (eqb_digits d4 d'4) && (eqb_digits d5 d'5) && (eqb_digits d6 d'6) && (eqb_digits d7 d'7) && (eqb_digits d8 d'8) && (eqb_digits d9 d'9) && (eqb_digits d10 d'10) && (eqb_digits d11 d'11) && (eqb_digits d12 d'12) && (eqb_digits d13 d'13) && (eqb_digits d14 d'14) && (eqb_digits d15 d'15) && (eqb_digits d16 d'16) && (eqb_digits d17 d'17) && (eqb_digits d18 d'18) && (eqb_digits d19 d'19) && (eqb_digits d20 d'20) && (eqb_digits d21 d'21) && (eqb_digits d22 d'22) && (eqb_digits d23 d'23) && (eqb_digits d24 d'24) && (eqb_digits d25 d'25) && (eqb_digits d26 d'26) && (eqb_digits d27 d'27) && (eqb_digits d28 d'28) && (eqb_digits d29 d'29) && (eqb_digits d30 d'30) && (eqb_digits d31 d'31) && (eqb_digits d32 d'32) && (eqb_digits d33 d'33) && (eqb_digits d34 d'34) && (eqb_digits d35 d'35) && (eqb_digits d36 d'36) && (eqb_digits d37 d'37) && (eqb_digits d38 d'38) && (eqb_digits d39 d'39) && (eqb_digits d40 d'40) && (eqb_digits d41 d'41) && (eqb_digits d42 d'42) && (eqb_digits d43 d'43) && (eqb_digits d44 d'44) && (eqb_digits d45 d'45) && (eqb_digits d46 d'46) && (eqb_digits d47 d'47) && (eqb_digits d48 d'48) && (eqb_digits d49 d'49) && (eqb_digits d50 d'50) && (eqb_digits d51 d'51) && (eqb_digits d52 d'52) && (eqb_digits d53 d'53) && (eqb_digits d54 d'54) && (eqb_digits d55 d'55) && (eqb_digits d56 d'56) && (eqb_digits d57 d'57) && (eqb_digits d58 d'58) && (eqb_digits d59 d'59) && (eqb_digits d60 d'60) && (eqb_digits d61 d'61) && (eqb_digits d62 d'62) *)
+(*   end. *)
+Definition eqb := eqb63.
 Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : int63_scope.
 
-Register ltb : int -> int -> bool as int63_lt.
+Definition ltb : int -> int -> bool :=
+  fun i j => match compare63 i j with | Lt => true | _ => false end.
 Notation "m < n" := (ltb m n) : int63_scope.
 
-Register leb : int -> int -> bool as int63_le.
+Definition leb : int -> int -> bool :=
+  fun i j => match compare63 i j with | Gt => false | _ => true end.
 Notation "m <= n" := (leb m n) : int63_scope.
 
 (* This operator has the following reduction rule
      eqb_correct i i (eq_refl true) ---> (eq_refl i) *)
-Register eqb_correct : forall i j, (i==j)%int63 = true -> i = j as int63_eqb_correct.
+(* Lemma eqb_digits_correct : *)
+(*   forall d1 d2, eqb_digits d1 d2 = true <-> d1 = d2. *)
+(* Proof. intros [|] [|]; split; try reflexivity; discriminate. Defined. *)
+
+(* Lemma andb_true_iff : forall b1 b2, *)
+(*   b1 && b2 = true <-> b1 = true /\ b2 = true. *)
+(* Proof. intros [|] [|]; repeat split; try reflexivity; try discriminate; intros [H1 H2]; discriminate. Defined. *)
+
+Lemma eqb_correct : forall i j, (i==j)%int = true -> i = j.
+Admitted.
+(* Proof. *)
+(*   unfold eqb. intros [d0 d1 d2 d3 d4 d5 d6 d7 d8 d9 d10 d11 d12 d13 d14 d15 d16 d17 d18 d19 d20 d21 d22 d23 d24 d25 d26 d27 d28 d29 d30 d31 d32 d33 d34 d35 d36 d37 d38 d39 d40 d41 d42 d43 d44 d45 d46 d47 d48 d49 d50 d51 d52 d53 d54 d55 d56 d57 d58 d59 d60 d61 d62] [d'0 d'1 d'2 d'3 d'4 d'5 d'6 d'7 d'8 d'9 d'10 d'11 d'12 d'13 d'14 d'15 d'16 d'17 d'18 d'19 d'20 d'21 d'22 d'23 d'24 d'25 d'26 d'27 d'28 d'29 d'30 d'31 d'32 d'33 d'34 d'35 d'36 d'37 d'38 d'39 d'40 d'41 d'42 d'43 d'44 d'45 d'46 d'47 d'48 d'49 d'50 d'51 d'52 d'53 d'54 d'55 d'56 d'57 d'58 d'59 d'60 d'61 d'62]. *)
+(*   do 62 (rewrite andb_true_iff; intros [H1 H2]; rewrite eqb_digits_correct in H2; subst; revert H1). *)
+(*   rewrite eqb_digits_correct. intros ->. reflexivity. *)
+(* Defined. *)
 
 
 (* Iterators *)
-Register foldi_cont : 
-   forall 
+
+Definition foldi_cont
      {A B     : Type}
-     (f       : int -> (A -> B) -> A -> B) 
+     (f       : int -> (A -> B) -> A -> B)
      (from to : int)
-     (cont    : A -> B), 
-     A -> B
-     as int63_foldi.
-
-Register foldi_down_cont : 
-  forall 
+     (cont    : A -> B)                      : A -> B :=
+  if ltb to from then
+    cont
+  else
+    let (_,r) := iter_int63 (to - from) _ (fun (jy: (int * (A -> B))%type) =>
+                     let (j,y) := jy in ((j+1)%int, f j y)
+                                      ) (from, cont) in
+    f to r.
+
+Definition foldi_down_cont
     {A B         : Type}
     (f           : int -> (A -> B) -> A -> B)
     (from downto : int)
-    (cont        : A -> B),
-    A -> B
-    as int63_foldi_down.
-
-(* Print *)
-
-Register print_int : int -> int as int63_print.
-
-
-
+    (cont        : A -> B)                      : A -> B :=
+  if ltb from downto then
+    cont
+  else
+    let (_,r) := iter_int63 (from - downto) _ (fun (jy: (int * (A -> B))%type) =>
+                     let (j,y) := jy in ((j-1)%int, f j y)
+                                      ) (from, cont) in
+    f downto r.
+
+(* Fake print *)
+
+Definition print_int : int -> int := fun i => i.
diff --git a/src/versions/standard/Int63/Int63Op_standard.v b/src/versions/standard/Int63/Int63Op_standard.v
index 933a045..119e6bd 100644
--- a/src/versions/standard/Int63/Int63Op_standard.v
+++ b/src/versions/standard/Int63/Int63Op_standard.v
@@ -15,38 +15,34 @@
 (**************************************************************************)
 
 
+Require Import Int63Lib Cyclic63.
 Require Export Int63Native.
 Require Import BigNumPrelude.
 Require Import Bvector.
 
-Set Vm Optimize.
-
 
 Local Open Scope int63_scope.
 
 (** The number of digits as a int *)
-Definition digits := 63.
+Definition digits := zdigits.
 
 (** The bigger int *)
 Definition max_int := Eval vm_compute in 0 - 1.
-Register max_int as PrimInline.
 
 (** Access to the nth digits *)
 Definition get_digit x p := (0 < (x land (1 << p))).
 
 Definition set_digit x p (b:bool) :=
-  if (0 <= p) && (p < digits) then 
+  if (0 <= p) && (p < digits) then
     if b then x lor (1 << p)
     else x land (max_int lxor (1 << p))
   else x.
 
 (** Equality to 0 *)
 Definition is_zero (i:int) := i == 0.
-Register is_zero as PrimInline.
 
 (** Parity *)
 Definition is_even (i:int) := is_zero (i land 1).
-Register is_even as PrimInline.
 
 (** Bit *)
 
@@ -55,100 +51,88 @@ Definition bit i n :=  negb (is_zero ((i >> n) << (digits - 1))).
 
 (** Extra modulo operations *)
 Definition opp (i:int) := 0 - i.
-Register opp as PrimInline.
 Notation "- x" := (opp x) : int63_scope.
 
 Definition oppcarry i := max_int - i.
-Register oppcarry as PrimInline.
 
 Definition succ i := i + 1.
-Register succ as PrimInline.
 
 Definition pred i := i - 1.
-Register pred as PrimInline.
 
 Definition addcarry i j := i + j + 1.
-Register addcarry as PrimInline.
 
 Definition subcarry i j := i - j - 1.
-Register subcarry as PrimInline.
 
 (** Exact arithmetic operations *)
 
 Definition addc_def x y :=
   let r := x + y in
   if r < x then C1 r else C0 r.
-(* the same but direct implementation for effeciancy *)
-Register addc      : int -> int -> carry int as int63_addc.
+(* the same but direct implementation for efficiancy *)
+Definition addc : int -> int -> carry int := add63c.
 Notation "n '+c' m" := (addc n m) (at level 50, no associativity) : int63_scope.
 
 Definition addcarryc_def x y :=
   let r := addcarry x y in
   if r <= x then C1 r else C0 r.
-(* the same but direct implementation for effeciancy *)
-Register addcarryc : int -> int -> carry int as int63_addcarryc.
+(* the same but direct implementation for efficiancy *)
+Definition addcarryc : int -> int -> carry int := add63carryc.
 
-Definition subc_def x y := 
+Definition subc_def x y :=
   if y <= x then C0 (x - y) else C1 (x - y).
-(* the same but direct implementation for effeciancy *)
-Register subc      : int -> int -> carry int as int63_subc.
+(* the same but direct implementation for efficiancy *)
+Definition subc : int -> int -> carry int := sub63c.
 Notation "n '-c' m" := (subc n m) (at level 50, no associativity) : int63_scope.
 
 Definition subcarryc_def x y :=
   if y < x then C0 (x - y - 1) else C1 (x - y - 1).
-(* the same but direct implementation for effeciancy *)
-Register subcarryc : int -> int -> carry int as int63_subcarryc.
+(* the same but direct implementation for efficiancy *)
+Definition subcarryc : int -> int -> carry int := sub63carryc.
 
 Definition diveucl_def x y := (x/y, x\%y).
-(* the same but direct implementation for effeciancy *) 
-Register diveucl   : int -> int -> int * int as int63_diveucl.
+(* the same but direct implementation for efficiancy *)
+Definition diveucl : int -> int -> int * int := div63.
 
-Register diveucl_21    : int -> int -> int -> int * int as int63_div21.
+Definition diveucl_21 : int -> int -> int -> int * int := div6321.
 
 Definition addmuldiv_def p x y :=
   (x << p) lor (y >> (digits - p)).
-Register addmuldiv   : int -> int -> int -> int as int63_addmuldiv.
+(* the same but direct implementation for efficiancy *)
+Definition addmuldiv : int -> int -> int -> int := addmuldiv63.
 
 Definition oppc (i:int) := 0 -c i.
-Register oppc as PrimInline.
 
 Definition succc i := i +c 1.
-Register succc as PrimInline.
 
 Definition predc i := i -c 1.
-Register predc as PrimInline.
 
 (** Comparison *)
 Definition compare_def x y :=
-  if x < y then Lt 
+  if x < y then Lt
   else if (x == y) then Eq else Gt.
 
-Register compare : int -> int -> comparison as int63_compare.
+Definition compare : int -> int -> comparison := compare63.
 Notation "n ?= m" := (compare n m) (at level 70, no associativity) : int63_scope.
 
 (** Exotic operations *)
 
 (** I should add the definition (like for compare) *)
-Register head0 : int -> int as int63_head0.
-Register tail0 : int -> int as int63_tail0.
+Definition head0 : int -> int := head063.
+Definition tail0 : int -> int := tail063.
 
 (** Iterators *)
 
 Definition foldi {A} (f:int -> A -> A) from to :=
   foldi_cont (fun i cont a => cont (f i a)) from to (fun a => a).
-Register foldi as PrimInline.
 
 Definition fold {A} (f: A -> A) from to :=
   foldi_cont (fun i cont a => cont (f a)) from to (fun a => a).
-Register fold as PrimInline.
 
 Definition foldi_down {A} (f:int -> A -> A) from downto :=
   foldi_down_cont (fun i cont a => cont (f i a)) from downto (fun a => a).
-Register foldi_down as PrimInline.
 
 Definition fold_down {A} (f:A -> A) from downto :=
   foldi_down_cont (fun i cont a => cont (f a)) from downto (fun a => a).
-Register fold_down as PrimInline.
 
 Definition forallb (f:int -> bool) from to :=
   foldi_cont (fun i cont _ => if f i then cont tt else false) from to (fun _ => true) tt.
@@ -158,17 +142,19 @@ Definition existsb (f:int -> bool) from to :=
 
 (** Translation to Z *)
 
-Fixpoint to_Z_rec (n:nat) (i:int) :=
-  match n with 
-  | O => 0%Z 
-  | S n => 
-    (if is_even i then Zdouble else Zdouble_plus_one) (to_Z_rec n (i >> 1))
-  end.
+(* Fixpoint to_Z_rec (n:nat) (i:int) := *)
+(*   match n with *)
+(*   | O => 0%Z *)
+(*   | S n => *)
+(*     (if is_even i then Zdouble else Zdouble_plus_one) (to_Z_rec n (i >> 1)) *)
+(*   end. *)
 
-Definition to_Z := to_Z_rec size.
+(* Definition to_Z := to_Z_rec size. *)
+
+Definition to_Z := phi.
 
 Fixpoint of_pos_rec (n:nat) (p:positive) :=
-  match n, p with 
+  match n, p with
   | O, _ => 0
   | S n, xH => 1
   | S n, xO p => (of_pos_rec n p) << 1
@@ -177,7 +163,7 @@ Fixpoint of_pos_rec (n:nat) (p:positive) :=
 
 Definition of_pos := of_pos_rec size.
 
-Definition of_Z z := 
+Definition of_Z z :=
   match z with
   | Zpos p => of_pos p
   | Z0 => 0
@@ -227,7 +213,7 @@ Definition sqrt2_step (rec: int -> int -> int -> int)
       match j +c quo with
       | C0 m1 => rec ih il (m1 >> 1)
       | C1 m1 => rec ih il ((m1 >> 1) + high_bit)
-      end 
+      end
     else j
   else j.
 
@@ -237,7 +223,7 @@ Definition iter2_sqrt :=
           (rec: int  -> int -> int -> int)
           (ih il j: int) {struct n} : int :=
   sqrt2_step
-   (fun ih il j => 
+   (fun ih il j =>
      match n with
      | O =>  rec ih il j
      | S n => (iter2_sqrt n (iter2_sqrt n rec)) ih il j
@@ -254,7 +240,7 @@ Definition sqrt2 ih il :=
   end.
 
 (* Extra function on equality *)
- 
+
 Definition cast i j :=
      (if i == j as b return ((b = true -> i = j) -> option (forall P : int -> Type, P i -> P j))
       then fun Heq : true = true -> i = j =>
diff --git a/src/versions/standard/Int63/Int63Properties_standard.v b/src/versions/standard/Int63/Int63Properties_standard.v
index 37fc128..e61714a 100644
--- a/src/versions/standard/Int63/Int63Properties_standard.v
+++ b/src/versions/standard/Int63/Int63Properties_standard.v
@@ -17,8 +17,10 @@
 
 Require Import Zgcd_alt.
 Require Import Bvector.
+Require Import Int63Lib Cyclic63.
 Require Export Int63Axioms.
 Require Import Eqdep_dec.
+Require Import Psatz.
 
 Local Open Scope int63_scope.
 Local Open Scope Z_scope.
@@ -54,15 +56,15 @@ Qed.
 
 Lemma eqb_false_complete : forall x y, x <> y -> (x == y) = false.
 Proof.
- intros x y;rewrite eqb_false_spec;trivial. 
+ intros x y;rewrite eqb_false_spec;trivial.
 Qed.
 
 Lemma eqb_false_correct : forall x y, (x == y) = false -> x <> y.
 Proof.
  intros x y;rewrite eqb_false_spec;trivial.
-Qed.  
- 
-Definition eqs (i j : int) : {i = j} + { i <> j } := 
+Qed.
+
+Definition eqs (i j : int) : {i = j} + { i <> j } :=
   (if i == j as b return ((b = true -> i = j) -> (b = false -> i <> j) -> {i=j} + {i <> j} )
     then fun (Heq : true = true -> i = j) _ => left _ (Heq (eq_refl true))
     else fun _ (Hdiff : false = false -> i <> j) => right _ (Hdiff (eq_refl false)))
@@ -99,7 +101,7 @@ Qed.
 Lemma eqo_diff : forall i j, i == j = false -> eqo i j = None.
 Proof.
  unfold eqo;intros; generalize (eqb_correct i j).
- rewrite H;trivial. 
+ rewrite H;trivial.
 Qed.
 
 (** translation with Z *)
@@ -116,21 +118,21 @@ Proof.
 Qed.
 
 Lemma to_Z_bounded : forall x, 0 <= [|x|] < wB.
-Proof.
- unfold to_Z, wB;induction size;intros.
- simpl;auto with zarith.
- rewrite inj_S;simpl;assert (W:= IHn (x >> 1)%int63).
- rewrite Zpower_Zsucc;auto with zarith.
- destruct (is_even x).
- rewrite Zdouble_mult;auto with zarith.
- rewrite Zdouble_plus_one_mult;auto with zarith.
-Qed.
+Proof. apply phi_bounded. Qed.
+(*  unfold to_Z, wB;induction size;intros. *)
+(*  simpl;auto with zarith. *)
+(*  rewrite inj_S;simpl;assert (W:= IHn (x >> 1)%int). *)
+(*  rewrite Zpower_Zsucc;auto with zarith. *)
+(*  destruct (is_even x). *)
+(*  rewrite Zdouble_mult;auto with zarith. *)
+(*  rewrite Zdouble_plus_one_mult;auto with zarith. *)
+(* Qed. *)
 
 (* TODO: move_this *)
-Lemma orb_true_iff : forall b1 b2, b1 || b2 = true <-> b1 = true \/ b2 = true.
-Proof.
- split;intros;[apply orb_prop | apply orb_true_intro];trivial.
-Qed.
+(* Lemma orb_true_iff : forall b1 b2, b1 || b2 = true <-> b1 = true \/ b2 = true. *)
+(* Proof. *)
+(*  split;intros;[apply orb_prop | apply orb_true_intro];trivial. *)
+(* Qed. *)
 
 Lemma to_Z_eq : forall x y, [|x|] = [|y|] <-> x = y.
 Proof.
@@ -138,7 +140,7 @@ Proof.
  apply to_Z_inj;trivial.
 Qed.
 
-Lemma leb_ltb_eqb : forall x y, ((x <= y) = (x < y) || (x == y))%int63.
+Lemma leb_ltb_eqb : forall x y, ((x <= y) = (x < y) || (x == y))%int.
 Proof.
  intros.
  apply eq_true_iff_eq.
@@ -152,17 +154,17 @@ Lemma compare_spec :
   forall x y, compare x y = ([|x|] ?= [|y|]).
 Proof.
  intros;rewrite compare_def_spec;unfold compare_def.
- case_eq (x < y)%int63;intros Heq.
+ case_eq (x < y)%int;intros Heq.
  rewrite ltb_spec in Heq.
  red in Heq;rewrite Heq;trivial.
  rewrite <- not_true_iff_false, ltb_spec in Heq.
- case_eq (x == y)%int63;intros Heq1.
+ case_eq (x == y)%int;intros Heq1.
  rewrite eqb_spec in Heq1;rewrite Heq1, Zcompare_refl;trivial.
  rewrite <- not_true_iff_false, eqb_spec in Heq1.
  symmetry;change ([|x|] > [|y|]);rewrite <- to_Z_eq in Heq1;omega.
 Qed.
 
-Lemma is_zero_spec : forall x : int, is_zero x = true <-> x = 0%int63.
+Lemma is_zero_spec : forall x : int, is_zero x = true <-> x = 0%int.
 Proof.
  unfold is_zero;intros;apply eqb_spec.
 Qed.
@@ -174,7 +176,7 @@ Lemma addc_spec  : forall x y, [+|x +c y|] = [|x|] + [|y|].
 Proof.
  intros;rewrite addc_def_spec;unfold addc_def.
  assert (W1 := to_Z_bounded x); assert (W2 := to_Z_bounded y).
- case_eq ((x + y < x)%int63).
+ case_eq ((x + y < x)%int).
  rewrite ltb_spec;intros.
  change (wB + [|x+y|] = [|x|] + [|y|]).
  rewrite add_spec in H |- *.
@@ -195,8 +197,9 @@ Proof.
  rewrite Zmod_small;auto with zarith.
 Qed.
 
+
 Lemma succc_spec : forall x, [+|succc x|] = [|x|] + 1.
-Proof. intros; apply addc_spec. Qed.
+Proof. intros; unfold succc; apply addc_spec. Qed.
 
 Lemma addcarry_spec : forall x y, [|addcarry x y|] = ([|x|] + [|y|] + 1) mod wB.
 Proof.
@@ -208,7 +211,7 @@ Lemma addcarryc_spec : forall x y, [+|addcarryc x y|] = [|x|] + [|y|] + 1.
 Proof.
  intros;rewrite addcarryc_def_spec;unfold addcarryc_def.
  assert (W1 := to_Z_bounded x); assert (W2 := to_Z_bounded y).
- case_eq ((addcarry x y <= x)%int63).
+ case_eq ((addcarry x y <= x)%int).
  rewrite leb_spec;intros.
  change (wB + [|(addcarry x y)|] = [|x|] + [|y|] + 1).
  rewrite addcarry_spec in H |- *.
@@ -237,7 +240,7 @@ Lemma subc_spec : forall x y, [-|x -c y|] = [|x|] - [|y|].
 Proof.
  intros;rewrite subc_def_spec;unfold subc_def.
  assert (W1 := to_Z_bounded x); assert (W2 := to_Z_bounded y).
- case_eq (y <= x)%int63.
+ case_eq (y <= x)%int.
  rewrite leb_spec;intros.
  change ([|x - y|] = [|x|] - [|y|]).
  rewrite sub_spec.
@@ -252,7 +255,7 @@ Qed.
 
 Lemma subcarry_spec :
    forall x y, [|subcarry x y|] = ([|x|] - [|y|] - 1) mod wB.
-Proof. 
+Proof.
  unfold subcarry; intros.
  rewrite sub_spec,sub_spec,Zminus_mod_idemp_l;trivial.
 Qed.
@@ -260,8 +263,9 @@ Qed.
 Lemma subcarryc_spec : forall x y, [-|subcarryc x y|] = [|x|] - [|y|] - 1.
  intros;rewrite subcarryc_def_spec;unfold subcarryc_def.
  assert (W1 := to_Z_bounded x); assert (W2 := to_Z_bounded y).
- fold (subcarry x y).
- case_eq (y < x)%int63.
+ (* fold (subcarry x y). *)
+ replace ((x - y - 1)%int) with (subcarry x y) by reflexivity.
+ case_eq (y < x)%int.
  rewrite ltb_spec;intros.
  change ([|subcarry x y|] = [|x|] - [|y|] - 1).
  rewrite subcarry_spec.
@@ -295,13 +299,13 @@ Proof.
 Qed.
 
 Lemma predc_spec : forall x, [-|predc x|] = [|x|] - 1.
-Proof. intros; apply subc_spec. Qed.
+Proof. intros; unfold predc; apply subc_spec. Qed.
 
 Lemma pred_spec : forall x, [|pred x|] = ([|x|] - 1) mod wB.
-Proof. intros; apply sub_spec. Qed.
+Proof. intros; unfold pred; apply sub_spec. Qed.
 
-Lemma diveucl_spec : 
-  forall x y, 
+Lemma diveucl_spec :
+  forall x y,
     let (q,r) := diveucl x y in
     ([|q|],[|r|]) = Zdiv_eucl [|x|] [|y|].
 Proof.
@@ -387,6 +391,7 @@ Proof.
  apply Z_mult_div_ge; auto with zarith.
 Qed.
 
+
 Lemma sqrt_step_correct rec i j:
   0 < [|i|] -> 0 < [|j|] -> [|i|] < ([|j|] + 1) ^ 2 ->
    2 * [|j|] < wB ->
@@ -398,7 +403,7 @@ Proof.
  assert (Hp2: 0 < [|2|]) by exact (refl_equal Lt).
  intros Hi Hj Hij H31 Hrec.
  unfold sqrt_step.
- case_eq ((i / j < j)%int63);[ | rewrite <- Bool.not_true_iff_false];
+ case_eq ((i / j < j)%int);[ | rewrite <- Bool.not_true_iff_false];
   rewrite ltb_spec, div_spec;intros.
  assert ([| j + i / j|] = [|j|] + [|i|]/[|j|]).
    rewrite add_spec, Zmod_small;rewrite div_spec;auto with zarith.
@@ -415,7 +420,7 @@ Proof.
  apply sqrt_main;auto with zarith.
  split;[apply sqrt_test_true | ];auto with zarith.
 Qed.
- 
+
 Lemma iter_sqrt_correct n rec i j: 0 < [|i|] -> 0 < [|j|] ->
   [|i|] < ([|j|] + 1) ^ 2 -> 2 * [|j|] < wB ->
   (forall j1, 0 < [|j1|] -> 2^(Z_of_nat n) + [|j1|] <= [|j|] ->
@@ -424,10 +429,11 @@ Lemma iter_sqrt_correct n rec i j: 0 < [|i|] -> 0 < [|j|] ->
   [|iter_sqrt n rec i j|] ^ 2 <= [|i|] < ([|iter_sqrt n rec i j|] + 1) ^ 2.
 Proof.
  revert rec i j; elim n; unfold iter_sqrt; fold iter_sqrt; clear n.
- intros rec i j Hi Hj Hij H31 Hrec; apply sqrt_step_correct; auto with zarith.
+ intros rec i j Hi Hj Hij H31 Hrec. replace (and (Z.le (Z.pow (to_Z match ltb (div i j) j return int with | true => rec i (lsr (add63 j (div i j)) In) | false => j end) (Zpos (xO xH))) (to_Z i)) (Z.lt (to_Z i) (Z.pow (Z.add (to_Z match ltb (div i j) j return int with | true => rec i (lsr (add63 j (div i j)) In) | false => j end) (Zpos xH)) (Zpos (xO xH))))) with ([|sqrt_step rec i j|] ^ 2 <= [|i|] < ([|sqrt_step rec i j|] + 1) ^ 2) by reflexivity. apply sqrt_step_correct; auto with zarith.
  intros; apply Hrec; auto with zarith.
  rewrite Zpower_0_r; auto with zarith.
  intros n Hrec rec i j Hi Hj Hij H31 HHrec.
+ replace (and (Z.le (Z.pow (to_Z match ltb (div i j) j return int with | true => iter_sqrt n (iter_sqrt n rec) i (lsr (add63 j (div i j)) In) | false => j end) (Zpos (xO xH))) (to_Z i)) (Z.lt (to_Z i) (Z.pow (Z.add (to_Z match ltb (div i j) j return int with | true => iter_sqrt n (iter_sqrt n rec) i (lsr (add63 j (div i j)) In) | false => j end) (Zpos xH)) (Zpos (xO xH))))) with ([|sqrt_step (iter_sqrt n (iter_sqrt n rec)) i j|] ^ 2 <= [|i|] < ([|sqrt_step (iter_sqrt n (iter_sqrt n rec)) i j|] + 1) ^ 2) by reflexivity.
  apply sqrt_step_correct; auto.
  intros j1 Hj1  Hjp1; apply Hrec; auto with zarith.
  intros j2 Hj2 H2j2 Hjp2 Hj31; apply Hrec; auto with zarith.
@@ -463,13 +469,13 @@ Qed.
 
 Lemma sqrt2_step_def rec ih il j:
    sqrt2_step rec ih il j =
-   if (ih < j)%int63 then
+   if (ih < j)%int then
     let quo := fst (diveucl_21 ih il j) in
-    if (quo < j)%int63 then
+    if (quo < j)%int then
      let m :=
       match j +c quo with
       | C0 m1 => m1 >> 1
-      | C1 m1 => (m1 >> 1 + 1 << (digits -1))%int63
+      | C1 m1 => (m1 >> 1 + 1 << (digits -1))%int
       end in
      rec ih il m
     else j
@@ -493,7 +499,8 @@ Proof.
  apply Zle_trans with ([|ih|] * wB)%Z;try rewrite Zpower_2; auto with zarith.
 Qed.
 
-Lemma div2_phi ih il j: 
+
+Lemma div2_phi ih il j:
   [|fst (diveucl_21 ih il j)|] = [|| WW ih il||] /[|j|].
 Proof.
  generalize (diveucl_21_spec ih il j).
@@ -508,7 +515,7 @@ Qed.
 
 
 Lemma sqrt2_step_correct rec ih il j:
-  2 ^ (Z_of_nat (size - 2)) <= [|ih|] -> 
+  2 ^ (Z_of_nat (size - 2)) <= [|ih|] ->
   0 < [|j|] -> [|| WW ih il||] < ([|j|] + 1) ^ 2 ->
   (forall j1, 0 < [|j1|] < [|j|] ->  [|| WW ih il||] < ([|j1|] + 1) ^ 2 ->
      [|rec ih il j1|] ^ 2 <= [||WW ih il||] < ([|rec ih il j1|] + 1) ^ 2) ->
@@ -526,7 +533,7 @@ Proof.
   apply Zmult_lt_0_compat; auto with zarith.
   apply Zlt_le_trans with (2:= Hih); auto with zarith.
  cbv zeta.
- case_eq (ih < j)%int63;intros Heq.
+ case_eq (ih < j)%int;intros Heq.
  rewrite ltb_spec in Heq.
  2: rewrite <-not_true_iff_false, ltb_spec in Heq.
  2: split; auto.
@@ -535,13 +542,13 @@ Proof.
  2: assert (0 <= [|il|]/[|j|]) by (apply Z_div_pos; auto with zarith).
  2: rewrite Zmult_comm, Z_div_plus_full_l; unfold base; auto with zarith.
  case (Zle_or_lt (2^(Z_of_nat size -1)) [|j|]); intros Hjj.
- case_eq (fst (diveucl_21 ih il j) < j)%int63;intros Heq0.
+ case_eq (fst (diveucl_21 ih il j) < j)%int;intros Heq0.
  2: rewrite <-not_true_iff_false, ltb_spec, div2_phi in Heq0.
  2: split; auto; apply sqrt_test_true; auto with zarith.
  rewrite ltb_spec, div2_phi in Heq0.
  match goal with |- context[rec _ _ ?X] =>
   set (u := X)
- end. 
+ end.
  assert (H: [|u|] = ([|j|] + ([||WW ih il||])/([|j|]))/2).
   unfold u; generalize (addc_spec j (fst (diveucl_21 ih il j)));
   case addc;unfold interp_carry;rewrite div2_phi;simpl zn2z_to_Z.
@@ -561,7 +568,7 @@ Proof.
  apply Hrec; rewrite H; clear u H.
  assert (Hf1: 0 <= [||WW ih il||]/ [|j|]) by (apply Z_div_pos; auto with zarith).
  case (Zle_lt_or_eq 1 ([|j|])); auto with zarith; intros Hf2.
- 2: contradict Heq0; apply Zle_not_lt; rewrite <- Hf2, Zdiv_1_r; auto with zarith.
+ 2: contradict Heq0; apply Zle_not_lt; rewrite <- Hf2, Zdiv_1_r; assert (H10: forall (x:Z), 0 < x -> 1 <= x) by (intros; omega); auto.
  split.
  replace ([|j|] + [||WW ih il||]/ [|j|])%Z with
         (1 * 2 + (([|j|] - 2) + [||WW ih il||] / [|j|])); try ring.
@@ -580,6 +587,7 @@ Proof.
 Qed.
 
 
+
 Lemma iter2_sqrt_correct n rec ih il j:
   2^(Z_of_nat (size - 2)) <= [|ih|] ->  0 < [|j|] -> [||WW ih il||] < ([|j|] + 1) ^ 2 ->
   (forall j1, 0 < [|j1|] -> 2^(Z_of_nat n) + [|j1|] <= [|j|] ->
@@ -603,6 +611,7 @@ Proof.
  apply Zle_0_nat.
 Qed.
 
+
 Lemma sqrt2_spec : forall x y,
        wB/ 4 <= [|x|] ->
        let (s,r) := sqrt2 x y in
@@ -632,7 +641,7 @@ Lemma sqrt2_spec : forall x y,
  generalize (subc_spec il il1).
  case subc; intros il2 Hil2.
  simpl interp_carry in Hil2.
- case_eq (ih1  < ih)%int63;  [idtac | rewrite <- not_true_iff_false];
+ case_eq (ih1  < ih)%int;  [idtac | rewrite <- not_true_iff_false];
   rewrite ltb_spec; intros Heq.
  unfold interp_carry; rewrite Zmult_1_l.
  rewrite Zpower_2, Hihl1, Hil2.
@@ -653,7 +662,7 @@ Lemma sqrt2_spec : forall x y,
  intros H2; split.
  unfold zn2z_to_Z; rewrite <- H2; ring.
  replace (wB + ([|il|] - [|il1|])) with ([||WW ih il||] - ([|s|] * [|s|])).
- rewrite <-Hbin in Hs2; auto with zarith.
+ rewrite <-Hbin in Hs2; assert (([||WW ih il||] < [|s|] * [|s|] + 2 * [|s|] + 1) -> ([||WW ih il||] - [|s|] * [|s|] <= 2 * [|s|])) by omega; auto.
  rewrite Hihl1; unfold zn2z_to_Z; rewrite <- H2; ring.
  unfold interp_carry.
  case (Zle_lt_or_eq [|ih|] [|ih1|]); auto with zarith; intros H.
@@ -670,7 +679,7 @@ Lemma sqrt2_spec : forall x y,
  unfold zn2z_to_Z; ring[Hil2 H].
  replace [|il2|] with ([||WW ih il||] - [||WW ih1 il1||]).
  unfold zn2z_to_Z at 2; rewrite <-Hihl1.
- rewrite <-Hbin in Hs2; auto with zarith.
+ rewrite <-Hbin in Hs2; assert (([||WW ih il||] < [|s|] * [|s|] + 2 * [|s|] + 1) -> ([||WW ih il||] - [|s|] * [|s|] <= 2 * [|s|])) by omega; auto.
  unfold zn2z_to_Z; rewrite H, Hil2; ring.
  unfold interp_carry in Hil2 |- *.
  assert (Hsih: [|ih - 1|] = [|ih|] - 1).
@@ -678,7 +687,7 @@ Lemma sqrt2_spec : forall x y,
   case (to_Z_bounded ih); intros H1 H2.
   split; auto with zarith.
   apply Zle_trans with (wB/4 - 1); auto with zarith.
- case_eq (ih1 < ih - 1)%int63;  [idtac | rewrite <- not_true_iff_false];
+ case_eq (ih1 < ih - 1)%int;  [idtac | rewrite <- not_true_iff_false];
   rewrite ltb_spec, Hsih; intros Heq.
  rewrite Zpower_2, Hihl1.
  case (Zle_lt_or_eq ([|ih1|] + 2) [|ih|]); auto with zarith.
@@ -702,7 +711,7 @@ Lemma sqrt2_spec : forall x y,
  rewrite <-Hil2; ring.
  replace (1 * wB + [|il2|]) with ([||WW ih il||] - [||WW ih1 il1||]).
  unfold zn2z_to_Z at 2; rewrite <-Hihl1.
- rewrite <-Hbin in Hs2; auto with zarith.
+ rewrite <-Hbin in Hs2; assert (([||WW ih il||] < [|s|] * [|s|] + 2 * [|s|] + 1) -> ([||WW ih il||] - [|s|] * [|s|] <= 2 * [|s|])) by omega; auto.
  unfold zn2z_to_Z; rewrite <-H2.
  replace [|il|] with (([|il|] - [|il1|]) + [|il1|]); try ring.
  rewrite <-Hil2; ring.
@@ -730,7 +739,7 @@ Lemma sqrt2_spec : forall x y,
  rewrite <-Hil2; ring.
  replace [|il2|] with ([||WW ih il||] - [||WW ih1 il1||]).
  unfold zn2z_to_Z at 2; rewrite <- Hihl1.
- rewrite <-Hbin in Hs2; auto with zarith.
+ rewrite <-Hbin in Hs2; assert (([||WW ih il||] < [|s|] * [|s|] + 2 * [|s|] + 1) -> ([||WW ih il||] - [|s|] * [|s|] <= 2 * [|s|])) by omega; auto.
  unfold zn2z_to_Z.
  rewrite <-H1.
  ring_simplify.
@@ -747,7 +756,7 @@ Proof.
  reflexivity.
  simpl.
  generalize (to_Z_bounded j)(to_Z_bounded i); intros.
- case_eq (j == 0)%int63.
+ case_eq (j == 0)%int.
  rewrite eqb_spec;intros H1;rewrite H1.
  replace [|0|] with 0;trivial;rewrite Z.abs_eq;auto with zarith.
  rewrite <- not_true_iff_false, eqb_spec;intros.
@@ -766,14 +775,14 @@ Proof.
  unfold Zgcd_bound.
  generalize (to_Z_bounded b).
  destruct [|b|].
- unfold size; auto with zarith.
+ unfold size; intros _; change Int63Lib.size with 63%nat; omega.
  intros (_,H).
  cut (Psize p <= size)%nat; [ omega | rewrite <- Zpower2_Psize; auto].
  intros (H,_); compute in H; elim H; auto.
 Qed.
 
 Lemma head00_spec:  forall x, [|x|] = 0 -> [|head0 x|] = [|digits|].
-Proof. 
+Proof.
  change 0 with [|0|];intros x Heq.
  apply to_Z_inj in Heq;rewrite Heq;trivial.
 Qed.
@@ -785,7 +794,7 @@ Proof.
 Qed.
 
 (* lsr lsl *)
-Lemma lsl_0_l i: 0 << i = 0%int63.
+Lemma lsl_0_l i: 0 << i = 0%int.
 Proof.
  apply to_Z_inj.
  generalize (lsl_spec 0 i).
@@ -799,7 +808,7 @@ Proof.
  apply Zmod_small; apply (to_Z_bounded i).
 Qed.
 
-Lemma lsl_M_r x i (H: (digits <= i = true)%int63) : x << i = 0%int63.
+Lemma lsl_M_r x i (H: (digits <= i = true)%int) : x << i = 0%int.
 Proof.
  apply to_Z_inj.
  rewrite lsl_spec, to_Z_0.
@@ -811,7 +820,7 @@ Proof.
  case (to_Z_bounded digits); auto with zarith.
 Qed.
 
-Lemma lsr_0_l i: 0 >> i = 0%int63.
+Lemma lsr_0_l i: 0 >> i = 0%int.
 Proof.
  apply to_Z_inj.
  generalize (lsr_spec 0 i).
@@ -824,7 +833,7 @@ Proof.
  rewrite lsr_spec, to_Z_0, Zdiv_1_r; auto.
 Qed.
 
-Lemma lsr_M_r x i (H: (digits <= i = true)%int63) : x >> i = 0%int63.
+Lemma lsr_M_r x i (H: (digits <= i = true)%int) : x >> i = 0%int.
 Proof.
  apply to_Z_inj.
  rewrite lsr_spec, to_Z_0.
@@ -837,8 +846,8 @@ Proof.
  apply Zpower_le_monotone; auto with zarith.
 Qed.
 
-Lemma add_le_r m n: 
-  if  (n <= m + n)%int63 then  ([|m|] + [|n|] < wB)%Z else  (wB <= [|m|] + [|n|])%Z.
+Lemma add_le_r m n:
+  if  (n <= m + n)%int then  ([|m|] + [|n|] < wB)%Z else  (wB <= [|m|] + [|n|])%Z.
 Proof.
  case (to_Z_bounded m); intros H1m H2m.
  case (to_Z_bounded n); intros H1n H2n.
@@ -849,20 +858,20 @@ Proof.
      rewrite Zplus_mod, Z_mod_same_full, Zplus_0_r, !Zmod_small; auto with zarith.
      rewrite !Zmod_small; auto with zarith.
      apply f_equal2 with (f := Zmod); auto with zarith.
-   case_eq (n <= m + n)%int63; auto.
+   case_eq (n <= m + n)%int; auto.
    rewrite leb_spec, H1; auto with zarith.
  assert (H1: ([| m + n |] = [|m|] + [|n|])%Z).
    rewrite add_spec, Zmod_small; auto with zarith.
- replace (n <= m + n)%int63 with true; auto.
+ replace (n <= m + n)%int with true; auto.
  apply sym_equal; rewrite leb_spec, H1; auto with zarith.
 Qed.
 
-Lemma lsr_add i m n: ((i >> m) >> n = if n <= m + n then i >> (m + n) else 0)%int63.
+Lemma lsr_add i m n: ((i >> m) >> n = if n <= m + n then i >> (m + n) else 0)%int.
 Proof.
  case (to_Z_bounded m); intros H1m H2m.
  case (to_Z_bounded n); intros H1n H2n.
  case (to_Z_bounded i); intros H1i H2i.
- generalize (add_le_r m n); case (n <= m + n)%int63; intros H.
+ generalize (add_le_r m n); case (n <= m + n)%int; intros H.
    apply to_Z_inj; rewrite !lsr_spec, Zdiv_Zdiv, <- Zpower_exp; auto with zarith.
    rewrite add_spec, Zmod_small; auto with zarith.
  apply to_Z_inj; rewrite !lsr_spec, Zdiv_Zdiv, <- Zpower_exp; auto with zarith.
@@ -872,12 +881,12 @@ Proof.
  apply Zpower2_le_lin; auto with zarith.
 Qed.
 
-Lemma lsl_add i m n: ((i << m) << n = if n <= m + n then i << (m + n) else 0)%int63.
+Lemma lsl_add i m n: ((i << m) << n = if n <= m + n then i << (m + n) else 0)%int.
 Proof.
  case (to_Z_bounded m); intros H1m H2m.
  case (to_Z_bounded n); intros H1n H2n.
  case (to_Z_bounded i); intros H1i H2i.
- generalize (add_le_r m n); case (n <= m + n)%int63; intros H.
+ generalize (add_le_r m n); case (n <= m + n)%int; intros H.
    apply to_Z_inj; rewrite !lsl_spec, Zmult_mod, Zmod_mod, <- Zmult_mod.
    rewrite <-Zmult_assoc, <- Zpower_exp; auto with zarith.
    apply f_equal2 with (f := Zmod); auto.
@@ -885,7 +894,7 @@ Proof.
  apply to_Z_inj; rewrite !lsl_spec, Zmult_mod, Zmod_mod, <- Zmult_mod.
  rewrite <-Zmult_assoc, <- Zpower_exp; auto with zarith.
  unfold wB.
- replace ([|m|] + [|n|])%Z with 
+ replace ([|m|] + [|n|])%Z with
          ((([|m|] + [|n|]) - Z_of_nat size) + Z_of_nat size)%Z.
  2: ring.
  rewrite Zpower_exp, Zmult_assoc, Z_mod_mult; auto with zarith.
@@ -893,7 +902,8 @@ Proof.
  apply Zpower2_lt_lin; auto with zarith.
 Qed.
 
-Coercion b2i (b: bool) : int := if b then 1%int63 else 0%int63.
+
+Coercion b2i (b: bool) : int63 := if b then 1%int else 0%int.
 
 Lemma bit_0 n : bit 0 n = false.
 Proof. unfold bit; rewrite lsr_0_l; auto. Qed.
@@ -904,7 +914,7 @@ Proof.
  rewrite eqb_spec; intros H; rewrite H, lsr_0_r.
  apply refl_equal.
  intros Hn.
- assert (H1n : (1 >> n = 0)%int63); auto.
+ assert (H1n : (1 >> n = 0)%int); auto.
  apply to_Z_inj; rewrite lsr_spec.
  apply Zdiv_small; rewrite to_Z_1; split; auto with zarith.
  change 1%Z with (2^0)%Z.
@@ -925,20 +935,20 @@ Proof.
  rewrite lsl_0_l; apply refl_equal.
 Qed.
 
-Lemma bit_M i n (H: (digits <= n = true)%int63): bit i n = false.
+Lemma bit_M i n (H: (digits <= n = true)%int): bit i n = false.
 Proof. unfold bit; rewrite lsr_M_r; auto. Qed.
 
-Lemma bit_half i n (H: (n < digits = true)%int63) : bit (i>>1) n = bit i (n+1).
+Lemma bit_half i n (H: (n < digits = true)%int) : bit (i>>1) n = bit i (n+1).
 Proof.
  unfold bit.
  rewrite lsr_add.
- case_eq (n <= (1 + n))%int63.
- replace (1+n)%int63 with (n+1)%int63; [auto|idtac].
+ case_eq (n <= (1 + n))%int.
+ replace (1+n)%int with (n+1)%int; [auto|idtac].
  apply to_Z_inj; rewrite !add_spec, Zplus_comm; auto.
  intros H1; assert (H2: n = max_int).
  2: generalize H; rewrite H2; discriminate.
  case (to_Z_bounded n); intros H1n H2n.
- case (Zle_lt_or_eq [|n|] (wB - 1)); auto with zarith; 
+ case (Zle_lt_or_eq [|n|] (wB - 1)); auto with zarith;
    intros H2; apply to_Z_inj; auto.
  generalize (add_le_r 1 n); rewrite H1.
  change [|max_int|] with (wB - 1)%Z.
@@ -980,7 +990,7 @@ Proof.
  rewrite to_Z_eq; auto.
 Qed.
 
-Lemma bit_split i : (i = (i>>1)<<1 + bit i 0)%int63.
+Lemma bit_split i : (i = (i>>1)<<1 + bit i 0)%int.
 Proof.
  apply to_Z_inj.
  rewrite add_spec, lsl_spec, lsr_spec, bit_0_spec, Zplus_mod_idemp_l.
@@ -989,6 +999,7 @@ Proof.
  rewrite Zmod_small; auto; case (to_Z_bounded i); auto.
 Qed.
 
+
 Lemma bit_eq i1 i2:
   i1 = i2 <-> forall i, bit i1 i = bit i2 i.
 Proof.
@@ -1000,7 +1011,7 @@ Proof.
  intros n IH i1 i2 H1i1 H2i1 H1i2 H2i2 H.
  rewrite (bit_split i1), (bit_split i2).
  rewrite H.
- apply f_equal2 with (f := add); auto.
+ apply f_equal2 with (f := add63); auto.
  apply f_equal2 with (f := lsl); auto.
  apply IH; try rewrite lsr_spec;
    replace (2^[|1|]) with 2%Z;  auto with zarith.
@@ -1017,23 +1028,23 @@ Proof.
 Qed.
 
 Lemma bit_lsr x i j :
- (bit (x >> i) j = if j <= i + j then bit x (i + j) else false)%int63.
+ (bit (x >> i) j = if j <= i + j then bit x (i + j) else false)%int.
 Proof.
  unfold bit; rewrite lsr_add; case leb; auto.
 Qed.
 
-Lemma bit_lsl x i j : bit (x << i) j = 
-(if (j < i) || (digits <= j) then false else bit x (j - i))%int63.
+Lemma bit_lsl x i j : bit (x << i) j =
+(if (j < i) || (digits <= j) then false else bit x (j - i))%int.
 Proof.
  assert (F1: 1 >= 0) by discriminate.
- case_eq (digits <= j)%int63; intros H.
+ case_eq (digits <= j)%int; intros H.
  rewrite orb_true_r, bit_M; auto.
  set (d := [|digits|]).
  case (Zle_or_lt d [|j|]); intros H1.
  case (leb_spec digits j); rewrite H; auto with zarith.
  intros _ HH; generalize (HH H1); discriminate.
  clear H.
- generalize (ltb_spec j i); case ltb; intros H2; unfold bit; simpl.
+ generalize (ltb_spec j i); case ltb; intros H2; unfold bit; [change (if true || false then false else negb (is_zero ((x >> (j - i)) << (digits - 1)))) with false | change (if false || false then false else negb (is_zero ((x >> (j - i)) << (digits - 1)))) with (negb (is_zero ((x >> (j - i)) << (digits - 1))))].
  assert (F2: ([|j|] < [|i|])%Z) by (case H2; auto); clear H2.
  replace (is_zero (((x << i) >> j) << (digits - 1))) with true; auto.
  case (to_Z_bounded j); intros  H1j H2j.
@@ -1068,22 +1079,22 @@ Proof.
  replace d with ((d - [|i|]) + [|i|])%Z.
  2: ring.
  case (to_Z_bounded i); intros  H1i H2i.
- rewrite Zpower_exp; auto with zarith.
+ rewrite Zpower_exp; [ |apply Z.le_ge; lia|apply Z.le_ge; assumption].
  rewrite Zmult_mod_distr_r.
  case (to_Z_bounded j); intros  H1j H2j.
  replace [|j - i|] with ([|j|] - [|i|])%Z.
  2: rewrite sub_spec, Zmod_small; auto with zarith.
  set (d1 := (d - [|i|])%Z).
  set (d2 := ([|j|] - [|i|])%Z).
- pattern [|j|] at 1; 
+ pattern [|j|] at 1;
    replace [|j|] with (d2 + [|i|])%Z.
  2: unfold d2; ring.
  rewrite Zpower_exp; auto with zarith.
  rewrite Zdiv_mult_cancel_r; auto with zarith.
  2: unfold d2; auto with zarith.
  rewrite (Z_div_mod_eq [|x|] (2^d1)) at 2; auto with zarith.
- 2: apply Zlt_gt; apply Zpower_gt_0; unfold d1; auto with zarith.
- pattern d1 at 2; 
+ 2: apply Zlt_gt; apply Zpower_gt_0; unfold d1; lia.
+ pattern d1 at 2;
    replace d1 with (d2 + (1+ (d - [|j|] - 1)))%Z.
  2: unfold d1, d2; ring.
  rewrite Zpower_exp; auto with zarith.
@@ -1096,6 +1107,7 @@ Proof.
  rewrite <-!Zmult_assoc, Zmult_comm, Z_mod_mult, Zplus_0_l; auto.
 Qed.
 
+
 Lemma bit_b2i (b: bool) i : bit b i = (i == 0) && b.
 Proof.
  case b; unfold bit; simpl b2i.
@@ -1103,7 +1115,7 @@ Proof.
  rewrite lsr_1; case (i == 0); auto.
 Qed.
 
-Lemma bit_or_split i : (i = (i>>1)<<1 lor bit i 0)%int63.
+Lemma bit_or_split i : (i = (i>>1)<<1 lor bit i 0)%int.
 Proof.
  rewrite bit_eq.
  intros n; rewrite lor_spec.
@@ -1112,12 +1124,12 @@ Proof.
  case (Zle_lt_or_eq _ _ Hi).
  2: replace 0%Z with [|0|]; auto; rewrite to_Z_eq.
  2: intros H; rewrite <-H.
- 2: replace (0 < 1)%int63 with true; auto.
+ 2: replace (0 < 1)%int with true; auto.
  intros H; clear Hi.
  case_eq (n == 0).
  rewrite eqb_spec; intros H1; generalize H; rewrite H1; discriminate.
  intros _; rewrite orb_false_r.
- case_eq (n < 1)%int63.
+ case_eq (n < 1)%int.
  rewrite ltb_spec, to_Z_1; intros HH; contradict HH; auto with zarith.
  intros _.
  generalize (@bit_M i n); case leb.
@@ -1127,7 +1139,7 @@ Proof.
  assert (F1: [|n - 1|] = ([|n|] - 1)%Z).
  rewrite sub_spec, Zmod_small; rewrite to_Z_1; auto with zarith.
  generalize (add_le_r 1 (n - 1)); case leb; rewrite F1, to_Z_1; intros HH.
- replace (1 + (n -1))%int63 with n; auto.
+ replace (1 + (n -1))%int with n; auto.
  apply to_Z_inj; rewrite add_spec, F1, Zmod_small; rewrite to_Z_1;
   auto with zarith.
  rewrite bit_M; auto; rewrite leb_spec.
@@ -1169,13 +1181,13 @@ Qed.
 
 (* More land *)
 
-Lemma land_0_l i: 0 land i = 0%int63.
+Lemma land_0_l i: 0 land i = 0%int.
 Proof.
  apply bit_eq; intros n.
  rewrite land_spec, bit_0; auto.
 Qed.
 
-Lemma land_0_r i: i land 0 = 0%int63.
+Lemma land_0_r i: i land 0 = 0%int.
 Proof.
  apply bit_eq; intros n.
  rewrite land_spec, bit_0, andb_false_r; auto.
@@ -1188,6 +1200,7 @@ Proof.
  rewrite !land_spec, andb_assoc; auto.
 Qed.
 
+
 Lemma land_comm i j : i land j = j land i.
 Proof.
  apply bit_eq; intros n.
@@ -1272,21 +1285,21 @@ Lemma land_lsr i1 i2 i: (i1 land i2) >> i = (i1 >> i) land (i2 >> i).
 Proof.
  apply bit_eq; intros n.
  rewrite land_spec, !bit_lsr, land_spec.
- case (_ <= _)%int63; auto.
+ case (_ <= _)%int; auto.
 Qed.
 
 Lemma lor_lsr i1 i2 i: (i1 lor i2) >> i = (i1 >> i) lor (i2 >> i).
 Proof.
  apply bit_eq; intros n.
  rewrite lor_spec, !bit_lsr, lor_spec.
- case (_ <= _)%int63; auto.
+ case (_ <= _)%int; auto.
 Qed.
 
 Lemma lxor_lsr i1 i2 i: (i1 lxor i2) >> i = (i1 >> i) lxor (i2 >> i).
 Proof.
  apply bit_eq; intros n.
  rewrite lxor_spec, !bit_lsr, lxor_spec.
- case (_ <= _)%int63; auto.
+ case (_ <= _)%int; auto.
 Qed.
 
 Lemma is_even_and i j : is_even (i land j) = is_even i || is_even j.
@@ -1304,25 +1317,25 @@ Proof.
  rewrite !is_even_bit, lxor_spec; do 2 case bit; auto.
 Qed.
 
-Lemma lsl_add_distr x y n: (x + y) << n = ((x << n) + (y << n))%int63.
+Lemma lsl_add_distr x y n: (x + y) << n = ((x << n) + (y << n))%int.
 Proof.
  apply to_Z_inj; rewrite !lsl_spec, !add_spec, Zmult_mod_idemp_l.
  rewrite !lsl_spec, <-Zplus_mod.
  apply f_equal2 with (f := Zmod); auto with zarith.
 Qed.
 
-Lemma add_assoc x y z: (x + (y + z) = (x + y) + z)%int63.
+Lemma add_assoc x y z: (x + (y + z) = (x + y) + z)%int.
 Proof.
  apply to_Z_inj; rewrite !add_spec.
  rewrite Zplus_mod_idemp_l, Zplus_mod_idemp_r, Zplus_assoc; auto.
 Qed.
 
-Lemma add_comm x y: (x + y = y + x)%int63.
+Lemma add_comm x y: (x + y = y + x)%int.
 Proof.
  apply to_Z_inj; rewrite !add_spec, Zplus_comm; auto.
 Qed.
 
-Lemma lsr_add_distr x y n: (x + y) << n = ((x << n) + (y << n))%int63.
+Lemma lsr_add_distr x y n: (x + y) << n = ((x << n) + (y << n))%int.
 Proof.
  apply to_Z_inj.
  rewrite add_spec, !lsl_spec, add_spec.
@@ -1330,7 +1343,7 @@ Proof.
  apply f_equal2 with (f := Zmod); auto with zarith.
 Qed.
 
-Lemma is_even_add x y : 
+Lemma is_even_add x y :
   is_even (x + y) = negb (xorb (negb (is_even x)) (negb (is_even y))).
 Proof.
  assert (F : [|x + y|] mod 2 = ([|x|] mod 2 + [|y|] mod 2) mod 2).
@@ -1356,13 +1369,13 @@ Proof.
  rewrite <-is_even_bit, is_even_add, !is_even_bit.
  do 2 case bit; auto.
 Qed.
- 
-Lemma add_cancel_l x y z : (x + y = x + z)%int63 -> y = z.
+
+Lemma add_cancel_l x y z : (x + y = x + z)%int -> y = z.
 Proof.
- intros H; case (to_Z_bounded x); case (to_Z_bounded y); case (to_Z_bounded z); 
+ intros H; case (to_Z_bounded x); case (to_Z_bounded y); case (to_Z_bounded z);
   intros H1z H2z H1y H2y H1x H2x.
  generalize (add_le_r y x) (add_le_r z x); rewrite (add_comm y x), H, (add_comm z x).
- case_eq  (x <= x + z)%int63; intros H1 H2 H3.
+ case_eq  (x <= x + z)%int; intros H1 H2 H3.
  apply to_Z_inj; generalize H; rewrite <-to_Z_eq, !add_spec, !Zmod_small; auto with zarith.
  apply to_Z_inj; assert ([|x|] + [|y|] = [|x|] + [|z|]); auto with zarith.
  assert (F1: wB > 0) by apply refl_equal.
@@ -1380,7 +1393,7 @@ Proof.
  generalize (Zdiv_lt_upper_bound _ _ _ (Zgt_lt _ _ F1) F2); auto with zarith.
 Qed.
 
-Lemma add_cancel_r x y z : (y + x = z + x)%int63 -> y = z.
+Lemma add_cancel_r x y z : (y + x = z + x)%int -> y = z.
 Proof.
   rewrite !(fun t => add_comm t x); intros Hl; apply (add_cancel_l x); auto.
 Qed.
@@ -1393,7 +1406,7 @@ Proof.
     rewrite lsr_spec, to_Z_1, Zpower_1_r; split; auto with zarith.
     apply Zdiv_lt_upper_bound; auto with zarith.
   rewrite (bit_split x) at 1.
-  rewrite add_spec, Zmod_small, lsl_spec, to_Z_1, Zpower_1_r, Zmod_small; 
+  rewrite add_spec, Zmod_small, lsl_spec, to_Z_1, Zpower_1_r, Zmod_small;
     split; auto with zarith.
   change wB with ((wB/2)*2); auto with zarith.
   rewrite lsl_spec, to_Z_1, Zpower_1_r, Zmod_small; auto with zarith.
@@ -1405,13 +1418,13 @@ Proof.
   case bit; discriminate.
 Qed.
 
-Lemma lor_le x y : (y <= x lor y)%int63 = true.
+Lemma lor_le x y : (y <= x lor y)%int = true.
 Proof.
  generalize x y (to_Z_bounded x) (to_Z_bounded y); clear x y.
  unfold wB; elim size.
  replace (2^Z_of_nat 0) with 1%Z; auto with zarith.
- intros x y Hx Hy; replace x with 0%int63.
- replace y with 0%int63; auto.
+ intros x y Hx Hy; replace x with 0%int.
+ replace y with 0%int; auto.
  apply to_Z_inj; rewrite to_Z_0; auto with zarith.
  apply to_Z_inj; rewrite to_Z_0; auto with zarith.
  intros n IH x y; rewrite inj_S.
@@ -1430,14 +1443,14 @@ Proof.
 Qed.
 
 
-Lemma bit_add_or x y: 
-  (forall n, bit x n = true -> bit y n = true -> False) <-> (x + y)%int63= x lor y.
+Lemma bit_add_or x y:
+  (forall n, bit x n = true -> bit y n = true -> False) <-> (x + y)%int= x lor y.
 Proof.
  generalize x y (to_Z_bounded x) (to_Z_bounded y); clear x y.
  unfold wB; elim size.
  replace (2^Z_of_nat 0) with 1%Z; auto with zarith.
- intros x y Hx Hy; replace x with 0%int63.
- replace y with 0%int63.
+ intros x y Hx Hy; replace x with 0%int.
+ replace y with 0%int.
  split; auto; intros _ n; rewrite !bit_0; discriminate.
  apply to_Z_inj; rewrite to_Z_0; auto with zarith.
  apply to_Z_inj; rewrite to_Z_0; auto with zarith.
@@ -1446,26 +1459,26 @@ Proof.
  intros Hx Hy.
  split.
  intros Hn.
- assert (F1: ((x >> 1) + (y >> 1))%int63 = (x >> 1) lor (y >> 1)).
+ assert (F1: ((x >> 1) + (y >> 1))%int = (x >> 1) lor (y >> 1)).
    apply IH.
    rewrite lsr_spec, Zpower_1_r; split; auto with zarith.
    apply Zdiv_lt_upper_bound; auto with zarith.
    rewrite lsr_spec, Zpower_1_r; split; auto with zarith.
    apply Zdiv_lt_upper_bound; auto with zarith.
    intros m H1 H2.
-   case_eq (digits <= m)%int63;  [idtac | rewrite <- not_true_iff_false];
+   case_eq (digits <= m)%int;  [idtac | rewrite <- not_true_iff_false];
      intros Heq.
    rewrite bit_M in H1; auto; discriminate.
    rewrite leb_spec in Heq.
-   apply (Hn (m + 1)%int63);
+   apply (Hn (m + 1)%int);
      rewrite <-bit_half; auto; rewrite ltb_spec; auto with zarith.
  rewrite (bit_split (x lor y)), lor_lsr, <- F1, lor_spec.
- replace (b2i (bit x 0 || bit y 0)) with (bit x 0 + bit y 0)%int63.
- 2: generalize (Hn 0%int63); do 2 case bit; auto; intros [ ]; auto.
+ replace (b2i (bit x 0 || bit y 0)) with (bit x 0 + bit y 0)%int.
+ 2: generalize (Hn 0%int); do 2 case bit; auto; intros [ ]; auto.
  rewrite lsl_add_distr.
  rewrite (bit_split x) at 1; rewrite (bit_split y) at 1.
- rewrite <-!add_assoc; apply f_equal2 with (f := add); auto.
- rewrite add_comm, <-!add_assoc; apply f_equal2 with (f := add); auto.
+ rewrite <-!add_assoc; apply f_equal2 with (f := add63); auto.
+ rewrite add_comm, <-!add_assoc; apply f_equal2 with (f := add63); auto.
  rewrite add_comm; auto.
  intros Heq.
  generalize (add_le_r x y); rewrite Heq, lor_le; intro Hb.
@@ -1474,7 +1487,7 @@ Proof.
          <-!add_assoc, (add_comm (bit y 0)), add_assoc, <-lsr_add_distr.
  rewrite (bit_split (x lor y)), lor_spec.
  intros Heq.
- assert (F: (bit x 0 + bit y 0)%int63 = (bit x 0 || bit y 0)).
+ assert (F: (bit x 0 + bit y 0)%int = (bit x 0 || bit y 0)).
   assert (F1: (2 | wB)) by (apply Zpower_divide; apply refl_equal).
   assert (F2: 0 < wB) by (apply refl_equal).
   assert (F3: [|bit x  0 + bit y 0|] mod 2 = [|bit x 0 || bit y 0|] mod 2).
@@ -1492,11 +1505,11 @@ Proof.
  rewrite lsr_spec, to_Z_1, Zpower_1_r; split; auto with zarith.
  apply Zdiv_lt_upper_bound; auto with zarith.
  intros _ HH m; case (to_Z_bounded m); intros H1m H2m.
- case_eq (digits <= m)%int63.
+ case_eq (digits <= m)%int.
  intros Hlm; rewrite bit_M; auto; discriminate.
  rewrite <- not_true_iff_false, leb_spec; intros Hlm.
  case (Zle_lt_or_eq 0 [|m|]); auto; intros Hm.
- replace m with ((m -1) + 1)%int63.
+ replace m with ((m -1) + 1)%int.
  rewrite <-(bit_half x), <-(bit_half y); auto with zarith.
  apply HH.
  rewrite <-lor_lsr.
@@ -1522,7 +1535,7 @@ Proof.
  rewrite ltb_spec, sub_spec, to_Z_1, Zmod_small; auto with zarith.
  apply to_Z_inj.
  rewrite add_spec, sub_spec, Zplus_mod_idemp_l, to_Z_1, Zmod_small; auto with zarith.
- replace m with 0%int63.
+ replace m with 0%int.
  intros Hbx Hby; generalize F; rewrite <-to_Z_eq, Hbx, Hby; discriminate.
  apply to_Z_inj; auto.
 Qed.
@@ -1541,13 +1554,13 @@ Proof.
  generalize (add_le_r (digits - p) n).
  case leb; try discriminate.
  rewrite sub_spec, Zmod_small; auto with zarith; intros H1.
- case_eq (n < p)%int63; try discriminate.
+ case_eq (n < p)%int; try discriminate.
  rewrite <- not_true_iff_false, ltb_spec; intros H2.
  case leb; try discriminate.
  intros _; rewrite bit_M; try discriminate.
  rewrite leb_spec, add_spec, Zmod_small, sub_spec, Zmod_small; auto with zarith.
  rewrite sub_spec, Zmod_small; auto with zarith.
-Qed. 
+Qed.
 
 Lemma lxor_comm: forall i1 i2 : int, i1 lxor i2 = i2 lxor i1.
 Proof.
@@ -1572,7 +1585,7 @@ Proof.
  intros;rewrite lxor_comm;apply lxor_0_l.
 Qed.
 
-Lemma lxor_nilpotent: forall i, i lxor i = 0%int63.
+Lemma lxor_nilpotent: forall i, i lxor i = 0%int.
 Proof.
  intros;apply bit_eq;intros.
  rewrite lxor_spec, xorb_nilpotent, bit_0;trivial.
@@ -1589,7 +1602,7 @@ Proof.
  intros;rewrite lor_comm;apply lor_0_l.
 Qed.
 
-Lemma reflect_leb : forall i j, reflect ([|i|] <= [|j|])%Z (i <= j)%int63.
+Lemma reflect_leb : forall i j, reflect ([|i|] <= [|j|])%Z (i <= j)%int.
 Proof.
  intros; apply iff_reflect.
  symmetry;apply leb_spec.
@@ -1601,7 +1614,7 @@ Proof.
  symmetry;apply eqb_spec.
 Qed.
 
-Lemma reflect_ltb : forall i j, reflect ([|i|] < [|j|])%Z (i < j)%int63.
+Lemma reflect_ltb : forall i j, reflect ([|i|] < [|j|])%Z (i < j)%int.
 Proof.
  intros; apply iff_reflect.
  symmetry;apply ltb_spec.
@@ -1620,18 +1633,18 @@ Proof.
  assert (W2 := to_Z_bounded n);clear n0.
  assert (W3 : [|n-1|] = [|n|] - 1).
    rewrite sub_spec, to_Z_1, Zmod_small;trivial;omega.
- assert (H1 : n = ((n-1)+1)%int63).
+ assert (H1 : n = ((n-1)+1)%int).
    apply to_Z_inj;rewrite add_spec, W3.
    rewrite Zmod_small;rewrite to_Z_1; omega.
  destruct (reflect_ltb (n-1) digits).
   rewrite <- ltb_spec in l.
   rewrite H1, <- !bit_half, H;trivial.
- assert ((digits <= n)%int63 = true).
+ assert ((digits <= n)%int = true).
   rewrite leb_spec;omega.
  rewrite !bit_M;trivial.
 Qed.
 
-Lemma lsr1_bit : forall i k, (bit i k >> 1 = 0)%int63.
+Lemma lsr1_bit : forall i k, (bit i k >> 1 = 0)%int.
 Proof.
  intros;destruct (bit i k);trivial.
 Qed.
@@ -1651,7 +1664,7 @@ Qed.
 Local Open Scope int63_scope.
 
 Lemma succ_max_int : forall x,
-  (x < max_int)%int63 = true -> (0 < x + 1)%int63 = true.
+  (x < max_int)%int = true -> (0 < x + 1)%int = true.
 Proof.
  intros x;rewrite ltb_spec, ltb_spec, add_spec.
  intros; assert (W:= to_Z_bounded x); assert (W1:= to_Z_bounded max_int).
@@ -1659,7 +1672,7 @@ Proof.
  rewrite Zmod_small;omega.
 Qed.
 
-Lemma leb_max_int : forall x, (x <= max_int)%int63 = true.
+Lemma leb_max_int : forall x, (x <= max_int)%int = true.
 Proof.
  intros x;rewrite leb_spec;assert (W:= to_Z_bounded x).
  change [|max_int|] with (wB - 1)%Z;omega.
@@ -1728,7 +1741,7 @@ Proof.
  intros x y;assert (W:= to_Z_bounded x);assert (W0:= to_Z_bounded y);
    rewrite leb_spec;intros;rewrite sub_spec, Zmod_small;omega.
 Qed.
- 
+
 Lemma not_0_ltb : forall x, x <> 0 <-> 0 < x = true.
 Proof.
  intros x;rewrite ltb_spec, to_Z_0;assert (W:=to_Z_bounded x);split.
@@ -1749,7 +1762,7 @@ Proof.
  generalize (leb_ltb_trans _ _ _ (leb_0 y) H).
  rewrite ltb_spec, leb_spec, to_Z_0, to_Z_1;auto with zarith.
 Qed.
- 
+
 Lemma to_Z_sub_1_diff : forall x, x <> 0 -> ([| x - 1|] = [|x|] - 1)%Z.
 Proof.
   intros x;rewrite not_0_ltb;apply to_Z_sub_1.
@@ -1760,7 +1773,7 @@ Proof.
   intros x y;assert (W:= to_Z_bounded x);assert (W0:= to_Z_bounded y);
    rewrite ltb_spec;intros;rewrite add_spec, to_Z_1, Zmod_small;omega.
 Qed.
- 
+
 Lemma ltb_leb_sub1 : forall x i,  x <> 0 -> (i < x = true <-> i <= x - 1 = true).
 Proof.
  intros x i Hdiff.
@@ -1778,8 +1791,8 @@ Qed.
 
 (** Iterators *)
 
-Lemma foldi_gt : forall A f from to (a:A), 
-  (to < from)%int63 = true -> foldi f from to a = a.
+Lemma foldi_gt : forall A f from to (a:A),
+  (to < from)%int = true -> foldi f from to a = a.
 Proof.
  intros;unfold foldi;rewrite foldi_cont_gt;trivial.
 Qed.
@@ -1790,14 +1803,14 @@ Proof.
  intros;unfold foldi;rewrite foldi_cont_eq;trivial.
 Qed.
 
-Lemma foldi_lt : forall A f from to (a:A), 
-  (from < to)%int63 = true -> foldi f from to a = foldi f (from + 1) to (f from a).
+Lemma foldi_lt : forall A f from to (a:A),
+  (from < to)%int = true -> foldi f from to a = foldi f (from + 1) to (f from a).
 Proof.
  intros;unfold foldi;rewrite foldi_cont_lt;trivial.
 Qed.
 
-Lemma fold_gt : forall A f from to (a:A), 
-  (to < from)%int63 = true -> fold f from to a = a.
+Lemma fold_gt : forall A f from to (a:A),
+  (to < from)%int = true -> fold f from to a = a.
 Proof.
  intros;apply foldi_gt;trivial.
 Qed.
@@ -1808,14 +1821,14 @@ Proof.
  intros;apply foldi_eq;trivial.
 Qed.
 
-Lemma fold_lt : forall A f from to (a:A), 
-  (from < to)%int63 = true -> fold f from to a = fold f (from + 1) to (f a).
+Lemma fold_lt : forall A f from to (a:A),
+  (from < to)%int = true -> fold f from to a = fold f (from + 1) to (f a).
 Proof.
  intros;apply foldi_lt;trivial.
 Qed.
 
 Lemma foldi_down_lt : forall A f from downto (a:A),
-  (from < downto)%int63 = true -> foldi_down f from downto a = a.
+  (from < downto)%int = true -> foldi_down f from downto a = a.
 Proof.
  intros;unfold foldi_down;rewrite foldi_down_cont_lt;trivial.
 Qed.
@@ -1827,15 +1840,15 @@ Proof.
 Qed.
 
 Lemma foldi_down_gt : forall A f from downto (a:A),
-  (downto < from)%int63 = true-> 
-  foldi_down f from downto a = 
+  (downto < from)%int = true->
+  foldi_down f from downto a =
   foldi_down f (from-1) downto (f from a).
 Proof.
  intros;unfold foldi_down;rewrite foldi_down_cont_gt;trivial.
 Qed.
 
 Lemma fold_down_lt : forall A f from downto (a:A),
-  (from < downto)%int63 = true -> fold_down f from downto a = a.
+  (from < downto)%int = true -> fold_down f from downto a = a.
 Proof.
  intros;apply foldi_down_lt;trivial.
 Qed.
@@ -1847,8 +1860,8 @@ Proof.
 Qed.
 
 Lemma fold_down_gt : forall A f from downto (a:A),
-  (downto < from)%int63 = true-> 
-  fold_down f from downto a = 
+  (downto < from)%int = true->
+  fold_down f from downto a =
   fold_down f (from-1) downto (f a).
 Proof.
  intros;apply foldi_down_gt;trivial.
@@ -1857,8 +1870,8 @@ Qed.
 Require Import Wf_Z.
 
 Lemma int_ind : forall (P:int -> Type),
-  P 0%int63 ->
-  (forall i, (i < max_int)%int63 = true -> P i -> P (i + 1)%int63) ->
+  P 0%int ->
+  (forall i, (i < max_int)%int = true -> P i -> P (i + 1)%int) ->
   forall i, P i.
 Proof.
  intros P HP0 Hrec.
@@ -1868,7 +1881,7 @@ Proof.
  assert (W:= to_Z_bounded i).
  assert ([|i - 1|] = [|i|] - 1)%Z.
   rewrite sub_spec, Zmod_small;rewrite to_Z_1;auto with zarith.
- assert (i = i - 1 + 1)%int63.
+ assert (i = i - 1 + 1)%int.
   apply to_Z_inj.
   rewrite add_spec, H2.
   rewrite Zmod_small;rewrite to_Z_1;auto with zarith.
@@ -1878,7 +1891,7 @@ Proof.
  intros;apply (X [|i|]);trivial.
  destruct (to_Z_bounded i);trivial.
 Qed.
- 
+
 Lemma int_ind_bounded : forall (P:int-> Type) min max,
   min <= max =true ->
   P max ->
@@ -1888,22 +1901,22 @@ Proof.
  intros P min max Hle.
  intros Hmax Hrec.
  assert (W1:= to_Z_bounded max);assert (W2:= to_Z_bounded min).
- assert (forall z, (0 <= z)%Z -> (z <= [|max|] - [|min|])%Z  -> forall i, z = [|i|] -> P (max - i)%int63).
+ assert (forall z, (0 <= z)%Z -> (z <= [|max|] - [|min|])%Z  -> forall i, z = [|i|] -> P (max - i)%int).
  intros z H1;pattern z;apply natlike_rec2;intros;trivial.
- assert (max - i = max)%int63.
+ assert (max - i = max)%int.
   apply to_Z_inj;rewrite sub_spec, <- H0, Zminus_0_r, Zmod_small;auto using to_Z_bounded.
  rewrite H2;trivial.
  assert (W3:= to_Z_bounded i);apply Hrec.
  rewrite leb_spec,add_spec, sub_spec, to_Z_1, (Zmod_small ([|max|] - [|i|])), Zmod_small;auto with zarith.
  rewrite ltb_spec, sub_spec, Zmod_small;auto with zarith.
- assert (max - i + 1 = max - (i - 1))%int63.
+ assert (max - i + 1 = max - (i - 1))%int.
   apply to_Z_inj;rewrite add_spec, !sub_spec, to_Z_1.
   rewrite (Zmod_small ([|max|] - [|i|]));auto with zarith.
   rewrite (Zmod_small ([|i|] - 1));auto with zarith.
   apply f_equal2;auto with zarith.
  rewrite H3;apply X;auto with zarith.
  rewrite sub_spec, to_Z_1, <- H2, Zmod_small;auto with zarith.
- rewrite leb_spec in Hle;assert (min = max - (max - min))%int63.
+ rewrite leb_spec in Hle;assert (min = max - (max - min))%int.
   apply to_Z_inj.
   rewrite !sub_spec, !Zmod_small;auto with zarith.
   rewrite Zmod_small;auto with zarith.
@@ -1933,11 +1946,12 @@ Proof.
  rewrite foldi_cont_gt;trivial;apply Ha;rewrite <- ltb_spec;trivial.
 Qed.
 
-Lemma of_pos_spec : forall p, [|of_pos p|] = Zpos p mod wB. 
+
+Lemma of_pos_spec : forall p, [|of_pos p|] = Zpos p mod wB.
 Proof.
  unfold of_pos.
  unfold wB.
- assert (forall k, (k <= size)%nat -> 
+ assert (forall k, (k <= size)%nat ->
    forall p : positive, [|of_pos_rec k p|] = Zpos p mod 2 ^ Z_of_nat k).
   induction k.
   simpl;intros;rewrite to_Z_0,Zmod_1_r;trivial.
@@ -1969,7 +1983,7 @@ Transparent Z_of_nat.
   intros n H1 H2.
   rewrite bit_1, eqb_spec in H2;subst.
   rewrite bit_lsl in H1;discriminate H1.
-  
+
   change (Zpos p~0) with (2*(Zpos p))%Z.
   rewrite lsl_spec, IHk, to_Z_1.
   rewrite Zmult_comm, Zmod_small.
@@ -1988,7 +2002,7 @@ Transparent Z_of_nat.
   split;auto with zarith.
   apply Zpower_gt_1;auto with zarith.
   rewrite inj_S;auto with zarith.
-  
+
   apply H;auto with zarith.
 Qed.
 
@@ -2036,15 +2050,15 @@ Proof.
  apply foldi_cont_ZInd;trivial.
 Qed.
 
-Lemma foldi_ZInd : forall A (P : Z -> A -> Prop) f min max a,  
+Lemma foldi_ZInd : forall A (P : Z -> A -> Prop) f min max a,
   (max < min = true -> P ([|max|] + 1)%Z a) ->
   P [|min|] a ->
-  (forall i a, min <= i = true -> i <= max = true -> 
+  (forall i a, min <= i = true -> i <= max = true ->
       P [|i|] a -> P ([|i|] + 1)%Z (f i a)) ->
   P ([|max|]+1)%Z (foldi f min max a).
 Proof.
  unfold foldi;intros A P f min max a Hlt;intros.
- set (P' z cont := 
+ set (P' z cont :=
        if Zlt_bool [|max|] z then cont = (fun a0 : A => a0)
        else forall a, P z a -> P ([|max|]+1)%Z (cont a)).
  assert (P' [|min|] (foldi_cont (fun (i : int) (cont : A -> A) (a0 : A) => cont (f i a0)) min
@@ -2062,17 +2076,17 @@ Proof.
  rewrite <- Zlt_is_lt_bool, <- ltb_spec;intros;rewrite foldi_cont_gt;auto.
 Qed.
 
-Lemma foldi_Ind : forall A (P : int -> A -> Prop) f min max a,  
+Lemma foldi_Ind : forall A (P : int -> A -> Prop) f min max a,
   (max < max_int = true) ->
   (max < min = true -> P (max + 1) a) ->
   P min a ->
-  (forall i a, min <= i = true -> i <= max = true -> 
+  (forall i a, min <= i = true -> i <= max = true ->
       P i a -> P (i + 1) (f i a)) ->
   P (max+1) (foldi f min max a).
 Proof.
  intros.
  set (P' z a := (0 <= z < wB)%Z -> P (of_Z z) a).
- assert (W:= to_Z_add_1 _ _ H). 
+ assert (W:= to_Z_add_1 _ _ H).
  assert (P' ([|max|]+1)%Z (foldi f min max a)).
  apply foldi_ZInd;unfold P';intros.
  rewrite <- W, of_to_Z;auto.
@@ -2102,7 +2116,7 @@ Qed.
 
 Lemma foldi_down_cont_ZInd :
    forall A B (P: Z -> (A -> B) -> Prop) (f:int -> (A -> B) -> (A -> B)) max min cont,
-   (forall z, (z < [|min|])%Z -> P z cont) -> 
+   (forall z, (z < [|min|])%Z -> P z cont) ->
    (forall i cont, min <= i = true -> i <= max = true -> P ([|i|] - 1)%Z cont -> P [|i|] (f i cont)) ->
    P [|max|] (foldi_down_cont f max min cont).
 Proof.
@@ -2150,12 +2164,12 @@ Qed.
 Lemma foldi_down_ZInd :
    forall A (P: Z -> A -> Prop) (f:int -> A -> A) max min a,
    (max < min = true -> P ([|min|] - 1)%Z a) ->
-   (P [|max|] a) -> 
+   (P [|max|] a) ->
    (forall i a, min <= i = true -> i <= max = true -> P [|i|]%Z a -> P ([|i|]-1)%Z (f i a)) ->
    P ([|min|] - 1)%Z (foldi_down f max min a).
 Proof.
  unfold foldi_down;intros A P f max min a Hlt;intros.
- set (P' z cont := 
+ set (P' z cont :=
        if Zlt_bool z [|min|] then cont = (fun a0 : A => a0)
        else forall a, P z a -> P ([|min|] - 1)%Z (cont a)).
  assert (P' [|max|] (foldi_down_cont (fun (i : int) (cont : A -> A) (a0 : A) => cont (f i a0)) max
@@ -2193,13 +2207,13 @@ Lemma foldi_down_Ind :
    forall A (P: int -> A -> Prop) (f:int -> A -> A) max min a,
    0 < min = true ->
    (max < min = true -> P (min - 1) a) ->
-   (P max a) -> 
+   (P max a) ->
    (forall i a, min <= i = true -> i <= max = true -> P i a -> P (i - 1) (f i a)) ->
    P (min - 1) (foldi_down f max min a).
 Proof.
  intros.
  set (P' z a := (0 <= z < wB)%Z -> P (of_Z z) a).
- assert (W:= to_Z_sub_1 _ _ H). 
+ assert (W:= to_Z_sub_1 _ _ H).
  assert (P' ([|min|]-1)%Z (foldi_down f max min a)).
  apply foldi_down_ZInd;unfold P';intros.
  rewrite <- W, of_to_Z;auto.
@@ -2211,13 +2225,13 @@ Proof.
  unfold P' in H3;rewrite <- W, of_to_Z in H3;apply H3;apply to_Z_bounded.
 Qed.
 
-Lemma foldi_down_min : 
+Lemma foldi_down_min :
   forall A f min max (a:A),
   min < max_int = true->
   (min <= max) = true ->
   foldi_down f max min a = f min (foldi_down f max (min + 1) a).
 Proof.
-  intros. 
+  intros.
   set (P:= fun i => i <= max - min = true ->
        forall a, foldi_down f (min + i) min a = f min (foldi_down f (min + i) (min + 1) a)).
   assert (min < min + 1 = true).
@@ -2230,7 +2244,7 @@ Proof.
     intros i Hi Hrec Hi1 a'.
     rewrite add_assoc.
     assert (Wi:= to_Z_add_1 _ _ Hi).
-    assert (Wmin:= to_Z_add_1 _ _ H). 
+    assert (Wmin:= to_Z_add_1 _ _ H).
     assert ((min + 1) <= (min + i + 1) = true).
       assert (W1 := to_Z_bounded min); assert (W2:= to_Z_bounded max); assert (W3:= to_Z_bounded i).
       replace (min + i + 1) with (min + 1 + i).
@@ -2247,7 +2261,7 @@ Proof.
       apply Hrec.
       apply leb_trans with (i+1);[rewrite leb_spec;omega | trivial].
       apply to_Z_inj;rewrite sub_spec, (add_spec (min + i)), to_Z_1, Zminus_mod_idemp_l.
-      replace ([|min + i|] + 1 - 1)%Z with [|min + i|] by ring.
+      assert (H100: forall (x:Z), (x + 1 - 1)%Z = x) by (intros; ring). rewrite H100.
       rewrite Zmod_small;auto using to_Z_bounded.
       apply leb_ltb_trans with (2:= Hlt).
       rewrite leb_spec;omega.
@@ -2513,7 +2527,7 @@ Proof.
 Qed.
 
 
-Lemma forallb_spec : forall f from to, 
+Lemma forallb_spec : forall f from to,
   forallb f from to = true <->
   forall i, from <= i = true -> i <= to = true -> f i = true.
 Proof.
@@ -2568,10 +2582,11 @@ Proof.
  rewrite H2, H;trivial.
 Qed.
 
-Lemma bit_max_int : forall i, (i < digits)%int63 = true -> bit max_int i = true.
+
+Lemma bit_max_int : forall i, (i < digits)%int = true -> bit max_int i = true.
 Proof.
  intros;apply (forallb_spec (bit max_int) 0 (digits - 1)).
- compute;trivial.
+ vm_compute;trivial.
  apply leb_0.
  rewrite ltb_spec in H.
  destruct (to_Z_bounded i);rewrite leb_spec.
@@ -2594,3 +2609,47 @@ Proof.
  intros;rewrite land_comm;apply land_max_int_l.
 Qed.
 
+
+(* int is an OrderedType *)
+
+Require Import OrderedType.
+
+Module IntOrderedType <: OrderedType.
+
+  Definition t := int.
+
+  Definition eq x y := (x == y) = true.
+
+  Definition lt x y := (x < y) = true.
+
+  Lemma eq_refl x : eq x x.
+  Proof. unfold eq. rewrite eqb_spec. reflexivity. Qed.
+
+  Lemma eq_sym x y : eq x y -> eq y x.
+  Proof. unfold eq. rewrite !eqb_spec. intros ->. reflexivity. Qed.
+
+  Lemma eq_trans x y z : eq x y -> eq y z -> eq x z.
+  Proof. unfold eq. rewrite !eqb_spec. intros -> ->. reflexivity. Qed.
+
+  Lemma lt_trans x y z : lt x y -> lt y z -> lt x z.
+  Proof. apply ltb_trans. Qed.
+
+  Lemma lt_not_eq x y : lt x y -> ~ eq x y.
+  Proof. unfold lt, eq. rewrite ltb_negb_geb, eqb_spec. intros H1 H2. rewrite H2, leb_refl in H1. discriminate. Qed.
+
+  Definition compare x y : Compare lt eq x y.
+  Proof.
+    case_eq (x < y); intro e.
+      exact (LT e).
+      case_eq (x == y); intro e2.
+        exact (EQ e2). apply GT. unfold lt. rewrite ltb_negb_geb, leb_ltb_eqb, e, e2. reflexivity.
+  Defined.
+
+  Definition eq_dec x y : { eq x y } + { ~ eq x y }.
+  Proof.
+    case_eq (x == y); intro e.
+      left; exact e.
+      right. intro H. rewrite H in e. discriminate.
+  Defined.
+
+End IntOrderedType.
diff --git a/src/versions/standard/Int63/Int63_standard.v b/src/versions/standard/Int63/Int63_standard.v
index 3540b71..1499dd3 100644
--- a/src/versions/standard/Int63/Int63_standard.v
+++ b/src/versions/standard/Int63/Int63_standard.v
@@ -14,6 +14,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
+
+(** Naive software representation of Int63. To improve. Anyway, if you
+    want efficiency, rather use native-coq. **)
+
+Require Export Cyclic63.
+Require Export Ring63.
 Require Export Int63Native.
 Require Export Int63Op.
 Require Export Int63Axioms.
diff --git a/src/versions/standard/Int63/Ring63_standard.v b/src/versions/standard/Int63/Ring63_standard.v
new file mode 100644
index 0000000..7b9fc1f
--- /dev/null
+++ b/src/versions/standard/Int63/Ring63_standard.v
@@ -0,0 +1,114 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** * Int63 numbers defines Z/(2^63)Z, and can hence be equipped
+      with a ring structure and a ring tactic *)
+
+Require Import Int63Lib Cyclic63 CyclicAxioms.
+
+Local Open Scope int63_scope.
+
+(** Detection of constants *)
+
+Local Open Scope list_scope.
+
+Ltac isInt63cst_lst l :=
+ match l with
+ | nil => constr:true
+ | ?t::?l => match t with
+               | D1 => isInt63cst_lst l
+               | D0 => isInt63cst_lst l
+               | _ => constr:false
+             end
+ | _ => constr:false
+ end.
+
+Ltac isInt63cst t :=
+ match t with
+ | I63 ?i0 ?i1 ?i2 ?i3 ?i4 ?i5 ?i6 ?i7 ?i8 ?i9 ?i10
+       ?i11 ?i12 ?i13 ?i14 ?i15 ?i16 ?i17 ?i18 ?i19 ?i20
+       ?i21 ?i22 ?i23 ?i24 ?i25 ?i26 ?i27 ?i28 ?i29 ?i30
+       ?i31 ?i32 ?i33 ?i34 ?i35 ?i36 ?i37 ?i38 ?i39 ?i40
+       ?i41 ?i42 ?i43 ?i44 ?i45 ?i46 ?i47 ?i48 ?i49 ?i50
+       ?i51 ?i52 ?i53 ?i54 ?i55 ?i56 ?i57 ?i58 ?i59 ?i60
+       ?i61 ?i62 =>
+    let l :=
+      constr:(i0::i1::i2::i3::i4::i5::i6::i7::i8::i9::i10
+      ::i11::i12::i13::i14::i15::i16::i17::i18::i19::i20
+      ::i21::i22::i23::i24::i25::i26::i27::i28::i29::i30
+      ::i31::i32::i33::i34::i35::i36::i37::i38::i39::i40
+      ::i41::i42::i43::i44::i45::i46::i47::i48::i49::i50
+      ::i51::i52::i53::i54::i55::i56::i57::i58::i59::i60
+      ::i61::i62::nil)
+    in isInt63cst_lst l
+ | Int63Lib.On => constr:true
+ | Int63Lib.In => constr:true
+ | Int63Lib.Tn => constr:true
+ | Int63Lib.Twon => constr:true
+ | _ => constr:false
+ end.
+
+Ltac Int63cst t :=
+ match isInt63cst t with
+ | true => constr:t
+ | false => constr:NotConstant
+ end.
+
+(** The generic ring structure inferred from the Cyclic structure *)
+
+Module Int63ring := CyclicRing Int63Cyclic.
+
+(** Unlike in the generic [CyclicRing], we can use Leibniz here. *)
+
+Lemma Int63_canonic : forall x y, phi x = phi y -> x = y.
+Proof.
+ intros x y EQ.
+ now rewrite <- (phi_inv_phi x), <- (phi_inv_phi y), EQ.
+Qed.
+
+Lemma ring_theory_switch_eq :
+ forall A (R R':A->A->Prop) zero one add mul sub opp,
+  (forall x y : A, R x y -> R' x y) ->
+  ring_theory zero one add mul sub opp R ->
+  ring_theory zero one add mul sub opp R'.
+Proof.
+intros A R R' zero one add mul sub opp Impl Ring.
+constructor; intros; apply Impl; apply Ring.
+Qed.
+
+Lemma Int63Ring : ring_theory 0 1 add63 mul63 sub63 opp63 Logic.eq.
+Proof.
+exact (ring_theory_switch_eq _ _ _ _ _ _ _ _ _ Int63_canonic Int63ring.CyclicRing).
+Qed.
+
+Lemma eqb63_eq : forall x y, eqb63 x y = true <-> x=y.
+Proof.
+unfold eqb63. intros x y.
+rewrite Cyclic63.spec_compare. case Z.compare_spec.
+intuition. apply Int63_canonic; auto.
+intuition; subst; auto with zarith; try discriminate.
+intuition; subst; auto with zarith; try discriminate.
+Qed.
+
+Lemma eqb63_correct : forall x y, eqb63 x y = true -> x=y.
+Proof. now apply eqb63_eq. Qed.
+
+Add Ring Int63Ring : Int63Ring
+ (decidable eqb63_correct,
+  constants [Int63cst]).
+
+Section TestRing.
+Let test : forall x y, 1 + x*y + x*x + 1 = 1*1 + 1 + y*x + 1*x*x.
+intros. ring.
+Qed.
+
+Let test2 : forall x, (x - 1) + 1 = x.
+intros. ring.
+Qed.
+End TestRing.
+
diff --git a/src/versions/standard/Make b/src/versions/standard/Make
index 4325d32..9e7b56b 100644
--- a/src/versions/standard/Make
+++ b/src/versions/standard/Make
@@ -43,6 +43,9 @@ CAMLLEX = $(CAMLBIN)ocamllex
 CAMLYACC = $(CAMLBIN)ocamlyacc
 
 versions/standard/Int63/Int63.v
+versions/standard/Int63/Int63Lib.v
+versions/standard/Int63/Cyclic63.v
+versions/standard/Int63/Ring63.v
 versions/standard/Int63/Int63Native.v
 versions/standard/Int63/Int63Op.v
 versions/standard/Int63/Int63Axioms.v
diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile
index f22a0af..127e8b2 100644
--- a/src/versions/standard/Makefile
+++ b/src/versions/standard/Makefile
@@ -147,6 +147,9 @@ VFILES:=Trace.v\
   versions/standard/Int63/Int63Axioms.v\
   versions/standard/Int63/Int63Op.v\
   versions/standard/Int63/Int63Native.v\
+  versions/standard/Int63/Ring63.v\
+  versions/standard/Int63/Cyclic63.v\
+  versions/standard/Int63/Int63Lib.v\
   versions/standard/Int63/Int63.v
 
 -include $(addsuffix .d,$(VFILES))