Start porting to the standard version of Coq (not finished yet)

10 files changed, 4070 insertions, 0 deletions

diff --git a/src/configure.sh b/src/configure.sh
index d889828..277f560 100755
--- a/src/configure.sh
+++ b/src/configure.sh
@@ -4,6 +4,12 @@ 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/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
+    cp versions/standard/Int63/Int63Properties_standard.v versions/standard/Int63/Int63Properties.v
+    cp versions/standard/Array/PArray_standard.v versions/standard/Array/PArray.v
 else
     cp versions/native/Makefile Makefile
 fi
diff --git a/src/versions/standard/Array/PArray_standard.v b/src/versions/standard/Array/PArray_standard.v
new file mode 100644
index 0000000..f27664e
--- /dev/null
+++ b/src/versions/standard/Array/PArray_standard.v
@@ -0,0 +1,362 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*       from the PArray library of native-coq                            *)
+(*       by Benjamin Gregoire and Laurent Thery                           *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+Require Export Int63.
+
+Register array : Type -> Type as array_type.
+
+Register make : forall {A:Type}, int -> A -> array A as array_make.
+
+Register get : forall {A:Type}, array A -> int -> A as array_get.
+
+Register default : forall {A:Type}, array A -> A as array_default.
+
+Register set : forall {A:Type}, array A -> int -> A -> array A as array_set.
+
+Register length : forall {A:Type}, array A -> int as array_length.
+
+Register copy : forall {A:Type}, array A -> array A as array_copy.
+
+Register reroot : forall {A:Type}, array A -> array A as array_reroot.
+
+(* Not done with the vm *)
+Register init : forall {A:Type}, int -> (int -> A) -> A -> array A as array_init.
+
+Register map : forall {A B:Type}, (A -> B) -> array A -> array B as array_map.
+
+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.
+
+(** Axioms *)
+Axiom get_outofbound : forall A (t:array A) i, (i < length t) = false -> t.[i] = default t.
+
+Axiom get_set_same : forall A t i (a:A), (i < length t) = true -> t.[i<-a].[i] = a.
+Axiom get_set_other : forall A t i j (a:A), i <> j -> t.[i<-a].[j] = t.[j].
+Axiom default_set : forall A t i (a:A), default (t.[i<-a]) = default t.
+
+
+Axiom get_make : forall A (a:A) size i, (make size a).[i] = a.
+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), 
+  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.
+
+Axiom get_copy : forall A (t:array A) i, (copy t).[i] = t.[i].
+Axiom length_copy : forall A (t:array A), length (copy t) = length t.
+
+Axiom get_reroot : forall A (t:array A) i, (reroot t).[i] = t.[i].
+Axiom length_reroot : forall A (t:array A), length (reroot t) = length t.
+
+
+Axiom length_init : forall A f size (def:A),
+  length (init size f def) = if size <= max_array_length then size else max_array_length.
+
+Axiom get_init : forall A f size (def:A) i,
+  (init size f def).[i] = if i < length (init size f def) then f i else def.
+
+Axiom default_init : forall A f size (def:A), default (init size f def) = def.
+
+(* Rename this ? *)
+Axiom get_ext : forall A (t1 t2:array A),
+  length t1 = length t2 ->
+  (forall i, i < length t1 = true -> t1.[i] = t2.[i]) ->
+  default t1 = default t2 ->
+  t1 = t2.
+
+(* Definition *)
+Definition to_list {A:Type} (t:array A) :=
+  let len := length t in
+  if 0 == len then nil
+  else foldi_down (fun i l => t.[i] :: l)%list (len - 1) 0 nil.
+
+Definition forallbi {A:Type} (f:int-> A->bool) (t:array A) :=
+  let len := length t in
+  if 0 == len then true
+  else forallb (fun i => f i (t.[i])) 0 (len - 1).
+
+Definition forallb {A:Type} (f: A->bool) (t:array A) :=
+  let len := length t in
+  if 0 == len then true
+  else forallb (fun i => f (t.[i])) 0 (len - 1).
+
+Definition existsbi {A:Type} (f:int->A->bool) (t:array A) :=
+  let len := length t in
+  if 0 == len then false
+  else existsb (fun i => f i (t.[i])) 0 (len - 1).
+
+Definition existsb {A:Type} (f:A->bool) (t:array A) :=
+  let len := length t in
+  if 0 == len then false
+  else existsb (fun i => f (t.[i])) 0 (len - 1).
+
+(* TODO : We should add init as native and add it *)
+Definition mapi {A B:Type} (f:int->A->B) (t:array A) :=
+  let size := length t in
+  let def := f size (default t) in
+  let tb := make size def in
+  if size == 0 then tb
+  else foldi (fun i tb => tb.[i<- f i (t.[i])]) 0 (size - 1) tb.
+
+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 
+  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 
+  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 
+  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 
+  else foldi_down (fun i b => f (t.[i]) b) (len - 1) 0 b.
+
+(* Lemmas *)
+
+Lemma default_copy : forall A (t:array A), default (copy t) = default t.
+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.
+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 : 
+   forall (A : Type) (t : array A) (i : int) ,
+       (t .[ i <- default t]) .[ i] = default t.
+Proof.
+ intros A t i;case_eq (i < (length t));intros.
+ rewrite get_set_same;trivial.
+ rewrite get_outofbound, default_set;trivial.
+ rewrite length_set;trivial.
+Qed.
+
+Lemma get_not_default_lt : forall A (t:array A) x,
+ t.[x] <> default t -> (x < length t)%int63 = 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 : 
+     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 ->
+     P (length t) (foldi_left f a t).
+Proof.
+ intros;unfold foldi_left.
+ destruct (reflect_eqb 0 (length t)).
+  rewrite <- e;trivial.
+ assert ((length t - 1) + 1 = length t) by ring.
+ rewrite <- H1 at 1;apply foldi_Ind;auto.
+ assert (W:= leb_max_int (length t));rewrite leb_spec in W.
+ rewrite ltb_spec, to_Z_sub_1_diff;auto with zarith.
+ intros Hlt;elim (ltb_0 _ Hlt).
+ intros;apply H;trivial. rewrite ltb_leb_sub1;auto.
+Qed.
+
+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 ->
+     P (length t) (fold_left f a t).
+Proof.
+ intros.
+ apply (foldi_left_Ind A B P (fun i => f));trivial.
+Qed.
+
+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 ->
+     P (fold_left f a t).
+Proof.
+ intros;apply (fold_left_Ind A B (fun _ => P));trivial.
+Qed.
+
+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 ->
+     P 0 (foldi_right f t a).
+Proof.
+ intros;unfold foldi_right.
+ destruct (reflect_eqb 0 (length t)).
+  rewrite e;trivial.
+ set (P' z a := (*-1 <= z < [|length t|] ->*) P (of_Z (z + 1)) a).
+ assert (P' ([|0|] - 1)%Z (foldi_down (fun (i : int) (b : A) => f i (t .[ i]) b) (length t - 1) 0 a)).
+ apply foldi_down_ZInd;unfold P'.
+ intros Hlt;elim (ltb_0 _ Hlt).
+ rewrite to_Z_sub_1_diff;auto.
+ ring_simplify ([|length t|] - 1 + 1)%Z;rewrite of_to_Z;trivial.
+ intros;ring_simplify ([|i|] - 1 + 1)%Z;rewrite of_to_Z;auto.
+ assert (i < length t = true).
+   rewrite ltb_leb_sub1;auto.
+ apply H;trivial.
+ rewrite <-(to_Z_add_1 _ _ H4), of_to_Z in H3;auto.
+ exact H1.
+Qed.
+ 
+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 ->
+     P 0 (fold_right f t a).
+Proof.
+ intros;apply (foldi_right_Ind A B P (fun i => f));trivial.
+Qed.
+
+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 ->
+     P (fold_right f t a).
+Proof.
+ intros;apply (fold_right_Ind A B (fun i => P));trivial.
+Qed.
+
+Lemma forallbi_spec : forall A (f : int -> A -> bool) t,
+  forallbi f t = true <-> forall i, i < length t = true -> f i (t.[i]) = true.
+Proof.
+ unfold forallbi;intros A f t.
+ destruct (reflect_eqb 0 (length t)).
+ split;[intros | trivial].
+ elim (ltb_0 i);rewrite e;trivial.
+ rewrite forallb_spec;split;intros Hi i;intros;apply Hi.
+ apply leb_0. rewrite <- ltb_leb_sub1;auto. rewrite ltb_leb_sub1;auto.
+Qed.
+
+Lemma forallb_spec : forall A (f : A -> bool) t,
+  forallb f t = true <-> forall i, i < length t = true -> f (t.[i]) = true.
+Proof.
+ intros A f;apply (forallbi_spec A (fun i => f)).
+Qed.
+
+Lemma existsbi_spec : forall A (f : int -> A -> bool) t,
+  existsbi f t = true <-> exists i, i < length t = true /\ f i (t.[i]) = true.
+Proof.
+ unfold existsbi;intros A f t.
+ destruct (reflect_eqb 0 (length t)).
+ split;[discriminate | intros [i [Hi _]];rewrite <- e in Hi;elim (ltb_0 _ Hi)].
+ rewrite existsb_spec. repeat setoid_rewrite Bool.andb_true_iff.
+ split;intros [i H];decompose [and] H;clear H;exists i;repeat split;trivial.
+ rewrite ltb_leb_sub1;auto. apply leb_0. rewrite <- ltb_leb_sub1;auto.
+Qed.
+
+Lemma existsb_spec : forall A (f : A -> bool) t,
+  existsb f t = true <-> exists i, i < length t = true /\ f (t.[i]) = true.
+Proof.
+ intros A f;apply (existsbi_spec A (fun i => f)).
+Qed.
+
+Local Open Scope list_scope.
+
+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.
+
+Lemma to_list_to_list_ntr : forall A (t:array A),
+   to_list t = to_list_ntr _ t.
+Proof.
+ unfold to_list, to_list_ntr; intros A t.
+ destruct (reflect_eqb 0 (length t));trivial.
+ rewrite foldi_ntr_foldi_down;trivial.
+ apply leb_ltb_trans with max_array_length;[ | trivial].
+ apply leb_trans with (length t);[ | apply ltb_length].
+ rewrite leb_spec, sub_spec.
+ rewrite to_Z_1, Zmod_small;try omega.
+ generalize (to_Z_bounded (length t)).
+ 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.
+  intros A B t f;rewrite to_list_to_list_ntr.
+  unfold fold_left, to_list_ntr; destruct (reflect_eqb 0 (length t));[trivial | ].
+  set (P1 := fun i => forall b,
+      foldi (fun (i : int) (a : B) => f a (t .[ i])) i (length t - 1) b =
+      List.fold_left f
+        (foldi_ntr (list A) (fun (i : int) (l : list A) => t .[ i] :: l) i
+           (length t - 1) nil) b).
+  assert (W: P1 0);[ | trivial].
+  apply int_ind_bounded with (max := length t - 1);unfold P1.
+  apply leb_0.
+  intros b;unfold foldi_ntr;rewrite foldi_eq, foldi_cont_eq;trivial.
+  intros i _ Hlt Hrec b.
+  unfold foldi_ntr;rewrite foldi_lt, foldi_cont_lt;trivial;simpl.
+  apply Hrec.
+Qed.
+
+Require Import Bool.
+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) && 
+  forallbi (fun i a1 => Aeqb a1 (t2.[i])) t1.
+
+Lemma reflect_eqb : forall (A:Type) (Aeqb:A->A->bool),
+  (forall a1 a2, reflect (a1 = a2) (Aeqb a1 a2)) ->
+  forall t1 t2, reflect (t1 = t2) (eqb Aeqb t1 t2).
+Proof.
+ intros A Aeqb HA t1 t2.
+ case_eq (eqb Aeqb t1 t2);unfold eqb;intros H;constructor.
+ rewrite !andb_true_iff in H;destruct H as [[H1 H2] H3].
+ apply get_ext.
+ rewrite (reflect_iff _ _ (reflect_eqb _ _));trivial.
+ rewrite forallbi_spec in H3.
+ intros i Hlt;rewrite (reflect_iff _ _ (HA _ _));auto.
+ rewrite (reflect_iff _ _ (HA _ _));trivial.
+ intros Heq;rewrite Heq in H;clear Heq.
+ revert H; rewrite Int63Axioms.eqb_refl;simpl.
+ case_eq (Aeqb (default t2) (default t2));simpl;intros H0 H1.
+ rewrite <- not_true_iff_false, forallbi_spec in H1;apply H1.
+ 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/Int63Axioms_standard.v b/src/versions/standard/Int63/Int63Axioms_standard.v
new file mode 100644
index 0000000..6bc1b3c
--- /dev/null
+++ b/src/versions/standard/Int63/Int63Axioms_standard.v
@@ -0,0 +1,135 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*       from the Int63 library of native-coq                             *)
+(*       by Benjamin Gregoire and Laurent Thery                           *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+Require Import Bvector.
+Require Export BigNumPrelude.
+Require Export Int63Native.
+Require Export Int63Op.
+
+Definition wB := (2^(Z_of_nat size)).
+
+Notation "[| x |]" := (to_Z x)  (at level 0, x at level 99) : int63_scope.
+
+Notation "[+| c |]" :=
+   (interp_carry 1 wB to_Z c)  (at level 0, x at level 99) : int63_scope.
+
+Notation "[-| c |]" :=
+   (interp_carry (-1) wB to_Z c)  (at level 0, x at level 99) : int63_scope.
+
+Notation "[|| x ||]" :=
+   (zn2z_to_Z wB to_Z x)  (at level 0, x at level 99) : int63_scope.
+
+Local Open Scope int63_scope.
+Local Open Scope Z_scope.
+
+(* Bijection : int63 <-> Bvector size *)
+
+Axiom to_Z_inj : forall x y, [|x|] = [|y|] -> x = y.
+
+Axiom of_to_Z : forall x, of_Z ([|x|]) = x.
+
+(** Specification of logical operations *)
+Axiom lsl_spec : forall x p, [| x << p |] = [|x|] * 2^[|p|] mod wB.
+
+Axiom lsr_spec : forall x p, [|x >> p|] = [|x|] / 2 ^ [|p|].
+
+Axiom land_spec: forall x y i , bit (x land y) i = bit x i && bit y i.
+
+Axiom lor_spec: forall x y i, bit (x lor y) i = bit x i || bit y i.
+
+Axiom lxor_spec: forall  x y i, bit (x lxor y) i = xorb (bit x i) (bit y i).
+
+(** Specification of basic opetations *)
+
+(* Arithmetic modulo operations *)
+
+(* Remarque : les axiomes seraient plus simple si on utilise of_Z a la place :
+   exemple : add_spec : forall x y, of_Z (x + y) = of_Z x + of_Z y. *)
+
+Axiom add_spec : forall x y, [|x + y|] = ([|x|] + [|y|]) mod wB.
+
+Axiom sub_spec : forall x y, [|x - y|] = ([|x|] - [|y|]) mod wB.
+
+Axiom mul_spec : forall x y, [| x * y |]  = [|x|] * [|y|] mod wB.
+
+Axiom mulc_spec : forall x y, [|x|] * [|y|] = [|fst (mulc x y)|] * wB + [|snd (mulc x y)|].
+
+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 ltb_spec : forall x y, (x < y)%int63 = true <-> [|x|] < [|y|].
+
+Axiom leb_spec : forall x y, (x <= y)%int63 = 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.
+
+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').
+
+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.
+
+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 = 
+  f from (fun a' => foldi_down_cont f (from-1) downto cont a').
+
+(** Print *)
+
+Axiom print_int_spec : forall x, x = print_int x.
+
+(** Axioms on operations which are just short cut *)
+
+Axiom compare_def_spec : forall x y, compare x y = compare_def x y.
+
+Axiom head0_spec  : forall x,  0 < [|x|] ->
+	 wB/ 2 <= 2 ^ ([|head0 x|]) * [|x|] < wB.
+
+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 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 subcarryc_def_spec : forall x y, subcarryc x y = subcarryc_def x y.
+
+Axiom diveucl_def_spec : forall x y, diveucl x y = diveucl_def x y.
+
+Axiom diveucl_21_spec :  forall a1 a2 b,
+   let (q,r) := diveucl_21 a1 a2 b in
+   ([|q|],[|r|]) = Zdiv_eucl ([|a1|] * wB + [|a2|]) [|b|].
+
+Axiom addmuldiv_def_spec : forall p x y,
+  addmuldiv p x y = addmuldiv_def p x y.
diff --git a/src/versions/standard/Int63/Int63Native_standard.v b/src/versions/standard/Int63/Int63Native_standard.v
new file mode 100644
index 0000000..3a263d2
--- /dev/null
+++ b/src/versions/standard/Int63/Int63Native_standard.v
@@ -0,0 +1,106 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*       from the Int63 library of native-coq                             *)
+(*       by Benjamin Gregoire and Laurent Thery                           *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+Require Export DoubleType.
+
+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.
+
+Register int : Set as int63_type.
+
+Delimit Scope int63_scope with int63.
+Bind Scope int63_scope with int.
+
+(* Logical operations *)
+Register lsl  : int -> int -> int as int63_lsl.
+Infix "<<" := lsl (at level 30, no associativity) : int63_scope.
+
+Register lsr  : int -> int -> int as int63_lsr.
+Infix ">>" := lsr (at level 30, no associativity) : int63_scope.
+
+Register land : int -> int -> int as int63_land.
+Infix "land" := land (at level 40, left associativity) : int63_scope.
+
+Register lor  : int -> int -> int as int63_lor.
+Infix "lor" := lor (at level 40, left associativity) : int63_scope.
+
+Register lxor : int -> int -> int as int63_lxor.
+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.
+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.
+
+(* Comparisons *)
+Register eqb : int -> int -> bool as int63_eq.
+Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : int63_scope.
+
+Register ltb : int -> int -> bool as int63_lt.
+Notation "m < n" := (ltb m n) : int63_scope.
+
+Register leb : int -> int -> bool as int63_le.
+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.
+
+
+(* Iterators *)
+Register foldi_cont : 
+   forall 
+     {A B     : Type}
+     (f       : int -> (A -> B) -> A -> B) 
+     (from to : int)
+     (cont    : A -> B), 
+     A -> B
+     as int63_foldi.
+
+Register foldi_down_cont : 
+  forall 
+    {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.
+
+
+
diff --git a/src/versions/standard/Int63/Int63Op_standard.v b/src/versions/standard/Int63/Int63Op_standard.v
new file mode 100644
index 0000000..933a045
--- /dev/null
+++ b/src/versions/standard/Int63/Int63Op_standard.v
@@ -0,0 +1,272 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*       from the Int63 library of native-coq                             *)
+(*       by Benjamin Gregoire and Laurent Thery                           *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+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.
+
+(** 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 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 *)
+
+Definition bit i n :=  negb (is_zero ((i >> n) << (digits - 1))).
+(* Register bit as PrimInline. *)
+
+(** 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.
+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.
+
+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.
+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.
+
+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.
+
+Register diveucl_21    : int -> int -> int -> int * int as int63_div21.
+
+Definition addmuldiv_def p x y :=
+  (x << p) lor (y >> (digits - p)).
+Register addmuldiv   : int -> int -> int -> int as int63_addmuldiv.
+
+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 
+  else if (x == y) then Eq else Gt.
+
+Register compare : int -> int -> comparison as int63_compare.
+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.
+
+(** 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.
+
+Definition existsb (f:int -> bool) from to :=
+  foldi_cont (fun i cont _ => if f i then true else cont tt) from to (fun _ => false) tt.
+
+(** 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.
+
+Definition to_Z := to_Z_rec size.
+
+Fixpoint of_pos_rec (n:nat) (p:positive) :=
+  match n, p with 
+  | O, _ => 0
+  | S n, xH => 1
+  | S n, xO p => (of_pos_rec n p) << 1
+  | S n, xI p => (of_pos_rec n p) << 1 lor 1
+  end.
+
+Definition of_pos := of_pos_rec size.
+
+Definition of_Z z := 
+  match z with
+  | Zpos p => of_pos p
+  | Z0 => 0
+  | Zneg p => - (of_pos p)
+  end.
+
+(** Gcd **)
+Fixpoint gcd_rec (guard:nat) (i j:int) {struct guard} :=
+   match guard with
+   | O => 1
+   | S p => if j == 0 then i else gcd_rec p j (i \% j)
+   end.
+
+Definition gcd := gcd_rec (2*size).
+
+(** Square root functions using newton iteration **)
+
+Definition sqrt_step (rec: int -> int -> int) (i j: int)  :=
+  let quo := i/j in
+  if quo < j then rec i ((j + i/j) >> 1)
+  else j.
+
+Definition iter_sqrt :=
+ Eval lazy beta delta [sqrt_step] in
+ fix iter_sqrt (n: nat) (rec: int -> int -> int)
+          (i j: int) {struct n} : int :=
+  sqrt_step
+   (fun i j => match n with
+      O =>  rec i j
+   | S n => (iter_sqrt n (iter_sqrt n rec)) i j
+   end) i j.
+
+Definition sqrt i :=
+  match compare 1 i with
+    Gt => 0
+  | Eq => 1
+  | Lt => iter_sqrt size (fun i j => j) i (i >> 1)
+  end.
+
+Definition high_bit := 1 << (digits - 1).
+
+Definition sqrt2_step (rec: int -> int -> int -> int)
+   (ih il j: int)  :=
+  if ih < j then
+    let (quo,_) := diveucl_21 ih il j in
+    if quo < j then
+      match j +c quo with
+      | C0 m1 => rec ih il (m1 >> 1)
+      | C1 m1 => rec ih il ((m1 >> 1) + high_bit)
+      end 
+    else j
+  else j.
+
+Definition iter2_sqrt :=
+ Eval lazy beta delta [sqrt2_step] in
+ fix iter2_sqrt (n: nat)
+          (rec: int  -> int -> int -> int)
+          (ih il j: int) {struct n} : int :=
+  sqrt2_step
+   (fun ih il j => 
+     match n with
+     | O =>  rec ih il j
+     | S n => (iter2_sqrt n (iter2_sqrt n rec)) ih il j
+   end) ih il j.
+
+Definition sqrt2 ih il :=
+  let s := iter2_sqrt size (fun ih il j => j) ih il max_int in
+  let (ih1, il1) := mulc s s in
+  match il -c il1 with
+  | C0 il2 =>
+    if ih1 < ih then (s, C1 il2) else (s, C0 il2)
+  | C1 il2 =>
+    if ih1 < (ih - 1) then (s, C1 il2) else (s, C0 il2)
+  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 =>
+             Some
+             (fun (P : int -> Type) (Hi : P i) =>
+               match Heq (eq_refl true) in (_ = y) return (P y) with
+               | eq_refl => Hi
+               end)
+      else fun _ : false = true -> i = j => None) (eqb_correct i j).
+
+Definition eqo i j :=
+   (if i == j as b return ((b = true -> i = j) -> option (i=j))
+    then fun Heq : true = true -> i = j =>
+             Some (Heq (eq_refl true))
+     else fun _ : false = true -> i = j => None) (eqb_correct i j).
diff --git a/src/versions/standard/Int63/Int63Properties_standard.v b/src/versions/standard/Int63/Int63Properties_standard.v
new file mode 100644
index 0000000..37fc128
--- /dev/null
+++ b/src/versions/standard/Int63/Int63Properties_standard.v
@@ -0,0 +1,2596 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*       from the Int63 library of native-coq                             *)
+(*       by Benjamin Gregoire and Laurent Thery                           *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+Require Import Zgcd_alt.
+Require Import Bvector.
+Require Export Int63Axioms.
+Require Import Eqdep_dec.
+
+Local Open Scope int63_scope.
+Local Open Scope Z_scope.
+(** Trivial lemmas without axiom *)
+
+Lemma wB_diff_0 : wB <> 0.
+Proof. compute;discriminate. Qed.
+
+Lemma wB_pos : 0 < wB.
+Proof. reflexivity. Qed.
+
+Lemma to_Z_0 : [|0|] = 0.
+Proof. reflexivity. Qed.
+
+Lemma to_Z_1 : [|1|] = 1.
+Proof. reflexivity. Qed.
+
+(** equality *)
+Lemma eqb_complete : forall x y, x = y -> (x == y) = true.
+Proof.
+ intros x y H;rewrite H, eqb_refl;trivial.
+Qed.
+
+Lemma eqb_spec : forall x y, (x == y) = true <-> x = y.
+Proof.
+ split;auto using eqb_correct, eqb_complete.
+Qed.
+
+Lemma eqb_false_spec : forall x y, (x == y) = false <-> x <> y.
+Proof.
+ intros;rewrite <- not_true_iff_false, eqb_spec;split;trivial.
+Qed.
+
+Lemma eqb_false_complete : forall x y, x <> y -> (x == y) = false.
+Proof.
+ 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 } := 
+  (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)))
+  (eqb_correct i j)
+  (eqb_false_correct i j).
+
+Lemma eq_dec : forall i j:int, i = j \/ i <> j.
+Proof.
+ intros i j;destruct (eqs i j);auto.
+Qed.
+
+Lemma cast_refl : forall i, cast i i = Some (fun P H => H).
+Proof.
+ unfold cast;intros.
+ generalize (eqb_correct i i).
+ rewrite eqb_refl;intros.
+ rewrite (eq_proofs_unicity eq_dec (e (eq_refl true)) (eq_refl i));trivial.
+Qed.
+
+Lemma cast_diff : forall i j, i == j = false -> cast i j = None.
+Proof.
+ intros;unfold cast;intros; generalize (eqb_correct i j).
+ rewrite H;trivial.
+Qed.
+
+Lemma eqo_refl : forall i, eqo i i = Some (eq_refl i).
+Proof.
+ unfold eqo;intros.
+ generalize (eqb_correct i i).
+ rewrite eqb_refl;intros.
+ rewrite (eq_proofs_unicity eq_dec (e (eq_refl true)) (eq_refl i));trivial.
+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. 
+Qed.
+
+(** translation with Z *)
+Require Import Ndigits.
+
+Lemma Z_of_N_double : forall n, Z_of_N (Ndouble n) = Zdouble (Z_of_N n).
+Proof.
+ destruct n;simpl;trivial.
+Qed.
+
+Lemma Z_of_N_double_plus_one : forall n, Z_of_N (Ndouble_plus_one n) = Zdouble_plus_one (Z_of_N n).
+Proof.
+ destruct n;simpl;trivial.
+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.
+
+(* 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 to_Z_eq : forall x y, [|x|] = [|y|] <-> x = y.
+Proof.
+ split;intros;subst;trivial.
+ apply to_Z_inj;trivial.
+Qed.
+
+Lemma leb_ltb_eqb : forall x y, ((x <= y) = (x < y) || (x == y))%int63.
+Proof.
+ intros.
+ apply eq_true_iff_eq.
+ rewrite leb_spec, orb_true_iff, ltb_spec, eqb_spec, <- to_Z_eq;omega.
+Qed.
+
+
+(** Comparison *)
+
+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.
+ 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.
+ 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.
+Proof.
+ unfold is_zero;intros;apply eqb_spec.
+Qed.
+
+
+(** Addition *)
+
+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).
+ rewrite ltb_spec;intros.
+ change (wB + [|x+y|] = [|x|] + [|y|]).
+ rewrite add_spec in H |- *.
+ assert ([|x|] + [|y|] >= wB).
+  destruct (Z_lt_ge_dec ([|x|] + [|y|]) wB);auto with zarith.
+  elimtype False;rewrite Zmod_small in H;auto with zarith.
+ assert (([|x|] + [|y|]) mod wB = [|x|] + [|y|] - wB).
+  symmetry;apply Zmod_unique with 1;auto with zarith.
+ rewrite H1;ring.
+ rewrite <- not_true_iff_false, ltb_spec;intros.
+ change ([|x+y|] = [|x|] + [|y|]).
+ rewrite add_spec in *.
+ assert ([|x|] + [|y|] < wB).
+  destruct (Z_lt_ge_dec ([|x|] + [|y|]) wB);auto with zarith.
+  assert (([|x|] + [|y|]) mod wB = [|x|] + [|y|] - wB).
+  symmetry;apply Zmod_unique with 1;auto with zarith.
+  elim H;omega.
+ rewrite Zmod_small;auto with zarith.
+Qed.
+
+Lemma succc_spec : forall x, [+|succc x|] = [|x|] + 1.
+Proof. intros; apply addc_spec. Qed.
+
+Lemma addcarry_spec : forall x y, [|addcarry x y|] = ([|x|] + [|y|] + 1) mod wB.
+Proof.
+ unfold addcarry;intros.
+ rewrite add_spec,add_spec,Zplus_mod_idemp_l;trivial.
+Qed.
+
+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).
+ rewrite leb_spec;intros.
+ change (wB + [|(addcarry x y)|] = [|x|] + [|y|] + 1).
+ rewrite addcarry_spec in H |- *.
+ assert ([|x|] + [|y|] + 1 >= wB).
+  destruct (Z_lt_ge_dec ([|x|] + [|y|] + 1) wB);auto with zarith.
+  elimtype False;rewrite Zmod_small in H;auto with zarith.
+ assert (([|x|] + [|y|] + 1) mod wB = [|x|] + [|y|] + 1 - wB).
+  symmetry;apply Zmod_unique with 1;auto with zarith.
+ rewrite H1;ring.
+ rewrite <- not_true_iff_false, leb_spec;intros.
+ change ([|addcarry x y|] = [|x|] + [|y|] + 1).
+ rewrite addcarry_spec in *.
+ assert ([|x|] + [|y|] + 1 < wB).
+  destruct (Z_lt_ge_dec ([|x|] + [|y|] + 1) wB);auto with zarith.
+  assert (([|x|] + [|y|] + 1) mod wB = [|x|] + [|y|] + 1 - wB).
+  symmetry;apply Zmod_unique with 1;auto with zarith.
+  elim H;omega.
+ rewrite Zmod_small;auto with zarith.
+Qed.
+
+Lemma succ_spec : forall x, [|succ x|] = ([|x|] + 1) mod wB.
+Proof. intros; apply add_spec. Qed.
+
+(** Subtraction *)
+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.
+ rewrite leb_spec;intros.
+ change ([|x - y|] = [|x|] - [|y|]).
+ rewrite sub_spec.
+ rewrite Zmod_small;auto with zarith.
+ rewrite <- not_true_iff_false, leb_spec;intros.
+ change (-wB + [|x - y|] = [|x|] - [|y|]).
+ rewrite sub_spec.
+ assert (([|x|] - [|y|]) mod wB = [|x|] - [|y|] + wB).
+  symmetry;apply Zmod_unique with (-1);auto with zarith.
+ rewrite H0;ring.
+Qed.
+
+Lemma subcarry_spec :
+   forall x y, [|subcarry x y|] = ([|x|] - [|y|] - 1) mod wB.
+Proof. 
+ unfold subcarry; intros.
+ rewrite sub_spec,sub_spec,Zminus_mod_idemp_l;trivial.
+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.
+ rewrite ltb_spec;intros.
+ change ([|subcarry x y|] = [|x|] - [|y|] - 1).
+ rewrite subcarry_spec.
+ rewrite Zmod_small;auto with zarith.
+ rewrite <- not_true_iff_false, ltb_spec;intros.
+ change (-wB + [|subcarry x y|] = [|x|] - [|y|] - 1).
+ rewrite subcarry_spec.
+ assert (([|x|] - [|y|] - 1) mod wB = [|x|] - [|y|] - 1 + wB).
+  symmetry;apply Zmod_unique with (-1);auto with zarith.
+ rewrite H0;ring.
+Qed.
+
+Lemma oppc_spec : forall x : int, [-|oppc x|] = - [|x|].
+Proof.
+ unfold oppc;intros;rewrite subc_spec, to_Z_0;trivial.
+Qed.
+
+Lemma opp_spec : forall x : int, [|- x|] = - [|x|] mod wB.
+Proof.
+ unfold opp;intros;rewrite sub_spec, to_Z_0;trivial.
+Qed.
+
+Lemma oppcarry_spec : forall x, [|oppcarry x|] = wB - [|x|] - 1.
+Proof.
+ unfold oppcarry;intros.
+ rewrite sub_spec.
+ change [|max_int|] with (wB - 1).
+ rewrite <- Zminus_plus_distr, Zplus_comm, Zminus_plus_distr.
+ apply Zmod_small.
+ generalize (to_Z_bounded x);auto with zarith.
+Qed.
+
+Lemma predc_spec : forall x, [-|predc x|] = [|x|] - 1.
+Proof. intros; apply subc_spec. Qed.
+
+Lemma pred_spec : forall x, [|pred x|] = ([|x|] - 1) mod wB.
+Proof. intros; apply sub_spec. Qed.
+
+Lemma diveucl_spec : 
+  forall x y, 
+    let (q,r) := diveucl x y in
+    ([|q|],[|r|]) = Zdiv_eucl [|x|] [|y|].
+Proof.
+ intros;rewrite diveucl_def_spec.
+ unfold diveucl_def;rewrite div_spec, mod_spec.
+ unfold Zdiv, Zmod;destruct (Zdiv_eucl [|x|] [|y|]);trivial.
+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 Zplus_0_l.
+ apply  Zmult_le_0_compat; 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 Zmult_0_r, Zplus_0_r, Zplus_0_l.
+ generalize (sqr_pos (Zsucc j / 2)) (quotient_by_2 (Zsucc j));
+   unfold Zsucc.
+ rewrite Zpower_2, Zmult_plus_distr_l; repeat rewrite Zmult_plus_distr_r.
+ auto with zarith.
+ intros k Hk _.
+ replace ((Zsucc j + Zsucc k) / 2) with ((j + k)/2 + 1).
+ generalize (Hrec Hj k Hk) (quotient_by_2 (j + k)).
+ unfold Zsucc; repeat rewrite Zpower_2;
+   repeat rewrite Zmult_plus_distr_l; repeat rewrite Zmult_plus_distr_r.
+ repeat rewrite Zmult_1_l; repeat rewrite Zmult_1_r.
+ auto with zarith.
+ rewrite Zplus_comm, <- Z_div_plus_full_l; auto with zarith.
+ apply f_equal2 with (f := Zdiv); 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 Zlt_le_trans with (2 := sqrt_main_trick _ _ (Zlt_le_weak _ _ 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 Zpower_2, Z_div_plus_full_l; auto with zarith.
+   generalize (sqr_pos ((i - 2)/ 2)) (Z_div_pos (i - 2) 2).
+   rewrite Zmult_plus_distr_l; repeat rewrite Zmult_plus_distr_r.
+   auto with zarith.
+ generalize (quotient_by_2 i).
+ rewrite Zpower_2 in H2 |- *;
+   repeat (rewrite Zmult_plus_distr_l ||
+           rewrite Zmult_plus_distr_r ||
+           rewrite Zmult_1_l || rewrite Zmult_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 Zpower_2.
+ apply Zle_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 (Zle_or_lt j ((j + (i/j))/2)); auto.
+ intros H1; contradict H; apply Zle_not_lt.
+ assert (2 * j <= j + (i/j)); auto with zarith.
+ apply Zle_trans with (2 * ((j + (i/j))/2)); auto with zarith.
+ 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 ->
+  (forall j1 : int,
+    0 < [|j1|] < [|j|] -> [|i|] < ([|j1|] + 1) ^ 2 ->
+    [|rec i j1|] ^ 2 <= [|i|] < ([|rec i j1|] + 1) ^ 2) ->
+  [|sqrt_step rec i j|] ^ 2 <= [|i|] < ([|sqrt_step rec i j|] + 1) ^ 2.
+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];
+  rewrite ltb_spec, div_spec;intros.
+ assert ([| j + i / j|] = [|j|] + [|i|]/[|j|]).
+   rewrite add_spec, Zmod_small;rewrite div_spec;auto with zarith.
+ apply Hrec;rewrite lsr_spec, H0, to_Z_1;change (2^1) with 2.
+ split; [ | apply sqrt_test_false;auto with zarith].
+ replace ([|j|] + [|i|]/[|j|]) with
+        (1 * 2 + (([|j|] - 2) + [|i|] / [|j|]));[ | 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.
+ case (Zle_lt_or_eq 1 [|j|]); auto with zarith; intros Hj1.
+ rewrite <- Hj1, Zdiv_1_r.
+ assert (0 <= ([|i|] - 1) /2)%Z;[ |apply Z_div_pos]; auto with zarith.
+ 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|] ->
+      [|i|] < ([|j1|] + 1) ^ 2 -> 2 * [|j1|] < wB ->
+       [|rec i j1|] ^ 2 <= [|i|] < ([|rec i j1|] + 1) ^ 2) ->
+  [|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; apply Hrec; auto with zarith.
+ rewrite Zpower_0_r; auto with zarith.
+ intros n Hrec rec i j Hi Hj Hij H31 HHrec.
+ 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.
+ intros j3 Hj3 Hpj3.
+ apply HHrec; auto.
+ rewrite inj_S, Zpower_Zsucc.
+ apply Zle_trans with (2 ^Z_of_nat n + [|j2|]); auto with zarith.
+ apply Zle_0_nat.
+Qed.
+
+Lemma sqrt_spec : forall x,
+       [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2.
+Proof.
+ intros i; unfold sqrt.
+ rewrite compare_spec. case Zcompare_spec; rewrite to_Z_1;
+   intros Hi; auto with zarith.
+ repeat rewrite Zpower_2; auto with zarith.
+ apply iter_sqrt_correct; auto with zarith;
+  rewrite lsr_spec, to_Z_1; change (2^1) 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.
+  apply sqrt_init; auto.
+  assert (W:= Z_mult_div_ge [|i|] 2);assert (W':= to_Z_bounded i);auto with zarith.
+  intros j2 H1 H2; contradict H2; apply Zlt_not_le.
+  fold wB;assert (W:=to_Z_bounded i).
+  apply Zle_lt_trans with ([|i|]); auto with zarith.
+  assert (0 <= [|i|]/2)%Z by (apply Z_div_pos; auto with zarith).
+  apply Zle_trans with (2 * ([|i|]/2)); auto with zarith.
+  apply Z_mult_div_ge; auto with zarith.
+ case (to_Z_bounded i); repeat rewrite Zpower_2; auto with zarith.
+Qed.
+
+Lemma sqrt2_step_def rec ih il j:
+   sqrt2_step rec ih il j =
+   if (ih < j)%int63 then
+    let quo := fst (diveucl_21 ih il j) in
+    if (quo < j)%int63 then
+     let m :=
+      match j +c quo with
+      | C0 m1 => m1 >> 1
+      | C1 m1 => (m1 >> 1 + 1 << (digits -1))%int63
+      end in
+     rec ih il m
+    else j
+   else j.
+Proof.
+ unfold sqrt2_step; case diveucl_21; intros;simpl.
+ case (j +c i);trivial.
+Qed.
+
+Lemma sqrt2_lower_bound ih il j:
+   [|| WW ih il||]  < ([|j|] + 1) ^ 2 -> [|ih|] <= [|j|].
+Proof.
+ intros H1.
+ case (to_Z_bounded j); intros Hbj _.
+ case (to_Z_bounded il); intros Hbil _.
+ case (to_Z_bounded ih); intros Hbih Hbih1.
+ assert (([|ih|] < [|j|] + 1)%Z); auto with zarith.
+ apply Zlt_square_simpl; auto with zarith.
+ simpl zn2z_to_Z in H1.
+ repeat rewrite <-Zpower_2; apply Zle_lt_trans with (2 := H1).
+ apply Zle_trans with ([|ih|] * wB)%Z;try rewrite Zpower_2; auto with zarith.
+Qed.
+
+Lemma div2_phi ih il j: 
+  [|fst (diveucl_21 ih il j)|] = [|| WW ih il||] /[|j|].
+Proof.
+ generalize (diveucl_21_spec ih il j).
+ case diveucl_21; intros q r Heq.
+ simpl zn2z_to_Z;unfold Zdiv;rewrite <- Heq;trivial.
+Qed.
+
+Lemma zn2z_to_Z_pos ih il : 0 <= [||WW ih il||].
+Proof.
+ simpl zn2z_to_Z;destruct (to_Z_bounded ih);destruct (to_Z_bounded il);auto with zarith.
+Qed.
+
+
+Lemma sqrt2_step_correct rec ih il j:
+  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) ->
+  [|sqrt2_step rec ih il j|] ^ 2 <= [||WW ih il ||]
+      < ([|sqrt2_step rec ih il j|] + 1) ^  2.
+Proof.
+ assert (Hp2: (0 < [|2|])%Z) by exact (refl_equal Lt).
+ intros Hih Hj Hij Hrec; rewrite sqrt2_step_def.
+ assert (H1: ([|ih|] <= [|j|])%Z) by (apply sqrt2_lower_bound with il; auto).
+ case (to_Z_bounded ih); intros Hih1 _.
+ case (to_Z_bounded il); intros Hil1 _.
+ case (to_Z_bounded j); intros _ Hj1.
+ assert (Hp3: (0 < [||WW ih il||])).
+  simpl zn2z_to_Z;apply Zlt_le_trans with ([|ih|] * wB)%Z; auto with zarith.
+  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.
+ rewrite ltb_spec in Heq.
+ 2: rewrite <-not_true_iff_false, ltb_spec in Heq.
+ 2: split; auto.
+ 2: apply sqrt_test_true; auto with zarith.
+ 2: unfold zn2z_to_Z; replace [|ih|] with [|j|]; auto with zarith.
+ 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.
+ 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. 
+ 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.
+  intros i H;rewrite lsr_spec, H;trivial.
+  intros i H;rewrite <- H.
+  case (to_Z_bounded i); intros H1i H2i.
+  rewrite add_spec, Zmod_small, lsr_spec.
+  change (1 * wB) with ([|(1 << (digits -1))|] * 2)%Z.
+  rewrite Z_div_plus_full_l; auto with zarith.
+  change wB with (2 * (wB/2))%Z; auto.
+  replace [|(1 << (digits - 1))|] with (wB/2); auto.
+  rewrite lsr_spec; auto.
+  replace (2^[|1|]) with 2%Z; auto.
+  split; auto with zarith.
+  assert ([|i|]/2 < wB/2); auto with zarith.
+  apply Zdiv_lt_upper_bound; auto with zarith.
+ 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.
+ split.
+ replace ([|j|] + [||WW ih il||]/ [|j|])%Z with
+        (1 * 2 + (([|j|] - 2) + [||WW ih il||] / [|j|])); try ring.
+ rewrite Z_div_plus_full_l; auto with zarith.
+ assert (0 <= ([|j|] - 2 + [||WW ih il||] / [|j|]) / 2) ; auto with zarith.
+ apply sqrt_test_false; auto with zarith.
+ apply sqrt_main; auto with zarith.
+ contradict Hij; apply Zle_not_lt.
+ assert ((1 + [|j|]) <= 2 ^ (Z_of_nat size - 1)); auto with zarith.
+ apply Zle_trans with ((2 ^ (Z_of_nat size - 1)) ^2); auto with zarith.
+ assert (0 <= 1 + [|j|]); auto with zarith.
+ apply Zmult_le_compat; auto with zarith.
+ change ((2 ^ (Z_of_nat size - 1))^2) with (2 ^ (Z_of_nat size - 2) * wB).
+ apply Zle_trans with ([|ih|] * wB); auto with zarith.
+ unfold zn2z_to_Z, wB; auto with zarith.
+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|] ->
+      [||WW ih il||] < ([|j1|] + 1) ^ 2 ->
+       [|rec ih il j1|] ^ 2 <= [||WW ih il||] < ([|rec ih il j1|] + 1) ^ 2)  ->
+  [|iter2_sqrt n rec ih il j|] ^ 2 <= [||WW ih il||]
+      < ([|iter2_sqrt n rec ih il j|] + 1) ^ 2.
+Proof.
+ revert rec ih il j; elim n; unfold iter2_sqrt; fold iter2_sqrt; clear n.
+ intros rec ih il j Hi Hj Hij Hrec; apply sqrt2_step_correct; auto with zarith.
+ intros; apply Hrec; auto with zarith.
+ rewrite Zpower_0_r; auto with zarith.
+ intros n Hrec rec ih il j Hi Hj Hij HHrec.
+ apply sqrt2_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 inj_S, Zpower_Zsucc.
+ apply Zle_trans with (2 ^Z_of_nat n + [|j2|])%Z; auto with zarith.
+ apply Zle_0_nat.
+Qed.
+
+Lemma sqrt2_spec : forall x y,
+       wB/ 4 <= [|x|] ->
+       let (s,r) := sqrt2 x y in
+          [||WW x y||] = [|s|] ^ 2 + [+|r|] /\
+          [+|r|] <= 2 * [|s|].
+ Proof.
+ intros ih il Hih; unfold sqrt2.
+ change [||WW ih il||] with ([||WW ih il||]).
+ assert (Hbin: forall s, s * s + 2* s + 1 = (s + 1) ^ 2) by
+  (intros s; ring).
+ assert (Hb: 0 <= wB) by (red; intros HH; discriminate).
+ assert (Hi2: [||WW ih il ||] < ([|max_int|] + 1) ^ 2).
+  apply Zle_lt_trans with ((wB - 1) * wB + (wB - 1)); auto with zarith.
+  2: apply refl_equal.
+  case (to_Z_bounded ih); case (to_Z_bounded il); intros H1 H2 H3 H4.
+  unfold zn2z_to_Z; auto with zarith.
+ case (iter2_sqrt_correct size (fun _ _ j => j) ih il max_int); auto with zarith.
+ apply refl_equal.
+ intros j1 _ HH; contradict HH.
+ apply Zlt_not_le.
+ case (to_Z_bounded j1); auto with zarith.
+ change (2 ^ Z_of_nat size) with ([|max_int|]+1)%Z; auto with zarith.
+ set (s := iter2_sqrt size (fun _ _ j : int=> j) ih il max_int).
+ intros Hs1 Hs2.
+ generalize (mulc_spec s s); case mulc.
+ simpl fst; simpl snd; intros ih1 il1 Hihl1.
+ 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];
+  rewrite ltb_spec; intros Heq.
+ unfold interp_carry; rewrite Zmult_1_l.
+ rewrite Zpower_2, Hihl1, Hil2.
+ case (Zle_lt_or_eq ([|ih1|] + 1) ([|ih|])); auto with zarith.
+ intros H2; contradict Hs2; apply Zle_not_lt.
+ replace (([|s|] + 1) ^ 2) with ([||WW ih1 il1||] + 2 * [|s|] + 1).
+ unfold zn2z_to_Z.
+ case (to_Z_bounded il); intros Hpil _.
+ assert (Hl1l: [|il1|] <= [|il|]).
+  case (to_Z_bounded il2); rewrite Hil2; auto with zarith.
+ assert ([|ih1|] * wB + 2 * [|s|] + 1 <= [|ih|] * wB); auto with zarith.
+ case (to_Z_bounded s); intros _ Hps.
+ case (to_Z_bounded ih1); intros Hpih1 _; auto with zarith.
+ apply Zle_trans with (([|ih1|] + 2) * wB); auto with zarith.
+ rewrite Zmult_plus_distr_l.
+ assert (2 * [|s|] + 1 <= 2 * wB); auto with zarith.
+ unfold zn2z_to_Z; rewrite <-Hihl1, Hbin; auto.
+ 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 Hihl1; unfold zn2z_to_Z; rewrite <- H2; ring.
+ unfold interp_carry.
+ case (Zle_lt_or_eq [|ih|] [|ih1|]); auto with zarith; intros H.
+ contradict Hs1.
+ apply Zlt_not_le; rewrite Zpower_2, Hihl1.
+ unfold zn2z_to_Z.
+ case (to_Z_bounded il); intros _ H2.
+ apply Zlt_le_trans with (([|ih|] + 1) * wB + 0).
+ rewrite Zmult_plus_distr_l, Zplus_0_r; auto with zarith.
+ case (to_Z_bounded il1); intros H3 _.
+ apply Zplus_le_compat; auto with zarith.
+ split.
+ rewrite Zpower_2, Hihl1.
+ 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.
+ unfold zn2z_to_Z; rewrite H, Hil2; ring.
+ unfold interp_carry in Hil2 |- *.
+ assert (Hsih: [|ih - 1|] = [|ih|] - 1).
+  rewrite sub_spec, Zmod_small; auto; replace [|1|] with 1; auto.
+  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];
+  rewrite ltb_spec, Hsih; intros Heq.
+ rewrite Zpower_2, Hihl1.
+ case (Zle_lt_or_eq ([|ih1|] + 2) [|ih|]); auto with zarith.
+ intros H2; contradict Hs2; apply Zle_not_lt.
+ replace (([|s|] + 1) ^ 2) with ([||WW ih1 il1||] + 2 * [|s|] + 1).
+ unfold zn2z_to_Z.
+ assert ([|ih1|] * wB + 2 * [|s|] + 1 <= [|ih|] * wB + ([|il|] - [|il1|]));
+  auto with zarith.
+ rewrite <-Hil2.
+ case (to_Z_bounded il2); intros Hpil2 _.
+ apply Zle_trans with ([|ih|] * wB + - wB); auto with zarith.
+ case (to_Z_bounded s);  intros _ Hps.
+ assert (2 * [|s|] + 1 <= 2 * wB); auto with zarith.
+ apply Zle_trans with ([|ih1|] * wB + 2 * wB); auto with zarith.
+ assert (Hi: ([|ih1|] + 3) * wB <= [|ih|] * wB); auto with zarith.
+ rewrite Zmult_plus_distr_l in Hi; auto with zarith.
+ unfold zn2z_to_Z; rewrite <-Hihl1, Hbin; auto.
+ intros H2; unfold zn2z_to_Z; rewrite <-H2.
+ split.
+ replace [|il|] with (([|il|] - [|il1|]) + [|il1|]); try ring.
+ 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.
+ unfold zn2z_to_Z; rewrite <-H2.
+ replace [|il|] with (([|il|] - [|il1|]) + [|il1|]); try ring.
+ rewrite <-Hil2; ring.
+ case (Zle_lt_or_eq ([|ih|] - 1) ([|ih1|])); auto with zarith; intros H1.
+ assert (He: [|ih|] = [|ih1|]).
+   apply Zle_antisym; auto with zarith.
+   case (Zle_or_lt [|ih1|] [|ih|]); auto; intros H2.
+   contradict Hs1; apply Zlt_not_le; rewrite Zpower_2, Hihl1.
+  unfold zn2z_to_Z.
+  case (to_Z_bounded il); intros _ Hpil1.
+  apply Zlt_le_trans with (([|ih|] + 1) * wB).
+  rewrite Zmult_plus_distr_l, Zmult_1_l; auto with zarith.
+  case (to_Z_bounded il1); intros Hpil2 _.
+  apply Zle_trans with (([|ih1|]) * wB); auto with zarith.
+ contradict Hs1; apply Zlt_not_le; rewrite Zpower_2, Hihl1.
+ unfold zn2z_to_Z; rewrite He.
+ assert ([|il|] - [|il1|] < 0); auto with zarith.
+ rewrite <-Hil2.
+ case (to_Z_bounded il2); auto with zarith.
+ split.
+ rewrite Zpower_2, Hihl1.
+ unfold zn2z_to_Z; rewrite <-H1.
+ apply trans_equal with ([|ih|] * wB + [|il1|] + ([|il|] - [|il1|])).
+ ring.
+ 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.
+ unfold zn2z_to_Z.
+ rewrite <-H1.
+ ring_simplify.
+ apply trans_equal with (wB + ([|il|] - [|il1|])).
+ ring.
+ rewrite <-Hil2; ring.
+Qed.
+
+Lemma to_Z_gcd : forall i j,
+  [|gcd i j|] = Zgcdn (2*size) [|j|] [|i|].
+Proof.
+ unfold gcd.
+ induction (2*size)%nat; intros.
+ reflexivity.
+ simpl.
+ generalize (to_Z_bounded j)(to_Z_bounded i); intros.
+ case_eq (j == 0)%int63.
+ 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.
+ case_eq [|j|]; intros.
+ elim H1;apply to_Z_inj;assumption.
+ rewrite IHn, <- H2, mod_spec;trivial.
+ rewrite H2 in H;destruct H as (H, _);elim H;trivial.
+Qed.
+
+Lemma gcd_spec : forall a b, Zis_gcd [|a|] [|b|] [|gcd a b|].
+Proof.
+ intros.
+ rewrite to_Z_gcd.
+ apply Zis_gcd_sym.
+ apply Zgcdn_is_gcd.
+ unfold Zgcd_bound.
+ generalize (to_Z_bounded b).
+ destruct [|b|].
+ unfold size; auto with zarith.
+ 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. 
+ change 0 with [|0|];intros x Heq.
+ apply to_Z_inj in Heq;rewrite Heq;trivial.
+Qed.
+
+Lemma tail00_spec:  forall x, [|x|] = 0 -> [|tail0 x|] = [|digits|].
+Proof.
+ change 0 with [|0|];intros x Heq.
+ apply to_Z_inj in Heq;rewrite Heq;trivial.
+Qed.
+
+(* lsr lsl *)
+Lemma lsl_0_l i: 0 << i = 0%int63.
+Proof.
+ apply to_Z_inj.
+ generalize (lsl_spec 0 i).
+ rewrite to_Z_0, Zmult_0_l, Zmod_0_l; auto.
+Qed.
+
+Lemma lsl_0_r i: i << 0 = i.
+Proof.
+ apply to_Z_inj.
+ rewrite lsl_spec, to_Z_0, Zmult_1_r.
+ apply Zmod_small; apply (to_Z_bounded i).
+Qed.
+
+Lemma lsl_M_r x i (H: (digits <= i = true)%int63) : x << i = 0%int63.
+Proof.
+ apply to_Z_inj.
+ rewrite lsl_spec, to_Z_0.
+ rewrite leb_spec in H.
+ unfold wB; change (Z_of_nat size) with [|digits|].
+ replace ([|i|]) with (([|i|] - [|digits|]) + [|digits|])%Z; try ring.
+ rewrite Zpower_exp, Zmult_assoc, Z_mod_mult; auto with arith.
+ apply Zle_ge; auto with zarith.
+ case (to_Z_bounded digits); auto with zarith.
+Qed.
+
+Lemma lsr_0_l i: 0 >> i = 0%int63.
+Proof.
+ apply to_Z_inj.
+ generalize (lsr_spec 0 i).
+ rewrite to_Z_0, Zdiv_0_l; auto.
+Qed.
+
+Lemma lsr_0_r i: i >> 0 = i.
+Proof.
+ apply to_Z_inj.
+ 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.
+Proof.
+ apply to_Z_inj.
+ rewrite lsr_spec, to_Z_0.
+ case (to_Z_bounded x); intros H1x H2x.
+ case (to_Z_bounded digits); intros H1d H2d.
+ rewrite leb_spec in H.
+ apply Zdiv_small; split; auto.
+ apply Zlt_le_trans with (1 := H2x).
+ unfold wB; change (Z_of_nat size) with [|digits|].
+ 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.
+Proof.
+ case (to_Z_bounded m); intros H1m H2m.
+ case (to_Z_bounded n); intros H1n H2n.
+ case (Zle_or_lt wB ([|m|] + [|n|])); intros H.
+   assert (H1: ([| m + n |] = [|m|] + [|n|] - wB)%Z).
+     rewrite add_spec.
+     replace (([|m|] + [|n|]) mod wB)%Z with (((([|m|] + [|n|]) - wB) + wB) mod wB)%Z.
+     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.
+   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.
+ 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.
+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.
+   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.
+ apply Zdiv_small; split; auto with zarith.
+ apply Zlt_le_trans with (1 := H2i).
+ apply Zle_trans with (1 := H).
+ 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.
+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.
+   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.
+   rewrite add_spec, Zmod_small; auto with zarith.
+ 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 
+         ((([|m|] + [|n|]) - Z_of_nat size) + Z_of_nat size)%Z.
+ 2: ring.
+ rewrite Zpower_exp, Zmult_assoc, Z_mod_mult; auto with zarith.
+ assert (Z_of_nat size < wB)%Z; auto with zarith.
+ apply Zpower2_lt_lin; auto with zarith.
+Qed.
+
+Coercion b2i (b: bool) : int := if b then 1%int63 else 0%int63.
+
+Lemma bit_0 n : bit 0 n = false.
+Proof. unfold bit; rewrite lsr_0_l; auto. Qed.
+
+Lemma lsr_1 n : 1 >> n = (n == 0).
+Proof.
+ case_eq (n == 0).
+ rewrite eqb_spec; intros H; rewrite H, lsr_0_r.
+ apply refl_equal.
+ intros Hn.
+ assert (H1n : (1 >> n = 0)%int63); 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.
+ apply Zpower_lt_monotone; split; auto with zarith.
+ case (Zle_lt_or_eq  0 [|n|]); auto.
+ case (to_Z_bounded n); auto.
+ intros H1.
+ assert ((n == 0) = true).
+ rewrite eqb_spec; apply to_Z_inj; rewrite <-H1, to_Z_0; auto.
+ generalize H; rewrite Hn; discriminate.
+Qed.
+
+Lemma bit_1 n : bit 1 n = (n == 0).
+Proof.
+ unfold bit; rewrite lsr_1.
+ case (n == 0).
+ apply refl_equal.
+ rewrite lsl_0_l; apply refl_equal.
+Qed.
+
+Lemma bit_M i n (H: (digits <= n = true)%int63): 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).
+Proof.
+ unfold bit.
+ rewrite lsr_add.
+ case_eq (n <= (1 + n))%int63.
+ replace (1+n)%int63 with (n+1)%int63; [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; 
+   intros H2; apply to_Z_inj; auto.
+ generalize (add_le_r 1 n); rewrite H1.
+ change [|max_int|] with (wB - 1)%Z.
+ replace [|1|] with 1%Z; auto with zarith.
+Qed.
+
+Lemma bit_0_spec i: [|bit i 0|] = [|i|] mod 2.
+Proof.
+ unfold bit, is_zero; rewrite lsr_0_r.
+ assert (Hbi: ([|i|] mod 2 < 2)%Z).
+   apply Z_mod_lt; auto with zarith.
+ case (to_Z_bounded i); intros H1i H2i.
+ case (Zmod_le_first [|i|] 2); auto with zarith; intros H3i H4i.
+ assert (H2b: (0 < 2 ^ [|digits - 1|])%Z).
+   apply Zpower_gt_0; auto with zarith.
+   case (to_Z_bounded (digits -1)); auto with zarith.
+ assert (H: [|i << (digits -1)|] = ([|i|] mod 2 * 2^ [|digits -1|])%Z).
+ rewrite lsl_spec.
+ rewrite (Z_div_mod_eq [|i|] 2) at 1; auto with zarith.
+ rewrite Zmult_plus_distr_l, <-Zplus_mod_idemp_l.
+ rewrite (Zmult_comm 2), <-Zmult_assoc.
+ replace (2 * 2 ^ [|digits - 1|])%Z with wB; auto.
+ rewrite Z_mod_mult, Zplus_0_l; apply Zmod_small.
+ split; auto with zarith.
+ replace wB with (2 * 2 ^ [|digits -1|])%Z; auto.
+ apply Zmult_lt_compat_r; auto with zarith.
+ case (Zle_lt_or_eq 0 ([|i|] mod 2)); auto with zarith; intros Hi.
+ 2: generalize H; rewrite <-Hi, Zmult_0_l.
+ 2: replace 0%Z with [|0|]; auto.
+ 2: rewrite to_Z_eq, <-eqb_spec; intros H1; rewrite H1; auto.
+ generalize H; replace ([|i|] mod 2) with 1%Z; auto with zarith.
+ rewrite Zmult_1_l.
+ intros H1.
+ assert (H2: [|i << (digits - 1)|] <> [|0|]).
+  replace [|0|] with 0%Z; auto with zarith.
+ generalize (eqb_spec (i << (digits - 1)) 0).
+ case (i << (digits - 1) == 0); auto.
+ intros (H3,_); case H2.
+ rewrite to_Z_eq; auto.
+Qed.
+
+Lemma bit_split i : (i = (i>>1)<<1 + bit i 0)%int63.
+Proof.
+ apply to_Z_inj.
+ rewrite add_spec, lsl_spec, lsr_spec, bit_0_spec, Zplus_mod_idemp_l.
+ replace (2 ^ [|1|]) with 2%Z; auto with zarith.
+ rewrite Zmult_comm, <-Z_div_mod_eq; auto with zarith.
+ 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.
+ split; try (intros; subst; auto; fail).
+ case (to_Z_bounded i2); case (to_Z_bounded i1).
+ unfold wB; generalize i1 i2; elim size; clear i1 i2.
+ replace (2^Z_of_nat 0) with 1%Z; auto with zarith.
+ intros; apply to_Z_inj; auto with zarith.
+ 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 := lsl); auto.
+ apply IH; try rewrite lsr_spec;
+   replace (2^[|1|]) with 2%Z;  auto with zarith.
+ apply Zdiv_lt_upper_bound; auto with zarith.
+ generalize H2i1; rewrite inj_S.
+ unfold Zsucc; rewrite Zpower_exp; auto with zarith.
+ apply Zdiv_lt_upper_bound; auto with zarith.
+ generalize H2i2; rewrite inj_S.
+ unfold Zsucc; rewrite Zpower_exp; auto with zarith.
+ intros i.
+ case (Zle_or_lt [|digits|] [|i|]); intros Hi.
+ rewrite !bit_M; auto; rewrite leb_spec; auto.
+ rewrite !bit_half; auto; rewrite ltb_spec; auto with zarith.
+Qed.
+
+Lemma bit_lsr x i j :
+ (bit (x >> i) j = if j <= i + j then bit x (i + j) else false)%int63.
+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.
+Proof.
+ assert (F1: 1 >= 0) by discriminate.
+ case_eq (digits <= j)%int63; 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.
+ 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.
+ apply sym_equal; rewrite is_zero_spec; apply to_Z_inj.
+ rewrite lsl_spec, lsr_spec, lsl_spec.
+ replace wB with (2^d); auto.
+ pattern d at 1; replace d with ((d - ([|j|] + 1)) + ([|j|] + 1))%Z.
+ 2: ring.
+ rewrite Zpower_exp; auto with zarith.
+ replace [|i|] with (([|i|] - ([|j|] + 1)) + ([|j|] + 1))%Z.
+ 2: ring.
+ rewrite Zpower_exp, Zmult_assoc; auto with zarith.
+ rewrite Zmult_mod_distr_r.
+ rewrite Zplus_comm, Zpower_exp, !Zmult_assoc; auto with zarith.
+ rewrite Z_div_mult_full; auto with zarith.
+ 2: assert (0 < 2 ^ [|j|])%Z; auto with zarith.
+ rewrite <-Zmult_assoc, <-Zpower_exp; auto with zarith.
+ replace (1 + [|digits - 1|])%Z with d; auto with zarith.
+ rewrite Z_mod_mult; auto.
+ case H2; intros _ H3; case (Zle_or_lt [|i|] [|j|]); intros F2.
+ 2: generalize (H3 F2); discriminate.
+ clear H2 H3.
+ apply f_equal with (f := negb).
+ apply f_equal with (f := is_zero).
+ apply to_Z_inj.
+ rewrite !lsl_spec, !lsr_spec, !lsl_spec.
+ pattern wB at 2 3; replace wB with (2^(1+ [|digits - 1|])); auto.
+ rewrite Zpower_exp, Zpower_1_r; auto with zarith.
+ rewrite !Zmult_mod_distr_r.
+ apply f_equal2 with (f := Zmult); auto.
+ replace wB with (2^ d); auto with zarith.
+ replace d with ((d - [|i|]) + [|i|])%Z.
+ 2: ring.
+ case (to_Z_bounded i); intros  H1i H2i.
+ rewrite Zpower_exp; auto with zarith.
+ 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; 
+   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; 
+   replace d1 with (d2 + (1+ (d - [|j|] - 1)))%Z.
+ 2: unfold d1, d2; ring.
+ rewrite Zpower_exp; auto with zarith.
+ 2: unfold d2; auto with zarith.
+ rewrite <-Zmult_assoc, Zmult_comm.
+ rewrite Z_div_plus_l; auto with zarith.
+ 2: unfold d2; auto with zarith.
+ rewrite Zpower_exp, Zpower_1_r; auto with zarith.
+ rewrite <-Zplus_mod_idemp_l.
+ 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.
+ 2: rewrite lsr_0_l, lsl_0_l, andb_false_r; auto.
+ rewrite lsr_1; case (i == 0); auto.
+Qed.
+
+Lemma bit_or_split i : (i = (i>>1)<<1 lor bit i 0)%int63.
+Proof.
+ rewrite bit_eq.
+ intros n; rewrite lor_spec.
+ rewrite bit_lsl, bit_lsr, bit_b2i.
+ case (to_Z_bounded n); intros Hi _.
+ 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.
+ 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.
+ rewrite ltb_spec, to_Z_1; intros HH; contradict HH; auto with zarith.
+ intros _.
+ generalize (@bit_M i n); case leb.
+ intros H1; rewrite H1; auto.
+ intros _.
+ case (to_Z_bounded n); intros H1n H2n.
+ 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.
+ apply to_Z_inj; rewrite add_spec, F1, Zmod_small; rewrite to_Z_1;
+  auto with zarith.
+ rewrite bit_M; auto; rewrite leb_spec.
+ replace [|n|] with wB; try discriminate; auto with zarith.
+Qed.
+
+(* is_zero *)
+Lemma is_zero_0: is_zero 0 = true.
+Proof. apply refl_equal. Qed.
+
+(* is_even *)
+Lemma is_even_bit i : is_even i = negb (bit i 0).
+Proof.
+ unfold is_even.
+ replace (i land 1) with (b2i (bit i 0)).
+ case bit; auto.
+ apply bit_eq; intros n.
+ rewrite bit_b2i, land_spec, bit_1.
+ generalize (eqb_spec n 0).
+ case (n == 0); auto.
+ intros(H,_); rewrite andb_true_r, H; auto.
+ rewrite andb_false_r; auto.
+Qed.
+
+Lemma is_even_0: is_even 0 = true.
+Proof. apply refl_equal. Qed.
+
+Lemma is_even_lsl_1 i: is_even (i << 1) = true.
+Proof.
+ rewrite is_even_bit, bit_lsl; auto.
+Qed.
+
+Lemma is_even_spec : forall x,
+      if is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1.
+Proof.
+intros x; rewrite is_even_bit.
+generalize (bit_0_spec x); case bit; simpl; auto.
+Qed.
+
+(* More land *)
+
+Lemma land_0_l i: 0 land i = 0%int63.
+Proof.
+ apply bit_eq; intros n.
+ rewrite land_spec, bit_0; auto.
+Qed.
+
+Lemma land_0_r i: i land 0 = 0%int63.
+Proof.
+ apply bit_eq; intros n.
+ rewrite land_spec, bit_0, andb_false_r; auto.
+Qed.
+
+Lemma land_assoc i1 i2 i3 :
+  i1 land (i2 land i3) = i1 land i2 land i3.
+Proof.
+ apply bit_eq; intros n.
+ rewrite !land_spec, andb_assoc; auto.
+Qed.
+
+Lemma land_comm i j : i land j = j land i.
+Proof.
+ apply bit_eq; intros n.
+ rewrite !land_spec, andb_comm; auto.
+Qed.
+
+Lemma lor_comm i1 i2 : i1 lor i2 = i2 lor i1.
+Proof.
+ apply bit_eq; intros n.
+ rewrite !lor_spec, orb_comm; auto.
+Qed.
+
+Lemma lor_assoc i1 i2 i3 :
+  i1 lor (i2 lor i3) = i1 lor i2 lor i3.
+Proof.
+ apply bit_eq; intros n.
+ rewrite !lor_spec, orb_assoc; auto.
+Qed.
+
+Lemma land_lor_distrib_r i1 i2 i3 :
+ i1 land (i2 lor i3) = (i1 land i2) lor (i1 land i3).
+Proof.
+ apply bit_eq; intros n.
+ rewrite !land_spec, !lor_spec, !land_spec, andb_orb_distrib_r; auto.
+Qed.
+
+Lemma land_lor_distrib_l i1 i2 i3 :
+ (i1 lor i2) land i3 = (i1 land i3) lor (i2 land i3).
+Proof.
+ apply bit_eq; intros n.
+ rewrite !land_spec, !lor_spec, !land_spec, andb_orb_distrib_l; auto.
+Qed.
+
+Lemma lor_land_distrib_r i1 i2 i3:
+  i1 lor (i2 land i3) = (i1 lor i2) land (i1 lor i3).
+Proof.
+ apply bit_eq; intros n.
+ rewrite !land_spec, !lor_spec, !land_spec, orb_andb_distrib_r; auto.
+Qed.
+
+Lemma lor_land_distrib_l i1 i2 i3:
+  (i1 land i2) lor i3 = (i1 lor i3) land (i2 lor i3).
+Proof.
+ apply bit_eq; intros n.
+ rewrite !land_spec, !lor_spec, !land_spec, orb_andb_distrib_l; auto.
+Qed.
+
+Lemma absoption_land i1 i2 : i1 land (i1 lor i2) = i1.
+Proof.
+ apply bit_eq; intros n.
+ rewrite land_spec, lor_spec, absoption_andb; auto.
+Qed.
+
+Lemma absoption_lor i1 i2: i1 lor (i1 land i2) = i1.
+Proof.
+ apply bit_eq; intros n.
+ rewrite lor_spec, land_spec, absoption_orb; auto.
+Qed.
+
+Lemma land_lsl i1 i2 i: (i1 land i2) << i = (i1 << i) land (i2 << i).
+Proof.
+ apply bit_eq; intros n.
+ rewrite land_spec, !bit_lsl, land_spec.
+ case (_ || _); auto.
+Qed.
+
+Lemma lor_lsl i1 i2 i: (i1 lor i2) << i = (i1 << i) lor (i2 << i).
+Proof.
+ apply bit_eq; intros n.
+ rewrite lor_spec, !bit_lsl, lor_spec.
+ case (_ || _); auto.
+Qed.
+
+Lemma lxor_lsl i1 i2 i: (i1 lxor i2) << i = (i1 << i) lxor (i2 << i).
+Proof.
+ apply bit_eq; intros n.
+ rewrite lxor_spec, !bit_lsl, lxor_spec.
+ case (_ || _); auto.
+Qed.
+
+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.
+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.
+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.
+Qed.
+
+Lemma is_even_and i j : is_even (i land j) = is_even i || is_even j.
+Proof.
+ rewrite !is_even_bit, land_spec; case bit; auto.
+Qed.
+
+Lemma is_even_or i j : is_even (i lor j) = is_even i && is_even j.
+Proof.
+ rewrite !is_even_bit, lor_spec; case bit; auto.
+Qed.
+
+Lemma is_even_xor i j : is_even (i lxor j) = negb (xorb (is_even i) (is_even j)).
+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.
+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.
+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.
+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.
+Proof.
+ apply to_Z_inj.
+ rewrite add_spec, !lsl_spec, add_spec.
+ rewrite Zmult_mod_idemp_l, <-Zplus_mod.
+ apply f_equal2 with (f := Zmod); auto with zarith.
+Qed.
+
+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).
+  assert (F1: (2 | wB)) by (apply Zpower_divide; apply refl_equal).
+  assert (F2: 0 < wB) by (apply refl_equal).
+  case (to_Z_bounded x); intros H1x H2x.
+  case (to_Z_bounded y); intros H1y H2y.
+  rewrite add_spec, <-Zmod_div_mod; auto with zarith.
+  rewrite (Z_div_mod_eq [|x|] 2) at 1; auto with zarith.
+  rewrite (Z_div_mod_eq [|y|] 2) at 1; auto with zarith.
+  rewrite Zplus_mod.
+  rewrite Zmult_comm, (fun x => Zplus_comm (x * 2)), Z_mod_plus; auto with zarith.
+  rewrite Zmult_comm, (fun x => Zplus_comm (x * 2)), Z_mod_plus; auto with zarith.
+  rewrite !Zmod_mod, <-Zplus_mod; auto.
+ generalize (is_even_spec (x + y)) (is_even_spec x) (is_even_spec y).
+ do 3 case is_even; auto; rewrite F; intros H1 H2 H3;
+  generalize H1; rewrite H2, H3; try discriminate.
+Qed.
+
+Lemma bit_add_0 x y: bit (x + y) 0 = xorb (bit x 0) (bit y 0).
+Proof.
+ rewrite <-(fun x => (negb_involutive (bit x 0))).
+ 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.
+Proof.
+ 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.
+ 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.
+ rewrite (Z_div_mod_eq ([|x|] + [|y|]) wB), (Z_div_mod_eq ([|x|] + [|z|]) wB); auto.
+ rewrite <-to_Z_eq, !add_spec in H; rewrite H.
+ replace (([|x|] + [|y|])/wB) with 1.
+ replace (([|x|] + [|z|])/wB) with 1; auto with zarith.
+ apply Zle_antisym.
+ apply Zdiv_le_lower_bound; auto with zarith.
+ assert (F2: [|x|] + [|z|] < 2 * wB); auto with zarith.
+ generalize (Zdiv_lt_upper_bound _ _ _ (Zgt_lt _ _ F1) F2); auto with zarith.
+ apply Zle_antisym.
+ apply Zdiv_le_lower_bound; auto with zarith.
+ assert (F2: [|x|] + [|y|] < 2 * wB); auto with zarith.
+ 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.
+Proof.
+  rewrite !(fun t => add_comm t x); intros Hl; apply (add_cancel_l x); auto.
+Qed.
+
+Lemma to_Z_split x : [|x|] = [|(x  >> 1)|] * 2 + [|bit x 0|].
+Proof.
+  case (to_Z_bounded x); intros H1x H2x.
+  case (to_Z_bounded (bit x 0)); intros H1b H2b.
+  assert (F1: 0 <= [|x >> 1|] < wB/2).
+    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; 
+    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.
+  change wB with ((wB/2)*2); auto with zarith.
+  rewrite lsl_spec, to_Z_1, Zpower_1_r, Zmod_small; auto with zarith.
+  2: change wB with ((wB/2)*2); auto with zarith.
+  change wB with (((wB/2 - 1) * 2 + 1) + 1).
+  assert ([|bit x 0|] <= 1); auto with zarith.
+  case bit; discriminate.
+Qed.
+
+Lemma lor_le x y : (y <= x lor y)%int63 = 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.
+ 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.
+ unfold Zsucc; rewrite Zpower_exp, Zpower_1_r; auto with zarith.
+ intros Hx Hy.
+ rewrite leb_spec.
+ rewrite (to_Z_split y) at 1; rewrite (to_Z_split (x lor y)).
+ assert ([|y>>1|] <= [|(x lor y) >> 1|]).
+  rewrite lor_lsr, <-leb_spec; apply IH.
+  rewrite lsr_spec, to_Z_1, Zpower_1_r; split; auto with zarith.
+  apply Zdiv_lt_upper_bound; auto with zarith.
+  rewrite lsr_spec, to_Z_1, Zpower_1_r; split; auto with zarith.
+  apply Zdiv_lt_upper_bound; auto with zarith.
+ assert ([|bit y 0|] <= [|bit (x lor y) 0|]); auto with zarith.
+ rewrite lor_spec; do 2 case bit; try discriminate.
+Qed.
+
+
+Lemma bit_add_or x y: 
+  (forall n, bit x n = true -> bit y n = true -> False) <-> (x + y)%int63= 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.
+ 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.
+ intros n IH x y; rewrite inj_S.
+ unfold Zsucc; rewrite Zpower_exp, Zpower_1_r; auto with zarith.
+ intros Hx Hy.
+ split.
+ intros Hn.
+ assert (F1: ((x >> 1) + (y >> 1))%int63 = (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];
+     intros Heq.
+   rewrite bit_M in H1; auto; discriminate.
+   rewrite leb_spec in Heq.
+   apply (Hn (m + 1)%int63);
+     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.
+ 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_comm; auto.
+ intros Heq.
+ generalize (add_le_r x y); rewrite Heq, lor_le; intro Hb.
+ generalize Heq; rewrite (bit_split x) at 1; rewrite (bit_split y )at 1; clear Heq.
+ rewrite (fun y => add_comm y (bit x 0)), <-!add_assoc, add_comm,
+         <-!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 (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).
+  apply trans_equal with (([|(x>>1 + y>>1) << 1|] + [|bit x 0 + bit y 0|]) mod 2).
+  rewrite lsl_spec, Zplus_mod, <-Zmod_div_mod; auto with zarith.
+  rewrite Zpower_1_r, Z_mod_mult, Zplus_0_l, Zmod_mod; auto with zarith.
+  rewrite (Zmod_div_mod 2 wB), <-add_spec, Heq; auto with zarith.
+  rewrite add_spec, <-Zmod_div_mod; auto with zarith.
+  rewrite lsl_spec, Zplus_mod, <-Zmod_div_mod; auto with zarith.
+  rewrite Zpower_1_r, Z_mod_mult, Zplus_0_l, Zmod_mod; auto with zarith.
+  generalize F3; do 2 case bit; try discriminate; auto.
+ case (IH (x >> 1) (y >> 1)).
+ rewrite lsr_spec, to_Z_1, Zpower_1_r; split; auto with zarith.
+ apply Zdiv_lt_upper_bound; auto with zarith.
+ 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.
+ 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.
+ rewrite <-(bit_half x), <-(bit_half y); auto with zarith.
+ apply HH.
+ rewrite <-lor_lsr.
+ assert (0 <= [|bit (x lor y) 0|] <= 1) by (case bit; split; discriminate).
+ rewrite F in Heq; generalize (add_cancel_r _ _ _ Heq).
+ intros Heq1; apply to_Z_inj.
+ generalize Heq1; rewrite <-to_Z_eq, lsl_spec, to_Z_1, Zpower_1_r, Zmod_small.
+ rewrite lsl_spec, to_Z_1, Zpower_1_r, Zmod_small; auto with zarith.
+ case (to_Z_bounded (x lor y)); intros H1xy H2xy.
+ rewrite lsr_spec, to_Z_1, Zpower_1_r; auto with zarith.
+ change wB with ((wB/2)*2); split; auto with zarith.
+ assert ([|x lor y|] / 2  < wB / 2); auto with zarith.
+ apply Zdiv_lt_upper_bound; auto with zarith.
+ split.
+ case (to_Z_bounded (x >> 1 + y >> 1)); auto with zarith.
+ rewrite add_spec.
+ apply Zle_lt_trans with (([|x >> 1|] + [|y >> 1|]) * 2); auto with zarith.
+ case (Zmod_le_first ([|x >> 1|] + [|y >> 1|]) wB); auto with zarith.
+ case (to_Z_bounded (x >> 1)); case (to_Z_bounded (y >> 1)); auto with zarith.
+ generalize Hb; rewrite (to_Z_split x) at 1; rewrite (to_Z_split y) at 1.
+ case (to_Z_bounded (bit x 0)); case (to_Z_bounded (bit y 0)); auto with zarith.
+ rewrite ltb_spec, sub_spec, to_Z_1, Zmod_small; auto with zarith.
+ 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.
+ intros Hbx Hby; generalize F; rewrite <-to_Z_eq, Hbx, Hby; discriminate.
+ apply to_Z_inj; auto.
+Qed.
+
+Lemma addmuldiv_spec : forall x y p, [|p|] <= [|digits|] ->
+   [| addmuldiv p x y |] =
+   ([|x|] * (2 ^ [|p|]) + [|y|] / (2 ^ ([|digits|] - [|p|]))) mod wB.
+Proof.
+ intros x y p H.
+ assert (Fp := to_Z_bounded p); assert (Fd := to_Z_bounded digits).
+ rewrite addmuldiv_def_spec; unfold addmuldiv_def.
+ case (bit_add_or (x << p) (y >> (digits - p))); intros HH _.
+ rewrite <-HH, add_spec, lsl_spec, lsr_spec, Zplus_mod_idemp_l, sub_spec.
+ rewrite (fun x y => Zmod_small (x - y)); auto with zarith.
+ intros n; rewrite bit_lsl, bit_lsr.
+ 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.
+ 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. 
+
+Lemma lxor_comm: forall i1 i2 : int, i1 lxor i2 = i2 lxor i1.
+Proof.
+ intros;apply bit_eq;intros.
+ rewrite !lxor_spec;apply xorb_comm.
+Qed.
+
+Lemma lxor_assoc: forall i1 i2 i3 : int, i1 lxor (i2 lxor i3) = i1 lxor i2 lxor i3.
+Proof.
+ intros;apply bit_eq;intros.
+ rewrite !lxor_spec, xorb_assoc;trivial.
+Qed.
+
+Lemma lxor_0_l : forall i, 0 lxor i = i.
+Proof.
+  intros;apply bit_eq;intros.
+  rewrite lxor_spec, bit_0, xorb_false_l;trivial.
+Qed.
+
+Lemma lxor_0_r : forall i, i lxor 0 = i.
+Proof.
+ intros;rewrite lxor_comm;apply lxor_0_l.
+Qed.
+
+Lemma lxor_nilpotent: forall i, i lxor i = 0%int63.
+Proof.
+ intros;apply bit_eq;intros.
+ rewrite lxor_spec, xorb_nilpotent, bit_0;trivial.
+Qed.
+
+Lemma lor_0_l : forall i, 0 lor i = i.
+Proof.
+  intros;apply bit_eq;intros.
+  rewrite lor_spec, bit_0, orb_false_l;trivial.
+Qed.
+
+Lemma lor_0_r : forall i, i lor 0 = i.
+Proof.
+ intros;rewrite lor_comm;apply lor_0_l.
+Qed.
+
+Lemma reflect_leb : forall i j, reflect ([|i|] <= [|j|])%Z (i <= j)%int63.
+Proof.
+ intros; apply iff_reflect.
+ symmetry;apply leb_spec.
+Qed.
+
+Lemma reflect_eqb : forall i j, reflect (i = j)%Z (i == j).
+Proof.
+ intros; apply iff_reflect.
+ symmetry;apply eqb_spec.
+Qed.
+
+Lemma reflect_ltb : forall i j, reflect ([|i|] < [|j|])%Z (i < j)%int63.
+Proof.
+ intros; apply iff_reflect.
+ symmetry;apply ltb_spec.
+Qed.
+
+Lemma lsr_is_even_eq : forall i j,
+  i >> 1 = j >> 1 ->
+  is_even i = is_even j ->
+  i = j.
+Proof.
+ intros;apply bit_eq.
+ intros n;destruct (reflect_eqb n 0).
+ rewrite <- (negb_involutive (bit i n)), <- (negb_involutive (bit j n)).
+ rewrite e, <- !is_even_bit, H0;trivial.
+ assert (W1 : [|n|] <> 0) by (intros Heq;apply n0;apply to_Z_inj;trivial).
+ 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).
+   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).
+  rewrite leb_spec;omega.
+ rewrite !bit_M;trivial.
+Qed.
+
+Lemma lsr1_bit : forall i k, (bit i k >> 1 = 0)%int63.
+Proof.
+ intros;destruct (bit i k);trivial.
+Qed.
+
+Lemma bit_xor_split: forall i : int, i = (i >> 1) << 1 lxor bit i 0.
+Proof.
+ intros.
+ rewrite bit_or_split at 1.
+ apply lsr_is_even_eq.
+ rewrite lxor_lsr, lor_lsr, lsr1_bit, lxor_0_r, lor_0_r;trivial.
+ rewrite is_even_or, is_even_xor.
+ rewrite is_even_lsl_1;trivial.
+ rewrite (xorb_true_l (is_even (bit i 0))), negb_involutive;trivial.
+Qed.
+
+(** Order *)
+Local Open Scope int63_scope.
+
+Lemma succ_max_int : forall x,
+  (x < max_int)%int63 = true -> (0 < x + 1)%int63 = 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).
+ change [|0|] with 0%Z;change [|1|] with 1%Z.
+ rewrite Zmod_small;omega.
+Qed.
+
+Lemma leb_max_int : forall x, (x <= max_int)%int63 = true.
+Proof.
+ intros x;rewrite leb_spec;assert (W:= to_Z_bounded x).
+ change [|max_int|] with (wB - 1)%Z;omega.
+Qed.
+
+Lemma leb_0 : forall x, 0 <= x = true.
+Proof.
+ intros x;rewrite leb_spec;destruct (to_Z_bounded x);trivial.
+Qed.
+
+Lemma ltb_0 : forall x, ~ (x < 0 = true).
+Proof.
+ intros x;rewrite ltb_spec, to_Z_0;destruct (to_Z_bounded x);omega.
+Qed.
+
+Lemma leb_trans : forall x y z, x <= y = true ->  y <= z = true -> x <= z = true.
+Proof.
+ intros x y z;rewrite !leb_spec;apply Zle_trans.
+Qed.
+
+Lemma ltb_trans : forall x y z, x < y = true ->  y < z = true -> x < z = true.
+Proof.
+ intros x y z;rewrite !ltb_spec;apply Zlt_trans.
+Qed.
+
+Lemma ltb_leb_trans : forall x y z, x < y = true ->  y <= z = true -> x < z = true.
+Proof.
+ intros x y z;rewrite leb_spec, !ltb_spec;apply Zlt_le_trans.
+Qed.
+
+Lemma leb_ltb_trans : forall x y z, x <= y = true ->  y < z = true -> x < z = true.
+Proof.
+ intros x y z;rewrite leb_spec, !ltb_spec;apply Zle_lt_trans.
+Qed.
+
+Lemma gtb_not_leb : forall n m, m < n = true -> ~(n <= m = true).
+Proof.
+ intros n m; rewrite ltb_spec, leb_spec;omega.
+Qed.
+
+Lemma leb_not_gtb : forall n m, m <= n = true -> ~(n < m = true).
+Proof.
+ intros n m; rewrite ltb_spec, leb_spec;omega.
+Qed.
+
+Lemma leb_refl : forall n, n <= n = true.
+Proof.
+ intros n;rewrite leb_spec;apply Zle_refl.
+Qed.
+
+Lemma leb_negb_gtb : forall x y, x <= y = negb (y < x).
+Proof.
+ intros x y;apply Bool.eq_true_iff_eq;split;intros.
+ apply Bool.eq_true_not_negb;apply leb_not_gtb;trivial.
+ rewrite Bool.negb_true_iff, <- Bool.not_true_iff_false in H.
+ rewrite leb_spec; rewrite ltb_spec in H;omega.
+Qed.
+
+Lemma ltb_negb_geb : forall x y, x < y = negb (y <= x).
+Proof.
+ intros;rewrite leb_negb_gtb, Bool.negb_involutive;trivial.
+Qed.
+
+Lemma to_Z_sub_gt : forall x y, y <= x = true -> [|x - y|] = ([|x|] - [|y|])%Z.
+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.
+ intros Hd;assert ([|x|] <> 0)%Z;[ | omega].
+   intros Heq;elim Hd;apply to_Z_inj;trivial.
+ intros Hlt Heq;elimtype False.
+ assert ([|x|] = 0)%Z;[ rewrite Heq, to_Z_0;trivial | omega].
+Qed.
+
+Lemma not_ltb_refl : forall i, ~(i < i = true).
+Proof.
+ intros;rewrite ltb_spec;omega.
+Qed.
+
+Lemma to_Z_sub_1 : forall x y, y < x = true -> ([| x - 1|] = [|x|] - 1)%Z.
+Proof.
+ intros;apply to_Z_sub_gt.
+ 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.
+Qed.
+
+Lemma to_Z_add_1 : forall x y, x < y = true -> [|x+1|] = ([|x|] + 1)%Z.
+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.
+ rewrite ltb_spec, leb_spec, to_Z_sub_1_diff;trivial.
+ split;auto with zarith.
+Qed.
+
+Lemma ltb_leb_add1 : forall x y i, i < y = true -> (i < x = true <-> i + 1 <= x = true).
+Proof.
+ intros x y i Hlt.
+ rewrite ltb_spec, leb_spec.
+ rewrite (to_Z_add_1 i y);trivial.
+ split;auto with zarith.
+Qed.
+
+(** Iterators *)
+
+Lemma foldi_gt : forall A f from to (a:A), 
+  (to < from)%int63 = true -> foldi f from to a = a.
+Proof.
+ intros;unfold foldi;rewrite foldi_cont_gt;trivial.
+Qed.
+
+Lemma foldi_eq : forall A f from to (a:A),
+  from = to -> foldi f from to a = f from a.
+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).
+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.
+Proof.
+ intros;apply foldi_gt;trivial.
+Qed.
+
+Lemma fold_eq : forall A f from to (a:A),
+  from = to -> fold f from to a = f a.
+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).
+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.
+Proof.
+ intros;unfold foldi_down;rewrite foldi_down_cont_lt;trivial.
+Qed.
+
+Lemma foldi_down_eq : forall A f from downto (a:A),
+  from = downto -> foldi_down f from downto a = f from a.
+Proof.
+ intros;unfold foldi_down;rewrite foldi_down_cont_eq;trivial.
+Qed.
+
+Lemma foldi_down_gt : forall A f from downto (a:A),
+  (downto < from)%int63 = 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.
+Proof.
+ intros;apply foldi_down_lt;trivial.
+Qed.
+
+Lemma fold_down_eq : forall A f from downto (a:A),
+  from = downto -> fold_down f from downto a = f a.
+Proof.
+ intros;apply foldi_down_eq;trivial.
+Qed.
+
+Lemma fold_down_gt : forall A f from downto (a:A),
+  (downto < from)%int63 = true-> 
+  fold_down f from downto a = 
+  fold_down f (from-1) downto (f a).
+Proof.
+ intros;apply foldi_down_gt;trivial.
+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) ->
+  forall i, P i.
+Proof.
+ intros P HP0 Hrec.
+ assert (forall z, (0 <= z)%Z -> forall i, z = [|i|] -> P i).
+ intros z H;pattern z;apply natlike_rec2;intros;trivial.
+ rewrite <- (of_to_Z i), <- H0;exact HP0.
+ 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.
+  apply to_Z_inj.
+  rewrite add_spec, H2.
+  rewrite Zmod_small;rewrite to_Z_1;auto with zarith.
+ rewrite H3;apply Hrec.
+ rewrite ltb_spec, H2;change [|max_int|] with (wB - 1)%Z;auto with zarith.
+ apply X;auto with zarith.
+ 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 ->
+  (forall i, min <= i + 1 = true-> i < max =true-> P (i + 1) -> P i) ->
+  P min.
+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).
+ intros z H1;pattern z;apply natlike_rec2;intros;trivial.
+ assert (max - i = max)%int63.
+  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.
+  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.
+  apply to_Z_inj.
+  rewrite !sub_spec, !Zmod_small;auto with zarith.
+  rewrite Zmod_small;auto with zarith.
+ rewrite H;apply (X [| max - min |]);trivial;rewrite sub_spec, Zmod_small;auto with zarith.
+Qed.
+
+Lemma foldi_cont_ZInd : forall A B (P: Z -> (A -> B) -> Prop) (f:int -> (A -> B) -> (A -> B)) min max cont,
+   (forall z, ([|max|] < z)%Z -> P z cont) ->
+   (forall i cont, min <= i = true -> i <= max = true -> P ([|i|] + 1)%Z cont -> P [|i|] (f i cont)) ->
+   P [|min|] (foldi_cont f min max cont).
+Proof.
+ intros A B P f min max cont Ha Hf.
+ assert (Bmax:= to_Z_bounded max);assert (Bmin:= to_Z_bounded min).
+ case_eq (min <= max);intros Heq.
+ generalize (leb_refl min).
+ assert (P ([|max|] + 1)%Z cont) by (apply Ha;auto with zarith).
+ clear Ha;revert cont H.
+ pattern min at 2 3 4;apply int_ind_bounded with max;trivial.
+ intros;rewrite foldi_cont_eq;auto using leb_refl.
+ intros i Hle Hlt Hr cont Hcont Hle'.
+ rewrite foldi_cont_lt;[ | trivial].
+ apply Hf;trivial. rewrite leb_spec;rewrite ltb_spec in Hlt;auto with zarith.
+ assert ([|i|] + 1 = [|i + 1|])%Z.
+  rewrite ltb_spec in Hlt;assert (W:= to_Z_bounded i);rewrite add_spec, to_Z_1, Zmod_small;omega.
+ rewrite H;apply Hr;trivial.
+ assert (max < min = true) by (rewrite ltb_negb_geb,Heq;trivial).
+ 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. 
+Proof.
+ unfold of_pos.
+ unfold wB.
+ 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.
+Opaque Z_of_nat.
+  destruct p;simpl.
+  destruct (bit_add_or (of_pos_rec k p << 1) 1) as (H1, _).
+  rewrite <- H1;clear H1.
+  change (Zpos p~1) with (2*(Zpos p) + 1)%Z.
+  rewrite add_spec,lsl_spec, IHk, to_Z_1.
+  rewrite Zmult_comm, Zplus_mod_idemp_l, Zmod_small.
+  change 2%Z with (2^1)%Z.
+  rewrite Zmod_distr.
+  rewrite inj_S, Zpower_Zsucc;[ | apply Zle_0_nat].
+  repeat change (2^1)%Z with 2%Z.
+  rewrite Zmult_mod_distr_l;trivial.
+Transparent Z_of_nat.
+  rewrite inj_S;omega.
+  discriminate.
+  split;[discriminate | trivial].
+  compute;trivial.
+  assert (W:0 <= Zpos p mod 2 ^ Z_of_nat k < 2 ^ Z_of_nat k).
+   apply Z.mod_pos_bound;auto with zarith.
+  change (2^1)%Z with 2%Z;split;try omega.
+  apply Zlt_le_trans with (2 ^ Z_of_nat (S k)).
+  rewrite inj_S, Zpower_Zsucc;omega.
+  unfold wB;apply Zpower_le_monotone;auto with zarith.
+  split;auto using inj_le with zarith.
+  auto with zarith.
+  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.
+  rewrite inj_S, Zpower_Zsucc;[ | apply Zle_0_nat].
+  rewrite Zmult_mod_distr_l;trivial.
+  assert (W:0 <= Zpos p mod 2 ^ Z_of_nat k < 2 ^ Z_of_nat k).
+   apply Z.mod_pos_bound;auto with zarith.
+  change (2^1)%Z with 2%Z;split;try omega.
+  apply Zlt_le_trans with (2 ^ Z_of_nat (S k)).
+  rewrite inj_S, Zpower_Zsucc;omega.
+  unfold wB;apply Zpower_le_monotone;auto with zarith.
+  split;auto using inj_le with zarith.
+  auto with zarith.
+
+  rewrite to_Z_1, Zmod_small;trivial.
+  split;auto with zarith.
+  apply Zpower_gt_1;auto with zarith.
+  rewrite inj_S;auto with zarith.
+  
+  apply H;auto with zarith.
+Qed.
+
+Lemma of_Z_spec : forall z, [|of_Z z|] = z mod wB.
+Proof.
+ unfold of_Z;destruct z.
+ assert (W:= to_Z_bounded 0);rewrite Zmod_small;trivial.
+ apply of_pos_spec.
+ rewrite opp_spec, of_pos_spec.
+ rewrite <- Zmod_opp_opp.
+ change (- Zpos p)%Z with (Zneg p).
+ destruct (Z_eq_dec (Zneg p mod wB) 0).
+ rewrite e, Z_mod_zero_opp_r;trivial.
+ rewrite Z_mod_nz_opp_r, Zminus_mod, Z_mod_same_full, Zmod_mod, Zminus_0_r, Zmod_mod;trivial.
+Qed.
+
+Lemma foldi_cont_Ind : forall A B (P: int -> (A -> B) -> Prop) (f:int -> (A -> B) -> (A -> B)) min max cont,
+   max < max_int = true ->
+   (forall z, max < z = true -> P z cont) ->
+   (forall i cont, min <= i = true -> i <= max = true -> P (i + 1) cont -> P i (f i cont)) ->
+   P min (foldi_cont f min max cont).
+Proof.
+ intros.
+ set (P' z cont := (0 <= z < wB)%Z -> P (of_Z z) cont).
+ assert (P' [|min|] (foldi_cont f min max cont)).
+ apply foldi_cont_ZInd;unfold P';intros.
+ assert ([|(of_Z z)|] = z).
+  rewrite of_Z_spec, Zmod_small;trivial.
+ apply H0;rewrite ltb_spec, H4;trivial.
+ rewrite of_to_Z;apply H1;trivial.
+ assert (i < max_int = true).
+   apply leb_ltb_trans with max;trivial.
+ rewrite <- (to_Z_add_1 _ _ H6), of_to_Z in H4;apply H4.
+ apply to_Z_bounded.
+ unfold P' in H2;rewrite of_to_Z in H2;apply H2;apply to_Z_bounded.
+Qed.
+
+Lemma foldi_cont_ind : forall A B (P: (A -> B) -> Prop) (f:int -> (A -> B) -> (A -> B)) min max cont,
+   P cont ->
+   (forall i cont, min <= i = true -> i <= max = true -> P cont -> P (f i cont)) ->
+   P (foldi_cont f min max cont).
+Proof.
+ intros A B P f min max cont Ha Hf.
+ set (P2 := fun (z:Z) b => P b);change (P2 [|min|] (foldi_cont f min max cont)).
+ apply foldi_cont_ZInd;trivial.
+Qed.
+
+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 -> 
+      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 := 
+       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
+                       max (fun a0 : A => a0))).
+ apply foldi_cont_ZInd;intros;red.
+ rewrite Zlt_is_lt_bool in H1;rewrite H1;trivial.
+ case_eq (Zlt_bool [|max|] [|i|]);intros.
+  rewrite <- Zlt_is_lt_bool in H4;rewrite leb_spec in H2;elimtype False;omega.
+ clear H4; revert H3;unfold P'.
+ case_eq (Zlt_bool [|max|] ([|i|] + 1));intros;auto.
+  rewrite <- Zlt_is_lt_bool in H3; assert ([|i|] = [|max|]) by (rewrite leb_spec in H2;omega).
+  rewrite H4, <- H6;apply H0;trivial.
+ revert H1;unfold P'.
+ case_eq (Zlt_bool [|max|] [|min|]);auto.
+ 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,  
+  (max < max_int = true) ->
+  (max < min = true -> P (max + 1) a) ->
+  P min a ->
+  (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 (P' ([|max|]+1)%Z (foldi f min max a)).
+ apply foldi_ZInd;unfold P';intros.
+ rewrite <- W, of_to_Z;auto.
+ rewrite of_to_Z;trivial.
+ assert (i < max_int = true).
+   apply leb_ltb_trans with max;trivial.
+ rewrite <- (to_Z_add_1 _ _ H7), of_to_Z;apply H2;trivial.
+ rewrite of_to_Z in H5;apply H5;apply to_Z_bounded.
+ unfold P' in H3;rewrite <- W, of_to_Z in H3;apply H3;apply to_Z_bounded.
+Qed.
+
+Lemma foldi_ind : forall A (P: A -> Prop) (f:int -> A -> A) min max a,
+   P a ->
+   (forall i a, min <= i = true -> i <= max = true -> P a -> P (f i a)) ->
+   P (foldi f min max a).
+Proof.
+ unfold foldi;intros A P f min max a Ha Hr;revert a Ha.
+ apply foldi_cont_ind;auto.
+Qed.
+
+Lemma fold_ind : forall A (P: A -> Prop) (f: A -> A) min max a,
+   P a -> (forall a, P a -> P (f a)) -> P (fold f min max a).
+Proof.
+ unfold fold;intros A P f min max a Ha Hr;revert a Ha.
+ apply foldi_cont_ind;auto.
+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 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.
+ intros A B P f max min cont Ha Hf.
+ assert (Bmax:= to_Z_bounded max);assert (Bmin:= to_Z_bounded min).
+ case_eq (min <= max);intros Heq.
+ generalize (leb_refl max).
+ assert (P ([|min|] -1)%Z cont) by (apply Ha;auto with zarith).
+ clear Ha;revert cont H Heq.
+ pattern max at 1 2 4 5;apply int_ind;trivial.
+ intros; assert (0 = min).
+   apply to_Z_inj;revert Heq;rewrite leb_spec, to_Z_0;omega.
+ rewrite foldi_down_cont_eq;subst;auto.
+ intros i Hmaxi Hr cont Hcont Hmin Hmax.
+ generalize Hmin;rewrite leb_ltb_eqb;case_eq (min < i+1);simpl;intros Hlt Hmin'.
+ rewrite foldi_down_cont_gt;[ | trivial].
+ apply Hf;trivial.
+ assert ([|i|] + 1 = [|i + 1|])%Z.
+   assert (W:= to_Z_bounded i);rewrite ltb_spec in Hmaxi;
+    assert (W2 := to_Z_bounded max_int);rewrite add_spec, to_Z_1, Zmod_small;auto with zarith.
+ assert (i + 1 - 1 = i).
+  rewrite leb_spec in *;rewrite ltb_spec in *.
+  assert (W1:= to_Z_bounded i); apply to_Z_inj;rewrite sub_spec,to_Z_1, Zmod_small;try omega.
+ assert ([|i|] = [|i+1|]-1)%Z.
+   rewrite <- H;ring.
+ rewrite <- H1, H0;apply Hr;trivial.
+ rewrite ltb_spec in Hlt;rewrite leb_spec;omega.
+ rewrite leb_spec in Hmax |- *;omega.
+ rewrite eqb_spec in Hmin';subst;rewrite foldi_down_cont_eq;auto.
+ assert (max < min = true) by (rewrite ltb_negb_geb,Heq;trivial).
+ rewrite foldi_down_cont_lt;trivial.
+ apply Ha;rewrite <- ltb_spec;trivial.
+Qed.
+
+Lemma foldi_down_cont_ind : forall A B (P: (A -> B) -> Prop) (f:int -> (A -> B) -> (A -> B)) max min cont,
+   P cont ->
+   (forall i cont, min <= i = true -> i <= max = true -> P cont -> P (f i cont)) ->
+   P (foldi_down_cont f max min cont).
+Proof.
+ intros A B P f max min cont Ha Hf.
+ set (P2 := fun (z:Z) b => P b);change (P2 [|max|] (foldi_down_cont f max min cont)).
+ apply foldi_down_cont_ZInd;trivial.
+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) -> 
+   (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 := 
+       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
+                       min (fun a0 : A => a0))).
+ apply foldi_down_cont_ZInd;intros;red.
+ rewrite Zlt_is_lt_bool in H1;rewrite H1;trivial.
+ case_eq (Zlt_bool [|i|] [|min|]);intros.
+  rewrite <- Zlt_is_lt_bool in H4;rewrite leb_spec in H1;elimtype False;omega.
+ clear H4;revert H3;unfold P'.
+ case_eq (Zlt_bool ([|i|] - 1) [|min|]);intros;auto.
+  rewrite <- Zlt_is_lt_bool in H3; assert ([|i|] = [|min|]) by (rewrite leb_spec in H1;omega).
+  rewrite H4, <- H6. apply H0;trivial.
+ revert H1;unfold P'.
+ case_eq (Zlt_bool [|max|] [|min|]);auto.
+ rewrite <- Zlt_is_lt_bool, <- ltb_spec;intros;rewrite foldi_down_cont_lt;auto.
+Qed.
+
+Lemma foldi_down_ind : forall A (P: A -> Prop) (f:int -> A -> A) max min a,
+   P a ->
+   (forall i a, min <= i = true -> i <= max = true -> P a -> P (f i a)) ->
+   P (foldi_down f max min a).
+Proof.
+ unfold foldi_down;intros A P f max min a Ha Hr;revert a Ha.
+ apply foldi_down_cont_ind;auto.
+Qed.
+
+Lemma fold_down_ind : forall A (P: A -> Prop) (f: A -> A) max min a,
+   P a -> (forall a, P a -> P (f a)) -> P (fold_down f max min a).
+Proof.
+ unfold fold_down;intros A P f max min a Ha Hr;revert a Ha.
+ apply foldi_down_cont_ind;auto.
+Qed.
+
+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) -> 
+   (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 (P' ([|min|]-1)%Z (foldi_down f max min a)).
+ apply foldi_down_ZInd;unfold P';intros.
+ rewrite <- W, of_to_Z;auto.
+ rewrite of_to_Z;trivial.
+ assert (0 < i = true).
+   apply ltb_leb_trans with min;trivial.
+ rewrite <- (to_Z_sub_1 _ _ H7), of_to_Z;apply H2;trivial.
+ rewrite of_to_Z in H5;apply H5;apply to_Z_bounded.
+ unfold P' in H3;rewrite <- W, of_to_Z in H3;apply H3;apply to_Z_bounded.
+Qed.
+
+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. 
+  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).
+   rewrite ltb_leb_add1 with (y:=max_int), leb_refl;trivial.
+  assert (P (max - min)).
+    apply int_ind;unfold P.
+      replace (min + 0) with min.
+      intros _ a'; rewrite foldi_down_eq, foldi_down_lt;trivial.
+      apply to_Z_inj;rewrite add_spec, to_Z_0, Zplus_0_r, Zmod_small;auto using to_Z_bounded.
+    intros i Hi Hrec Hi1 a'.
+    rewrite add_assoc.
+    assert (Wi:= to_Z_add_1 _ _ Hi).
+    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).
+      rewrite leb_spec, (add_spec (min+1)).
+      unfold is_true in Hi1;rewrite leb_spec in *; rewrite ltb_spec in *.
+      rewrite sub_spec in Hi1;rewrite Zmod_small in Hi1;[ | omega].
+      rewrite Zmod_small;omega.
+      rewrite <- !add_assoc, (add_comm 1 i);trivial.
+    rewrite leb_ltb_eqb in H2;revert H2.
+    case_eq (min + 1 < min + i + 1).
+      intros Hlt _;rewrite foldi_down_gt.
+      rewrite foldi_down_gt with (from := min + i + 1);trivial.
+      replace (min + i + 1 - 1) with (min + i).
+      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.
+      rewrite Zmod_small;auto using to_Z_bounded.
+      apply leb_ltb_trans with (2:= Hlt).
+      rewrite leb_spec;omega.
+    simpl;rewrite eqb_spec;intros _ Heq.
+    rewrite <- Heq.
+    rewrite foldi_down_gt.
+     replace (min + 1 - 1) with min.
+     rewrite !foldi_down_eq;trivial.
+     apply to_Z_inj;rewrite sub_spec, add_spec, to_Z_1, Zminus_mod_idemp_l.
+     replace ([|min|] + 1 - 1)%Z with [|min|] by ring.
+     rewrite Zmod_small;auto using to_Z_bounded.
+     rewrite ltb_spec;omega.
+  generalize (H2 (leb_refl _) a).
+  replace (min + (max - min)) with max;trivial.
+  apply to_Z_inj;rewrite add_spec, sub_spec, Zplus_mod_idemp_r.
+  ring_simplify ([|min|] + ([|max|] - [|min|]))%Z.
+  rewrite Zmod_small;auto using to_Z_bounded.
+Qed.
+
+Definition foldi_ntr A f min max (a:A) :=
+  foldi_cont (fun i cont _ => f i (cont tt)) min max (fun _ => a) tt.
+
+Lemma foldi_ntr_foldi_down : forall A f min max (a:A),
+  max < max_int = true ->
+  foldi_down f max min a = foldi_ntr _ f min max a.
+Proof.
+ intros;unfold foldi_ntr.
+ apply foldi_cont_Ind;trivial.
+   intros;apply foldi_down_lt;trivial.
+ intros i cont Hmin Hmax Heq;rewrite <- Heq;clear Heq.
+ apply foldi_down_min;trivial.
+ apply leb_ltb_trans with (1:= Hmax);trivial.
+Qed.
+
+
+(** Two iterators *)
+
+Lemma foldi_cont_ZInd2 : forall A B C D (P: Z -> (A -> B) -> (C -> D) -> Prop) (f1 : int -> (A -> B) -> (A -> B)) (f2 : int -> (C -> D) -> (C -> D)) min max cont1 cont2,
+  (forall z, ([|max|] < z)%Z -> P z cont1 cont2) ->
+  (forall i cont1 cont2, min <= i = true -> i <= max = true -> P ([|i|] + 1)%Z cont1 cont2 ->
+    P [|i|] (f1 i cont1) (f2 i cont2)) ->
+  P [|min|] (foldi_cont f1 min max cont1) (foldi_cont f2 min max cont2).
+Proof.
+  intros.
+  set (P' z cont :=
+    if Zlt_bool [|max|] z then cont = cont1
+      else P z cont (foldi_cont f2 (of_Z z) max cont2)).
+  assert (P' [|min|] (foldi_cont f1 min max cont1)).
+  apply foldi_cont_ZInd;unfold P';intros.
+  rewrite Zlt_is_lt_bool in H1;rewrite H1;trivial.
+  case_eq (Zlt_bool [|max|] [|i|]);intros.
+  rewrite <- Zlt_is_lt_bool, <- ltb_spec in H4.
+  elim (not_ltb_refl max);apply ltb_leb_trans with i;trivial.
+  rewrite of_to_Z;generalize H2;rewrite leb_ltb_eqb, orb_true_iff;intros [Hlt | Heq].
+  rewrite foldi_cont_lt;[apply H0 | ];trivial.
+  revert H3;case_eq (Zlt_bool [|max|] ([|i|] + 1)).
+  rewrite <- Zlt_is_lt_bool;rewrite ltb_spec in Hlt;intros;elimtype False;omega.
+  rewrite <- (to_Z_add_1 _ _ Hlt), of_to_Z; intros _ W;exact W.
+  rewrite eqb_spec in Heq;subst.
+  rewrite foldi_cont_eq;[apply H0 | ];trivial.
+  assert ([|max|] < [|max|] + 1)%Z by auto with zarith.
+  rewrite Zlt_is_lt_bool in H5;rewrite H5 in H3;rewrite H3.
+  apply H;rewrite Zlt_is_lt_bool;trivial.
+  revert H1;unfold P';case_eq (Zlt_bool [|max|] [|min|]).
+  rewrite <- Zlt_is_lt_bool;intros.
+  rewrite H2;rewrite foldi_cont_gt;[ | rewrite ltb_spec];auto.
+  rewrite of_to_Z;auto.
+Qed.
+
+
+Lemma foldi_cont_ind2 : forall A B C D (P: (A -> B) -> (C -> D) -> Prop) (f:int -> (A -> B) -> (A -> B)) (g:int -> (C -> D) -> (C -> D)) min max cont1 cont2,
+  P cont1 cont2 ->
+  (forall i cont1 cont2, min <= i = true -> i <= max = true -> P cont1 cont2 -> P (f i cont1) (g i cont2)) ->
+  P (foldi_cont f min max cont1) (foldi_cont g min max cont2).
+Proof.
+  intros A B C D P f g min max cont1 cont2 Ha Hf.
+  set (P2 := fun (z:Z) b c => P b c);change (P2 [|min|] (foldi_cont f min max cont1) (foldi_cont g min max cont2)).
+  apply foldi_cont_ZInd2;trivial.
+Qed.
+
+
+Lemma foldi_ZInd2 : forall A B (P : Z -> A -> B -> Prop) f g min max a b,
+  (max < min = true -> P ([|max|] + 1)%Z a b) ->
+  P [|min|] a b ->
+  (forall i a b, min <= i = true -> i <= max = true ->
+    P [|i|] a b -> P ([|i|] + 1)%Z (f i a) (g i b)) ->
+  P ([|max|]+1)%Z (foldi f min max a) (foldi g min max b).
+Proof.
+  unfold foldi;intros A B P f g min max a b Hlt;intros.
+  set (P' z cont1 cont2 :=
+    if Zlt_bool [|max|] z then cont1 = (fun a : A => a) /\ cont2 = (fun b : B => b)
+      else forall a b, P z a b -> P ([|max|]+1)%Z (cont1 a) (cont2 b)).
+  assert (P' [|min|] (foldi_cont (fun (i : int) (cont : A -> A) (a : A) => cont (f i a)) min
+    max (fun a : A => a))
+  (foldi_cont (fun (i : int) (cont : B -> B) (b : B) => cont (g i b)) min
+    max (fun b : B => b))).
+  apply foldi_cont_ZInd2;intros;red.
+  rewrite Zlt_is_lt_bool in H1;rewrite H1;auto.
+  case_eq (Zlt_bool [|max|] [|i|]);intros.
+  rewrite <- Zlt_is_lt_bool in H4;rewrite leb_spec in H2;elimtype False;omega.
+  clear H4; revert H3;unfold P'.
+  case_eq (Zlt_bool [|max|] ([|i|] + 1));intros;auto.
+  rewrite <- Zlt_is_lt_bool in H3; assert ([|i|] = [|max|]) by (rewrite leb_spec in H2;omega).
+  destruct H4;subst;rewrite <- H6;apply H0;trivial.
+  revert H1;unfold P'.
+  case_eq (Zlt_bool [|max|] [|min|]);auto.
+  rewrite <- Zlt_is_lt_bool, <- ltb_spec;intros;rewrite !foldi_cont_gt;auto.
+Qed.
+
+
+Lemma foldi_Ind2 : forall A B (P : int -> A -> B -> Prop) f g min max a b,
+  (max < max_int = true) ->
+  (max < min = true -> P (max + 1) a b) ->
+  P min a b ->
+  (forall i a b, min <= i = true -> i <= max = true ->
+    P i a b -> P (i + 1) (f i a) (g i b)) ->
+  P (max+1) (foldi f min max a) (foldi g min max b).
+Proof.
+  intros.
+  set (P' z a b := (0 <= z < wB)%Z -> P (of_Z z) a b).
+  assert (W:= to_Z_add_1 _ _ H).
+  assert (P' ([|max|]+1)%Z (foldi f min max a) (foldi g min max b)).
+  apply foldi_ZInd2;unfold P';intros.
+  rewrite <- W, of_to_Z;auto.
+  rewrite of_to_Z;trivial.
+  assert (i < max_int = true).
+  apply leb_ltb_trans with max;trivial.
+  rewrite <- (to_Z_add_1 _ _ H7), of_to_Z;apply H2;trivial.
+  rewrite of_to_Z in H5;apply H5;apply to_Z_bounded.
+  unfold P' in H3;rewrite <- W, of_to_Z in H3;apply H3;apply to_Z_bounded.
+Qed.
+
+
+Lemma foldi_ind2 : forall A B (P: A -> B -> Prop) (f:int -> A -> A) (g:int -> B -> B) min max a b,
+  P a b ->
+  (forall i a b, min <= i = true -> i <= max = true -> P a b -> P (f i a) (g i b)) ->
+  P (foldi f min max a) (foldi g min max b).
+Proof.
+  unfold foldi;intros A B P f g min max a b Ha Hr; revert a b Ha.
+  apply (foldi_cont_ind2 _ _ _ _ (fun cont1 cont2 => forall a b, P a b -> P (cont1 a) (cont2 b))); auto.
+Qed.
+
+
+Lemma fold_ind2 : forall A B (P: A -> B -> Prop) (f: A -> A) (g: B -> B) min max a b,
+  P a b -> (forall a b, P a b -> P (f a) (g b)) -> P (fold f min max a) (fold g min max b).
+Proof.
+  unfold fold;intros A B P f g min max a b Ha Hr;revert a b Ha.
+  apply (foldi_cont_ind2 _ _ _ _ (fun cont1 cont2 => forall a b, P a b -> P (cont1 a) (cont2 b)));auto.
+Qed.
+
+Lemma foldi_eq_compat : forall A (f1 f2:int -> A -> A) min max a,
+  (forall i a, min <= i = true -> i <= max = true -> f1 i a = f2 i a) ->
+  foldi f1 min max a = foldi f2 min max a.
+Proof.
+ intros; set (P' (z:Z) (a1 a2:A) := a1 = a2).
+ assert (P' ([|max|] + 1)%Z (foldi f1 min max a) (foldi f2 min max a)).
+ apply foldi_ZInd2;unfold P';intros;subst;auto.
+ apply H0.
+Qed.
+
+Lemma foldi_down_cont_ZInd2 :
+  forall A B C D (P: Z -> (A -> B) -> (C -> D) -> Prop) (f1:int -> (A -> B) -> (A -> B)) (f2:int -> (C -> D) -> (C -> D)) max min cont1 cont2,
+    (forall z, (z < [|min|])%Z -> P z cont1 cont2) ->
+    (forall i cont1 cont2, min <= i = true -> i <= max = true -> P ([|i|] - 1)%Z cont1 cont2 ->
+      P [|i|] (f1 i cont1) (f2 i cont2)) ->
+    P [|max|] (foldi_down_cont f1 max min cont1) (foldi_down_cont f2 max min cont2).
+Proof.
+  intros.
+  set (P' z cont :=
+    if Zlt_bool z [|min|] then cont = cont1
+      else P z cont (foldi_down_cont f2 (of_Z z) min cont2)).
+  assert (P' [|max|] (foldi_down_cont f1 max min cont1)).
+  apply foldi_down_cont_ZInd;unfold P';intros.
+  rewrite Zlt_is_lt_bool in H1;rewrite H1;trivial.
+  case_eq (Zlt_bool [|i|] [|min|]);intros.
+  rewrite <- Zlt_is_lt_bool, <- ltb_spec in H4.
+  elim (not_ltb_refl min);apply leb_ltb_trans with i;trivial.
+  rewrite of_to_Z;generalize H1;rewrite leb_ltb_eqb, orb_true_iff;intros [Hlt | Heq].
+  rewrite foldi_down_cont_gt;[apply H0 | ];trivial.
+  revert H3;case_eq (Zlt_bool ([|i|] - 1) [|min|]).
+  rewrite <- Zlt_is_lt_bool;rewrite ltb_spec in Hlt;intros;elimtype False;omega.
+  rewrite <- (to_Z_sub_1 _ _ Hlt), of_to_Z; intros _ W;exact W.
+  rewrite eqb_spec in Heq;subst.
+  rewrite foldi_down_cont_eq;[apply H0 | ];trivial.
+  assert ([|i|] - 1 < [|i|])%Z by auto with zarith.
+  rewrite Zlt_is_lt_bool in H5;rewrite H5 in H3;rewrite H3.
+  apply H;rewrite Zlt_is_lt_bool;trivial.
+  revert H1;unfold P';case_eq (Zlt_bool [|max|] [|min|]).
+  rewrite <- Zlt_is_lt_bool;intros.
+  rewrite H2;rewrite foldi_down_cont_lt;[ | rewrite ltb_spec];auto.
+  rewrite of_to_Z;auto.
+Qed.
+
+
+Lemma foldi_down_cont_ind2 : forall A B C D (P: (A -> B) -> (C -> D) -> Prop) (f:int -> (A -> B) -> (A -> B)) (g:int -> (C -> D) -> (C -> D)) max min cont1 cont2,
+  P cont1 cont2 ->
+  (forall i cont1 cont2, min <= i = true -> i <= max = true -> P cont1 cont2 -> P (f i cont1) (g i cont2)) ->
+  P (foldi_down_cont f max min cont1) (foldi_down_cont g max min cont2).
+Proof.
+  intros A B C D P f g max min cont1 cont2 Ha Hf.
+  set (P2 := fun (z:Z) b c => P b c);change (P2 [|max|] (foldi_down_cont f max min cont1) (foldi_down_cont g max min cont2)).
+  apply foldi_down_cont_ZInd2;trivial.
+Qed.
+
+
+Lemma foldi_down_ZInd2 :
+  forall A B (P: Z -> A -> B -> Prop) (f1:int -> A -> A) (f2:int -> B -> B) max min a1 a2,
+    (max < min = true -> P ([|min|] - 1)%Z a1 a2) ->
+    (P [|max|] a1 a2) ->
+    (forall z, (z < [|min|])%Z -> P z a1 a2) ->
+    (forall i a1 a2, min <= i = true -> i <= max = true -> P [|i|] a1 a2 ->
+      P ([|i|] - 1)%Z (f1 i a1) (f2 i a2)) ->
+    P ([|min|] - 1)%Z (foldi_down f1 max min a1) (foldi_down f2 max min a2).
+Proof.
+  unfold foldi_down;intros A B P f1 f2 max min a1 a2 Hlt;intros.
+  set (P' z cont1 cont2 :=
+    if Zlt_bool z [|min|] then cont1 = (fun a0 : A => a0) /\ cont2 = (fun a0 : B => a0)
+      else forall a1 a2, P z a1 a2 -> P ([|min|] - 1)%Z (cont1 a1) (cont2 a2)).
+  assert (P' [|max|] (foldi_down_cont (fun (i : int) (cont : A -> A) (a0 : A) => cont (f1 i a0)) max
+    min (fun a0 : A => a0))
+  (foldi_down_cont (fun (i : int) (cont : B -> B) (a0 : B) => cont (f2 i a0)) max
+    min (fun a0 : B => a0))).
+  apply foldi_down_cont_ZInd2;intros;red.
+  rewrite Zlt_is_lt_bool in H2;rewrite H2;auto.
+  case_eq (Zlt_bool [|i|] [|min|]);intros.
+  rewrite <- Zlt_is_lt_bool in H5;rewrite leb_spec in H2;elimtype False;omega.
+  clear H5;revert H4;unfold P'.
+  case_eq (Zlt_bool ([|i|] - 1) [|min|]);intros;auto.
+  rewrite <- Zlt_is_lt_bool in H4; assert ([|i|] = [|min|]) by (rewrite leb_spec in H2;omega).
+  destruct H5;subst;rewrite <- H7;apply H1;trivial.
+  revert H2;unfold P'.
+  case_eq (Zlt_bool [|max|] [|min|]);auto.
+  rewrite <- Zlt_is_lt_bool, <- ltb_spec;intros;rewrite foldi_down_cont_lt;auto.
+  destruct H3. rewrite H4;auto.
+Qed.
+
+
+Lemma foldi_down_ind2 : forall A B (P: A -> B -> Prop) (f:int -> A -> A) (g:int -> B -> B) max min a b,
+  P a b ->
+  (forall i a b, min <= i = true -> i <= max = true -> P a b -> P (f i a) (g i b)) ->
+  P (foldi_down f max min a) (foldi_down g max min b).
+Proof.
+  unfold foldi_down;intros A B P f g max min a b Ha Hr;revert a b Ha.
+  apply (foldi_down_cont_ind2 _ _ _ _ (fun cont1 cont2 => forall a b, P a b -> P (cont1 a) (cont2 b)));auto.
+Qed.
+
+
+Lemma fold_down_ind2 : forall A B (P: A -> B -> Prop) (f: A -> A) (g: B -> B) max min a b,
+  P a b -> (forall a b, P a b -> P (f a) (g b)) -> P (fold_down f max min a) (fold_down g max min b).
+Proof.
+  unfold fold_down;intros A B P f g max min a b Ha Hr;revert a b Ha.
+  apply (foldi_down_cont_ind2 _ _ _ _ (fun cont1 cont2 => forall a b, P a b -> P (cont1 a) (cont2 b)));auto.
+Qed.
+
+Lemma foldi_down_eq_compat : forall A (f1 f2:int -> A -> A) max min a,
+  (forall i a, min <= i = true -> i <= max = true -> f1 i a = f2 i a) ->
+  foldi_down f1 max min a = foldi_down f2 max min a.
+Proof.
+  intros; set (P' (z:Z) (a1 a2:A) := a1 = a2).
+  assert (P' ([|min|] - 1)%Z (foldi_down f1 max min a) (foldi_down f2 max min a)).
+  apply foldi_down_ZInd2;unfold P';intros;subst;auto.
+  apply H0.
+Qed.
+
+
+Lemma forallb_spec : forall f from to, 
+  forallb f from to = true <->
+  forall i, from <= i = true -> i <= to = true -> f i = true.
+Proof.
+ unfold forallb;intros f from to.
+ setoid_rewrite leb_spec.
+ apply foldi_cont_ZInd.
+ intros;split;[intros;elimtype False;omega | trivial].
+ intros i cont Hfr Hto Hcont.
+ case_eq (f i);intros Heq.
+ rewrite Hcont;clear Hcont;split;auto with zarith;intros.
+ assert (H2 : ([|i0|] = [|i|] \/ [|i|] + 1 <= [|i0|])%Z) by omega; destruct H2;auto with zarith.
+ apply to_Z_inj in H2;rewrite H2;trivial.
+ split;[discriminate | intros].
+ rewrite leb_spec in Hto;rewrite <- Heq;auto with zarith.
+Qed.
+
+Lemma forallb_eq_compat : forall f1 f2 from to,
+  (forall i, from <= i = true -> i <= to = true -> f1 i = f2 i) ->
+  forallb f1 from to = forallb f2 from to.
+Proof.
+ unfold forallb;intros.
+ set (P' (z:Z) (cont1 cont2:unit -> bool) := cont1 tt = cont2 tt).
+ refine (foldi_cont_ZInd2 _ _ _ _ P' _ _ from to _ _ _ _);unfold P';intros;trivial.
+ rewrite H2, H;trivial.
+Qed.
+
+Lemma existsb_spec : forall f from to,
+  existsb f from to = true <->
+  exists i, ((from <= i) && (i <= to) && (f i)) = true .
+Proof.
+ unfold existsb;intros.
+ repeat setoid_rewrite andb_true_iff;setoid_rewrite leb_spec.
+ apply foldi_cont_ZInd.
+ intros;split;[discriminate | intros [i [W1 W2]];elimtype False;omega].
+ intros i cont Hfr Hto Hcont.
+ case_eq (f i);intros Heq.
+  split;trivial.
+  exists i;rewrite leb_spec in Hto;auto with zarith.
+ rewrite Hcont;clear Hcont;split;intros [i0 [W1 W2]];
+  exists i0;split;auto with zarith.
+ assert (~ [|i|] = [|i0|]);[ | auto with zarith].
+ intros W;apply to_Z_inj in W;rewrite W in Heq;rewrite Heq in W2;discriminate.
+Qed.
+
+Lemma existsb_eq_compat : forall f1 f2 from to,
+  (forall i, from <= i = true -> i <= to = true -> f1 i = f2 i) ->
+  existsb f1 from to = existsb f2 from to.
+Proof.
+ unfold existsb;intros.
+ set (P' (z:Z) (cont1 cont2:unit -> bool) := cont1 tt = cont2 tt).
+ refine (foldi_cont_ZInd2 _ _ _ _ P' _ _ from to _ _ _ _);unfold P';intros;trivial.
+ rewrite H2, H;trivial.
+Qed.
+
+Lemma bit_max_int : forall i, (i < digits)%int63 = true -> bit max_int i = true.
+Proof.
+ intros;apply (forallb_spec (bit max_int) 0 (digits - 1)).
+ compute;trivial.
+ apply leb_0.
+ rewrite ltb_spec in H.
+ destruct (to_Z_bounded i);rewrite leb_spec.
+ change [|digits - 1 |] with ([|digits|] - 1)%Z;omega.
+Qed.
+
+Lemma land_max_int_l : forall i, max_int land i = i.
+Proof.
+  intros;apply bit_eq;intros.
+  rewrite land_spec.
+  destruct (reflect_leb digits i0).
+  rewrite <- leb_spec in l.
+  rewrite !bit_M;trivial.
+  rewrite bit_max_int;trivial.
+  rewrite ltb_spec;omega.
+Qed.
+
+Lemma land_max_int_r : forall i, i land max_int = i.
+Proof.
+ intros;rewrite land_comm;apply land_max_int_l.
+Qed.
+
diff --git a/src/versions/standard/Int63/Int63_standard.v b/src/versions/standard/Int63/Int63_standard.v
new file mode 100644
index 0000000..3540b71
--- /dev/null
+++ b/src/versions/standard/Int63/Int63_standard.v
@@ -0,0 +1,20 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*       from the Int63 library of native-coq                             *)
+(*       by Benjamin Gregoire and Laurent Thery                           *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+Require Export Int63Native.
+Require Export Int63Op.
+Require Export Int63Axioms.
+Require Export Int63Properties.
diff --git a/src/versions/standard/Make b/src/versions/standard/Make
new file mode 100644
index 0000000..4325d32
--- /dev/null
+++ b/src/versions/standard/Make
@@ -0,0 +1,97 @@
+########################################################################
+##   This file is intended to developers, please do not use it to     ##
+## generate a Makefile, rather use the provided Makefile.             ##
+########################################################################
+
+
+
+
+########################################################################
+## To generate the Makefile:                                          ##
+##   coq_makefile -f Make -o Makefile                                 ##
+## Change the "all" target into:                                      ##
+##   all: ml $(CMXFILES) $(CMXA) $(CMXS) $(VOFILES)                   ##
+## Change the "install-natdynlink" target: change CMXSFILES into CMXS and add the same thing for CMXA. ##
+## Change the "install" target: change CMO into CMX.                  ##
+## Finally, suppress the "Makefile" target and add to the "clean" target: ##
+##   - rm -f ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml verit/smtlib2_parse.mli verit/smtlib2_parse.ml verit/smtlib2_lex.ml ##
+########################################################################
+
+
+-R . SMTCoq
+
+-I cnf
+-I euf
+-I lia
+-I trace
+-I verit
+-I zchaff
+-I versions/standard
+
+-custom "cd ../unit-tests; make" "" "test"
+
+-custom "$(CAMLLEX) $<" "%.mll" "%.ml"
+-custom "$(CAMLYACC) $<" "%.mly" "%.ml %.mli"
+-custom "" "verit/veritParser.ml verit/veritLexer.ml verit/smtlib2_parse.ml verit/smtlib2_lex.ml" "ml"
+
+-custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "versions/standard/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx verit/smtlib2_util.cmx verit/smtlib2_ast.cmx verit/smtlib2_parse.cmx verit/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx verit/smtlib2_genConstr.cmx verit/verit.cmx trace/smt_tactic.cmx" "$(CMXA)"
+-custom "$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^" "$(CMXA)" "$(CMXS)"
+
+CMXA = trace/smtcoq.cmxa
+CMXS = trace/smt_tactic.cmxs
+CAMLLEX = $(CAMLBIN)ocamllex
+CAMLYACC = $(CAMLBIN)ocamlyacc
+
+versions/standard/Int63/Int63.v
+versions/standard/Int63/Int63Native.v
+versions/standard/Int63/Int63Op.v
+versions/standard/Int63/Int63Axioms.v
+versions/standard/Int63/Int63Properties.v
+versions/standard/Array/PArray.v
+
+versions/standard/structures.ml
+
+trace/coqTerms.ml
+trace/satAtom.ml
+trace/smtAtom.ml
+trace/smtAtom.mli
+trace/smtCertif.ml
+trace/smtCnf.ml
+trace/smtForm.ml
+trace/smtForm.mli
+trace/smtMisc.ml
+trace/smt_tactic.ml4
+trace/smtTrace.ml
+
+verit/smtlib2_ast.ml
+verit/smtlib2_genConstr.ml
+verit/smtlib2_lex.ml
+verit/smtlib2_parse.ml
+verit/smtlib2_util.ml
+verit/veritParser.ml
+verit/veritLexer.ml
+verit/verit.ml
+verit/veritSyntax.ml
+verit/veritSyntax.mli
+
+zchaff/cnfParser.ml
+zchaff/satParser.ml
+zchaff/zchaff.ml
+zchaff/zchaffParser.ml
+
+cnf/Cnf.v
+
+euf/Euf.v
+
+lia/lia.ml
+lia/Lia.v
+
+spl/Syntactic.v
+spl/Arithmetic.v
+spl/Operators.v
+
+Misc.v
+SMTCoq.v
+SMT_terms.v
+State.v
+Trace.v
diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile
new file mode 100644
index 0000000..f22a0af
--- /dev/null
+++ b/src/versions/standard/Makefile
@@ -0,0 +1,429 @@
+#############################################################################
+##  v      #                   The Coq Proof Assistant                     ##
+## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##
+##   \VV/  #                                                               ##
+##    //   #  Makefile automagically generated by coq_makefile V8.4pl5     ##
+#############################################################################
+
+# WARNING
+#
+# This Makefile has been automagically generated
+# Edit at your own risks !
+#
+# END OF WARNING
+
+#
+# This Makefile was generated by the command line :
+# coq_makefile -f Make -o Makefile 
+#
+
+.DEFAULT_GOAL := all
+
+# 
+# This Makefile may take arguments passed as environment variables:
+# COQBIN to specify the directory where Coq binaries resides;
+# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;
+# DSTROOT to specify a prefix to install path.
+
+# Here is a hack to make $(eval $(shell works:
+define donewline
+
+
+endef
+includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; })))
+$(call includecmdwithout@,$(COQBIN)coqtop -config)
+
+##########################
+#                        #
+# Libraries definitions. #
+#                        #
+##########################
+
+OCAMLLIBS?=-I versions/standard\
+  -I zchaff\
+  -I verit\
+  -I trace\
+  -I lia\
+  -I euf\
+  -I cnf
+COQLIBS?=-I versions/standard\
+  -I zchaff\
+  -I verit\
+  -I trace\
+  -I lia\
+  -I euf\
+  -I cnf -R . SMTCoq
+COQDOCLIBS?=-R . SMTCoq
+
+##########################
+#                        #
+# Variables definitions. #
+#                        #
+##########################
+
+CAMLYACC=$(CAMLBIN)ocamlyacc
+CAMLLEX=$(CAMLBIN)ocamllex
+CMXS=trace/smt_tactic.cmxs
+CMXA=trace/smtcoq.cmxa
+
+OPT?=
+COQDEP?="$(COQBIN)coqdep" -c
+COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
+COQCHKFLAGS?=-silent -o
+COQDOCFLAGS?=-interpolate -utf8
+COQC?="$(COQBIN)coqc"
+GALLINA?="$(COQBIN)gallina"
+COQDOC?="$(COQBIN)coqdoc"
+COQCHK?="$(COQBIN)coqchk"
+
+COQSRCLIBS?=-I "$(COQLIB)kernel" -I "$(COQLIB)lib" \
+  -I "$(COQLIB)library" -I "$(COQLIB)parsing" -I "$(COQLIB)pretyping" \
+  -I "$(COQLIB)interp" -I "$(COQLIB)proofs" -I "$(COQLIB)tactics" \
+  -I "$(COQLIB)tools" -I "$(COQLIB)toplevel" \
+  -I "$(COQLIB)plugins/"cc \
+  -I "$(COQLIB)plugins/"decl_mode \
+  -I "$(COQLIB)plugins/"extraction \
+  -I "$(COQLIB)plugins/"field \
+  -I "$(COQLIB)plugins/"firstorder \
+  -I "$(COQLIB)plugins/"fourier \
+  -I "$(COQLIB)plugins/"funind \
+  -I "$(COQLIB)plugins/"micromega \
+  -I "$(COQLIB)plugins/"nsatz \
+  -I "$(COQLIB)plugins/"omega \
+  -I "$(COQLIB)plugins/"quote \
+  -I "$(COQLIB)plugins/"ring \
+  -I "$(COQLIB)plugins/"romega \
+  -I "$(COQLIB)plugins/"rtauto \
+  -I "$(COQLIB)plugins/"setoid_ring \
+  -I "$(COQLIB)plugins/"subtac \
+  -I "$(COQLIB)plugins/"subtac/test \
+  -I "$(COQLIB)plugins/"syntax \
+  -I "$(COQLIB)plugins/"xml
+ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)
+
+CAMLC?=$(OCAMLC) -c -rectypes
+CAMLOPTC?=$(OCAMLOPT) -c -rectypes
+CAMLLINK?=$(OCAMLC) -rectypes
+CAMLOPTLINK?=$(OCAMLOPT) -rectypes
+GRAMMARS?=grammar.cma
+CAMLP4EXTEND?=pa_extend.cmo pa_macro.cmo q_MLast.cmo
+CAMLP4OPTIONS?=-loc loc
+PP?=-pp '"$(CAMLP4BIN)$(CAMLP4)o" -I "$(CAMLLIB)" -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'
+
+##################
+#                #
+# Install Paths. #
+#                #
+##################
+
+ifdef USERINSTALL
+XDG_DATA_HOME?="$(HOME)/.local/share"
+COQLIBINSTALL=$(XDG_DATA_HOME)/coq
+COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq
+else
+COQLIBINSTALL="${COQLIB}user-contrib"
+COQDOCINSTALL="${DOCDIR}user-contrib"
+endif
+
+######################
+#                    #
+# Files dispatching. #
+#                    #
+######################
+
+VFILES:=Trace.v\
+  State.v\
+  SMT_terms.v\
+  SMTCoq.v\
+  Misc.v\
+  spl/Operators.v\
+  spl/Arithmetic.v\
+  spl/Syntactic.v\
+  lia/Lia.v\
+  euf/Euf.v\
+  cnf/Cnf.v\
+  versions/standard/Array/PArray.v\
+  versions/standard/Int63/Int63Properties.v\
+  versions/standard/Int63/Int63Axioms.v\
+  versions/standard/Int63/Int63Op.v\
+  versions/standard/Int63/Int63Native.v\
+  versions/standard/Int63/Int63.v
+
+-include $(addsuffix .d,$(VFILES))
+.SECONDARY: $(addsuffix .d,$(VFILES))
+
+VOFILES:=$(VFILES:.v=.vo)
+GLOBFILES:=$(VFILES:.v=.glob)
+VIFILES:=$(VFILES:.v=.vi)
+GFILES:=$(VFILES:.v=.g)
+HTMLFILES:=$(VFILES:.v=.html)
+GHTMLFILES:=$(VFILES:.v=.g.html)
+ML4FILES:=trace/smt_tactic.ml4
+
+-include $(addsuffix .d,$(ML4FILES))
+.SECONDARY: $(addsuffix .d,$(ML4FILES))
+
+MLFILES:=lia/lia.ml\
+  zchaff/zchaffParser.ml\
+  zchaff/zchaff.ml\
+  zchaff/satParser.ml\
+  zchaff/cnfParser.ml\
+  verit/veritSyntax.ml\
+  verit/verit.ml\
+  verit/veritLexer.ml\
+  verit/veritParser.ml\
+  verit/smtlib2_util.ml\
+  verit/smtlib2_parse.ml\
+  verit/smtlib2_lex.ml\
+  verit/smtlib2_genConstr.ml\
+  verit/smtlib2_ast.ml\
+  trace/smtTrace.ml\
+  trace/smtMisc.ml\
+  trace/smtForm.ml\
+  trace/smtCnf.ml\
+  trace/smtCertif.ml\
+  trace/smtAtom.ml\
+  trace/satAtom.ml\
+  trace/coqTerms.ml\
+  versions/standard/structures.ml
+
+-include $(addsuffix .d,$(MLFILES))
+.SECONDARY: $(addsuffix .d,$(MLFILES))
+
+MLIFILES:=verit/veritSyntax.mli\
+  trace/smtForm.mli\
+  trace/smtAtom.mli
+
+-include $(addsuffix .d,$(MLIFILES))
+.SECONDARY: $(addsuffix .d,$(MLIFILES))
+
+ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo)
+CMOFILES=$(filter-out $(addsuffix .cmo,$(foreach lib,$(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES) $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ALLCMOFILES))
+CMXFILES=$(CMOFILES:.cmo=.cmx)
+OFILES=$(CMXFILES:.cmx=.o)
+CMIFILES=$(sort $(ALLCMOFILES:.cmo=.cmi) $(MLIFILES:.mli=.cmi))
+CMXSFILES=$(CMXFILES:.cmx=.cmxs)
+ifeq '$(HASNATDYNLINK)' 'true'
+HASNATDYNLINK_OR_EMPTY := yes
+else
+HASNATDYNLINK_OR_EMPTY :=
+endif
+
+#######################################
+#                                     #
+# Definition of the toplevel targets. #
+#                                     #
+#######################################
+
+all: ml $(CMXFILES) $(CMXA) $(CMXS) $(VOFILES)
+
+mlihtml: $(MLIFILES:.mli=.cmi)
+	 mkdir $@ || rm -rf $@/*
+	$(OCAMLDOC) -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)
+
+all-mli.tex: $(MLIFILES:.mli=.cmi)
+	$(OCAMLDOC) -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)
+
+spec: $(VIFILES)
+
+gallina: $(GFILES)
+
+html: $(GLOBFILES) $(VFILES)
+	- mkdir -p html
+	$(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)
+
+gallinahtml: $(GLOBFILES) $(VFILES)
+	- mkdir -p html
+	$(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)
+
+all.ps: $(VFILES)
+	$(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
+
+all-gal.ps: $(VFILES)
+	$(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
+
+all.pdf: $(VFILES)
+	$(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
+
+all-gal.pdf: $(VFILES)
+	$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
+
+validate: $(VOFILES)
+	$(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=))
+
+beautify: $(VFILES:=.beautified)
+	for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
+	@echo 'Do not do "make clean" until you are sure that everything went well!'
+	@echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/'
+
+.PHONY: all opt byte archclean clean install userinstall depend html validate
+
+###################
+#                 #
+# Custom targets. #
+#                 #
+###################
+
+$(CMXS): $(CMXA)
+	$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^
+
+$(CMXA): versions/standard/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx verit/smtlib2_util.cmx verit/smtlib2_ast.cmx verit/smtlib2_parse.cmx verit/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx verit/smtlib2_genConstr.cmx verit/verit.cmx trace/smt_tactic.cmx
+	$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^
+
+ml: verit/veritParser.ml verit/veritLexer.ml verit/smtlib2_parse.ml verit/smtlib2_lex.ml
+
+
+%.ml %.mli: %.mly
+	$(CAMLYACC) $<
+
+%.ml: %.mll
+	$(CAMLLEX) $<
+
+test: 
+	cd ../unit-tests; make
+
+####################
+#                  #
+# Special targets. #
+#                  #
+####################
+
+byte:
+	$(MAKE) all "OPT:=-byte"
+
+opt:
+	$(MAKE) all "OPT:=-opt"
+
+userinstall:
+	+$(MAKE) USERINSTALL=true install
+
+install-natdynlink:
+	for i in $(CMXS); do \
+	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
+	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
+	done
+	for i in $(CMXA); do \
+	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
+	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
+	done
+
+install:$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink)
+	for i in $(VOFILES); do \
+	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
+	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
+	done
+	for i in $(CMXFILES); do \
+	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
+	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
+	done
+	for i in $(CMIFILES); do \
+	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
+	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
+	done
+
+install-doc:
+	install -d "$(DSTROOT)"$(COQDOCINSTALL)/SMTCoq/html
+	for i in html/*; do \
+	 install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/SMTCoq/$$i;\
+	done
+	install -d "$(DSTROOT)"$(COQDOCINSTALL)/SMTCoq/mlihtml
+	for i in mlihtml/*; do \
+	 install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/SMTCoq/$$i;\
+	done
+
+clean:
+	rm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES)
+	rm -f $(ALLCMOFILES:.cmo=.cmx) $(CMXAFILES) $(CMXSFILES) $(ALLCMOFILES:.cmo=.o) $(CMXAFILES:.cmxa=.a)
+	rm -f $(addsuffix .d,$(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(MLPACKFILES))
+	rm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)
+	rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex
+	- rm -rf html mlihtml
+	- rm -rf $(CMXS)
+	- rm -rf $(CMXA)
+	- rm -rf ml
+	- rm -rf test
+	- rm -f ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml verit/smtlib2_parse.mli verit/smtlib2_parse.ml verit/smtlib2_lex.ml
+
+archclean:
+	rm -f *.cmx *.o
+
+printenv:
+	@"$(COQBIN)coqtop" -config
+	@echo 'CAMLC =	$(CAMLC)'
+	@echo 'CAMLOPTC =	$(CAMLOPTC)'
+	@echo 'PP =	$(PP)'
+	@echo 'COQFLAGS =	$(COQFLAGS)'
+	@echo 'COQLIBINSTALL =	$(COQLIBINSTALL)'
+	@echo 'COQDOCINSTALL =	$(COQDOCINSTALL)'
+
+
+###################
+#                 #
+# Implicit rules. #
+#                 #
+###################
+
+%.cmi: %.mli
+	$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<
+
+%.mli.d: %.mli
+	$(OCAMLDEP) -slash $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
+
+%.cmo: %.ml4
+	$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<
+
+%.cmx: %.ml4
+	$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<
+
+%.ml4.d: %.ml4
+	$(COQDEP) -slash $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
+
+%.cmo: %.ml
+	$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<
+
+%.cmx: %.ml
+	$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<
+
+%.ml.d: %.ml
+	$(OCAMLDEP) -slash $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
+
+%.cmxs: %.cmxa
+	$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<
+
+%.cmxs: %.cmx
+	$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<
+
+%.vo %.glob: %.v
+	$(COQC) $(COQDEBUG) $(COQFLAGS) $*
+
+%.vi: %.v
+	$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
+
+%.g: %.v
+	$(GALLINA) $<
+
+%.tex: %.v
+	$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
+
+%.html: %.v %.glob
+	$(COQDOC) $(COQDOCFLAGS) -html $< -o $@
+
+%.g.tex: %.v
+	$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
+
+%.g.html: %.v %.glob
+	$(COQDOC) $(COQDOCFLAGS)  -html -g $< -o $@
+
+%.v.d: %.v
+	$(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
+
+%.v.beautified:
+	$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*
+
+# WARNING
+#
+# This Makefile has been automagically generated
+# Edit at your own risks !
+#
+# END OF WARNING
+
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
new file mode 100644
index 0000000..6c95ffe
--- /dev/null
+++ b/src/versions/standard/structures.ml
@@ -0,0 +1,47 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+open Entries
+
+
+(* Int63 *)
+let int63_modules = [["SMTCoq";"Int63Native"]]
+
+let mkInt : int -> Term.constr =
+  failwith "Not implemented yet"
+
+
+(* PArray *)
+let parray_modules = [["SMTCoq";"PArray"]]
+
+let max_array_size : int =
+  failwith "Not implemented yet"
+let mkArray : Term.types * Term.constr array -> Term.constr =
+  failwith "Not implemented yet"
+
+
+(* Differences between the two versions of Coq *)
+let dummy_loc = Util.dummy_loc
+
+let mkConst c =
+  { const_entry_body = c;
+    const_entry_type = None;
+    const_entry_secctx = None;
+    const_entry_opaque = false}
+
+let glob_term_CbvVm = Glob_term.CbvVm
+
+let error = Util.error