Numbers and bitwise functions.

 See NatInt/NZBits.v for the common axiomatization of bitwise functions
 over naturals / integers. Some specs aren't pretty, but easier to
 prove, see alternate statements in property functors {N,Z}Bits.
 Negative numbers are considered via the two's complement convention.

 We provide implementations for N (in Ndigits.v), for nat (quite dummy,
 just for completeness), for Z (new file Zdigits_def), for BigN
 (for the moment partly by converting to N, to be improved soon)
 and for BigZ.

 NOTA: For BigN.shiftl and BigN.shiftr, the two arguments are now in
 the reversed order (for consistency with the rest of the world):
 for instance BigN.shiftl 1 10 is 2^10.

 NOTA2: Zeven.Zdiv2 is _not_ doing (Zdiv _ 2), but rather (Zquot _ 2)
 on negative numbers. For the moment I've kept it intact, and have
 just added a Zdiv2' which is truly equivalent to (Zdiv _ 2).
 To reorganize someday ?

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13689 85f007b7-540e-0410-9357-904b9bb8a0f7

14 files changed, 1953 insertions, 256 deletions

diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index 82f0727467..09438628da 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-Require Export NZAxioms NZPow NZSqrt NZLog NZDiv NZGcd.
+Require Export Bool NZAxioms NZParity NZPow NZSqrt NZLog NZDiv NZGcd NZBits.
 
 (** From [NZ], we obtain natural numbers just by stating that [pred 0] == 0 *)
 
@@ -19,19 +19,8 @@ End NAxiom.
 Module Type NAxiomsMiniSig := NZOrdAxiomsSig <+ NAxiom.
 Module Type NAxiomsMiniSig' := NZOrdAxiomsSig' <+ NAxiom.
 
-
 (** Let's now add some more functions and their specification *)
 
-(** Parity functions *)
-
-Module Type Parity (Import N : NAxiomsMiniSig').
- Parameter Inline even odd : t -> bool.
- Definition Even n := exists m, n == 2*m.
- Definition Odd n := exists m, n == 2*m+1.
- Axiom even_spec : forall n, even n = true <-> Even n.
- Axiom odd_spec : forall n, odd n = true <-> Odd n.
-End Parity.
-
 (** Division Function : we reuse NZDiv.DivMod and NZDiv.NZDivCommon,
     and add to that a N-specific constraint. *)
 
@@ -39,17 +28,17 @@ Module Type NDivSpecific (Import N : NAxiomsMiniSig')(Import DM : DivMod' N).
  Axiom mod_upper_bound : forall a b, b ~= 0 -> a mod b < b.
 End NDivSpecific.
 
-(** For div mod gcd pow sqrt log2, the NZ axiomatizations are enough. *)
+(** For all other functions, the NZ axiomatizations are enough. *)
 
 (** We now group everything together. *)
 
-Module Type NAxiomsSig := NAxiomsMiniSig <+ HasCompare <+ Parity
-  <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2 <+ NZGcd.NZGcd
-  <+ NZDiv.NZDiv.
+Module Type NAxiomsSig := NAxiomsMiniSig <+ HasCompare <+ HasEqBool
+  <+ NZParity.NZParity <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2
+  <+ NZGcd.NZGcd <+ NZDiv.NZDiv <+ NZBits.NZBits.
 
-Module Type NAxiomsSig' := NAxiomsMiniSig' <+ HasCompare <+ Parity
-  <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2 <+ NZGcd.NZGcd'
-  <+ NZDiv.NZDiv'.
+Module Type NAxiomsSig' := NAxiomsMiniSig' <+ HasCompare <+ HasEqBool
+  <+ NZParity.NZParity <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2
+  <+ NZGcd.NZGcd' <+ NZDiv.NZDiv' <+ NZBits.NZBits'.
 
 
 (** It could also be interesting to have a constructive recursor function. *)
diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v
new file mode 100644
index 0000000000..2cb5bbc065
--- /dev/null
+++ b/theories/Numbers/Natural/Abstract/NBits.v
@@ -0,0 +1,1422 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import Bool NAxioms NSub NPow NDiv NParity NLog.
+
+(** Derived properties of bitwise operations *)
+
+Module Type NBitsProp
+ (Import A : NAxiomsSig')
+ (Import B : NSubProp A)
+ (Import C : NParityProp A B)
+ (Import D : NPowProp A B C)
+ (Import E : NDivProp A B)
+ (Import F : NLog2Prop A B C D).
+
+Include BoolEqualityFacts A.
+
+Ltac order_nz := try apply pow_nonzero; order'.
+Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz.
+
+(** Some properties of power and division *)
+
+Lemma pow_sub_r : forall a b c, a~=0 -> c<=b -> a^(b-c) == a^b / a^c.
+Proof.
+ intros a b c Ha H.
+ apply div_unique with 0.
+ generalize (pow_nonzero a c Ha) (le_0_l (a^c)); order'.
+ nzsimpl. now rewrite <- pow_add_r, add_comm, sub_add.
+Qed.
+
+Lemma pow_div_l : forall a b c, b~=0 -> a mod b == 0 ->
+ (a/b)^c == a^c / b^c.
+Proof.
+ intros a b c Hb H.
+ apply div_unique with 0.
+ generalize (pow_nonzero b c Hb) (le_0_l (b^c)); order'.
+ nzsimpl. rewrite <- pow_mul_l. apply pow_wd. now apply div_exact.
+ reflexivity.
+Qed.
+
+(** An injection from bits [true] and [false] to numbers 1 and 0.
+    We declare it as a (local) coercion for shorter statements. *)
+
+Definition b2n (b:bool) := if b then 1 else 0.
+Local Coercion b2n : bool >-> t.
+
+(** Alternative caracterisations of [testbit] *)
+
+Lemma testbit_spec' : forall a n, a.[n] == (a / 2^n) mod 2.
+Proof.
+ intros a n.
+ destruct (testbit_spec a n) as (l & h & (_,H) & EQ).
+ apply le_0_l.
+ fold (b2n a.[n]) in EQ.
+ apply mod_unique with h. destruct a.[n]; order'.
+ symmetry. apply div_unique with l; trivial.
+ now rewrite add_comm, mul_comm, (add_comm (2*h)).
+Qed.
+
+Lemma testbit_true : forall a n,
+ a.[n] = true <-> (a / 2^n) mod 2 == 1.
+Proof.
+ intros a n.
+ rewrite <- testbit_spec'; destruct a.[n]; split; simpl; now try order'.
+Qed.
+
+Lemma testbit_false : forall a n,
+ a.[n] = false <-> (a / 2^n) mod 2 == 0.
+Proof.
+ intros a n.
+ rewrite <- testbit_spec'; destruct a.[n]; split; simpl; now try order'.
+Qed.
+
+Lemma testbit_eqb : forall a n,
+ a.[n] = eqb ((a / 2^n) mod 2) 1.
+Proof.
+ intros a n.
+ apply eq_true_iff_eq. now rewrite testbit_true, eqb_eq.
+Qed.
+
+(** testbit is hence a morphism *)
+
+Instance testbit_wd : Proper (eq==>eq==>Logic.eq) testbit.
+Proof.
+ intros a a' Ha n n' Hn. now rewrite 2 testbit_eqb, Ha, Hn.
+Qed.
+
+(** Results about the injection [b2n] *)
+
+Lemma b2n_inj : forall (a0 b0:bool), a0 == b0 -> a0 = b0.
+Proof.
+ intros [|] [|]; simpl; trivial; order'.
+Qed.
+
+Lemma add_b2n_double_div2 : forall (a0:bool) a, (a0+2*a)/2 == a.
+Proof.
+ intros a0 a. rewrite mul_comm, div_add by order'.
+ now rewrite div_small, add_0_l by (destruct a0; order').
+Qed.
+
+Lemma add_b2n_double_bit0 : forall (a0:bool) a, (a0+2*a).[0] = a0.
+Proof.
+ intros a0 a. apply b2n_inj.
+ rewrite testbit_spec'. nzsimpl. rewrite mul_comm, mod_add by order'.
+ now rewrite mod_small by (destruct a0; order').
+Qed.
+
+Lemma b2n_div2 : forall (a0:bool), a0/2 == 0.
+Proof.
+ intros a0. rewrite <- (add_b2n_double_div2 a0 0). now nzsimpl.
+Qed.
+
+Lemma b2n_bit0 : forall (a0:bool), a0.[0] = a0.
+Proof.
+ intros a0. rewrite <- (add_b2n_double_bit0 a0 0) at 2. now nzsimpl.
+Qed.
+
+(** The initial specification of testbit is complete *)
+
+Lemma testbit_unique : forall a n (a0:bool) l h,
+ l<2^n -> a == l + (a0 + 2*h)*2^n -> a.[n] = a0.
+Proof.
+ intros a n a0 l h Hl EQ.
+ apply b2n_inj. rewrite testbit_spec' by trivial.
+ symmetry. apply mod_unique with h. destruct a0; simpl; order'.
+ symmetry. apply div_unique with l; trivial.
+ now rewrite add_comm, (add_comm _ a0), mul_comm.
+Qed.
+
+(** All bits of number 0 are 0 *)
+
+Lemma bits_0 : forall n, 0.[n] = false.
+Proof.
+ intros n. apply testbit_false. nzsimpl; order_nz.
+Qed.
+
+(** Various ways to refer to the lowest bit of a number *)
+
+Lemma bit0_mod : forall a, a.[0] == a mod 2.
+Proof.
+ intros a. rewrite testbit_spec'. now nzsimpl.
+Qed.
+
+Lemma bit0_eqb : forall a, a.[0] = eqb (a mod 2) 1.
+Proof.
+ intros a. rewrite testbit_eqb. now nzsimpl.
+Qed.
+
+Lemma bit0_odd : forall a, a.[0] = odd a.
+Proof.
+ intros. rewrite bit0_eqb.
+ apply eq_true_iff_eq. rewrite eqb_eq, odd_spec. split.
+ intros H. exists (a/2). rewrite <- H. apply div_mod. order'.
+ intros (b,H). rewrite H, add_comm, mul_comm, mod_add, mod_small; order'.
+Qed.
+
+(** Hence testing a bit is equivalent to shifting and testing parity *)
+
+Lemma testbit_odd : forall a n, a.[n] = odd (a>>n).
+Proof.
+ intros. now rewrite <- bit0_odd, shiftr_spec, add_0_l.
+Qed.
+
+(** [log2] gives the highest nonzero bit *)
+
+Lemma bit_log2 : forall a, a~=0 -> a.[log2 a] = true.
+Proof.
+ intros a Ha.
+ assert (Ha' : 0 < a) by (generalize (le_0_l a); order).
+ destruct (log2_spec_alt a Ha') as (r & EQ & (_,Hr)).
+ rewrite EQ at 1.
+ rewrite testbit_true, add_comm.
+ rewrite <- (mul_1_l (2^log2 a)) at 1.
+ rewrite div_add by order_nz.
+ rewrite div_small by trivial.
+ rewrite add_0_l. apply mod_small. order'.
+Qed.
+
+Lemma bits_above_log2 : forall a n, log2 a < n ->
+ a.[n] = false.
+Proof.
+ intros a n H.
+ rewrite testbit_false.
+ rewrite div_small. nzsimpl; order'.
+ apply log2_lt_cancel. rewrite log2_pow2; trivial using le_0_l.
+Qed.
+
+(** Hence the number of bits of [a] is [1+log2 a]
+    (see [Psize] and [Psize_pos]).
+*)
+
+(** Testing bits after division or multiplication by a power of two *)
+
+Lemma div2_bits : forall a n, (a/2).[n] = a.[S n].
+Proof.
+ intros. apply eq_true_iff_eq.
+ rewrite 2 testbit_true.
+ rewrite pow_succ_r by apply le_0_l.
+ now rewrite div_div by order_nz.
+Qed.
+
+Lemma div_pow2_bits : forall a n m, (a/2^n).[m] = a.[m+n].
+Proof.
+ intros a n. revert a. induct n.
+ intros a m. now nzsimpl.
+ intros n IH a m. nzsimpl; try apply le_0_l.
+ rewrite <- div_div by order_nz.
+ now rewrite IH, div2_bits.
+Qed.
+
+Lemma double_bits_succ : forall a n, (2*a).[S n] = a.[n].
+Proof.
+ intros. rewrite <- div2_bits. now rewrite mul_comm, div_mul by order'.
+Qed.
+
+Lemma mul_pow2_bits_add : forall a n m, (a*2^n).[m+n] = a.[m].
+Proof.
+ intros. rewrite <- div_pow2_bits. now rewrite div_mul by order_nz.
+Qed.
+
+Lemma mul_pow2_bits_high : forall a n m, n<=m -> (a*2^n).[m] = a.[m-n].
+Proof.
+ intros.
+ rewrite <- (sub_add n m) at 1 by order'.
+ now rewrite mul_pow2_bits_add.
+Qed.
+
+Lemma mul_pow2_bits_low : forall a n m, m<n -> (a*2^n).[m] = false.
+Proof.
+ intros. apply testbit_false.
+ rewrite <- (sub_add m n) by order'. rewrite pow_add_r, mul_assoc.
+ rewrite div_mul by order_nz.
+ rewrite <- (succ_pred (n-m)). rewrite pow_succ_r.
+ now rewrite (mul_comm 2), mul_assoc, mod_mul by order'.
+ apply lt_le_pred.
+ apply sub_gt in H. generalize (le_0_l (n-m)); order.
+ now apply sub_gt.
+Qed.
+
+(** Selecting the low part of a number can be done by a modulo *)
+
+Lemma mod_pow2_bits_high : forall a n m, n<=m ->
+ (a mod 2^n).[m] = false.
+Proof.
+ intros a n m H.
+ destruct (eq_0_gt_0_cases (a mod 2^n)) as [EQ|LT].
+ now rewrite EQ, bits_0.
+ apply bits_above_log2.
+ apply lt_le_trans with n; trivial.
+ apply log2_lt_pow2; trivial.
+ apply mod_upper_bound; order_nz.
+Qed.
+
+Lemma mod_pow2_bits_low : forall a n m, m<n ->
+ (a mod 2^n).[m] = a.[m].
+Proof.
+ intros a n m H.
+ rewrite testbit_eqb.
+ rewrite <- (mod_add _ (2^(P (n-m))*(a/2^n))) by order'.
+ rewrite <- div_add by order_nz.
+ rewrite (mul_comm _ 2), mul_assoc, <- pow_succ_r', succ_pred
+   by now apply sub_gt.
+ rewrite mul_comm, mul_assoc, <- pow_add_r, (add_comm m), sub_add
+   by order.
+ rewrite add_comm, <- div_mod by order_nz.
+ symmetry. apply testbit_eqb.
+Qed.
+
+(** We now prove that having the same bits implies equality.
+    For that we use a notion of equality over functional
+    streams of bits. *)
+
+Definition eqf (f g:t -> bool) := forall n:t, f n = g n.
+
+Instance eqf_equiv : Equivalence eqf.
+Proof.
+ split; congruence.
+Qed.
+
+Local Infix "===" := eqf (at level 70, no associativity).
+
+Instance testbit_eqf : Proper (eq==>eqf) testbit.
+Proof.
+ intros a a' Ha n. now rewrite Ha.
+Qed.
+
+(** Only zero corresponds to the always-false stream. *)
+
+Lemma bits_inj_0 :
+ forall a, (forall n, a.[n] = false) -> a == 0.
+Proof.
+ intros a H. destruct (eq_decidable a 0) as [EQ|NEQ]; trivial.
+ apply bit_log2 in NEQ. now rewrite H in NEQ.
+Qed.
+
+(** If two numbers produce the same stream of bits, they are equal. *)
+
+Lemma bits_inj : forall a b, testbit a === testbit b -> a == b.
+Proof.
+ intros a. pattern a.
+ apply strong_right_induction with 0;[solve_predicate_wd|clear a|apply le_0_l].
+ intros a _ IH b H.
+ destruct (eq_0_gt_0_cases a) as [EQ|LT].
+ rewrite EQ in H |- *. symmetry. apply bits_inj_0.
+ intros n. now rewrite <- H, bits_0.
+ rewrite (div_mod a 2), (div_mod b 2) by order'.
+ apply add_wd; [ | now rewrite <- 2 bit0_mod, H].
+ apply mul_wd. reflexivity.
+ apply IH; trivial using le_0_l.
+ apply div_lt; order'.
+ intro n. rewrite 2 div2_bits. apply H.
+Qed.
+
+Lemma bits_inj_iff : forall a b, testbit a === testbit b <-> a == b.
+Proof.
+ split. apply bits_inj. intros EQ; now rewrite EQ.
+Qed.
+
+Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise.
+
+Ltac bitwise := apply bits_inj; intros ?m; autorewrite with bitwise.
+
+(** The streams of bits that correspond to a natural numbers are
+  exactly the ones that are always 0 after some point *)
+
+Lemma are_bits : forall (f:t->bool), Proper (eq==>Logic.eq) f ->
+ ((exists n, f === testbit n) <->
+  (exists k, forall m, k<=m -> f m = false)).
+Proof.
+ intros f Hf. split.
+ intros (a,H).
+  exists (S (log2 a)). intros m Hm. apply le_succ_l in Hm.
+  rewrite H, bits_above_log2; trivial using lt_succ_diag_r.
+ intros (k,Hk).
+  revert f Hf Hk. induct k.
+  intros f Hf H0.
+  exists 0. intros m. rewrite bits_0, H0; trivial. apply le_0_l.
+  intros k IH f Hf Hk.
+  destruct (IH (fun m => f (S m))) as (n, Hn).
+  solve_predicate_wd.
+  intros m Hm. apply Hk. now rewrite <- succ_le_mono.
+  exists (f 0 + 2*n). intros m.
+  destruct (zero_or_succ m) as [Hm|(m', Hm)]; rewrite Hm.
+  symmetry. apply add_b2n_double_bit0.
+  rewrite Hn, <- div2_bits.
+  rewrite mul_comm, div_add, b2n_div2, add_0_l; trivial. order'.
+Qed.
+
+(** Properties of shifts *)
+
+Lemma shiftr_spec' : forall a n m, (a >> n).[m] = a.[m+n].
+Proof.
+ intros. apply shiftr_spec. apply le_0_l.
+Qed.
+
+Lemma shiftl_spec_high' : forall a n m, n<=m -> (a << n).[m] = a.[m-n].
+Proof.
+ intros. apply shiftl_spec_high; trivial. apply le_0_l.
+Qed.
+
+Lemma shiftr_div_pow2 : forall a n, a >> n == a / 2^n.
+Proof.
+ intros. bitwise. rewrite shiftr_spec'.
+ symmetry. apply div_pow2_bits.
+Qed.
+
+Lemma shiftl_mul_pow2 : forall a n, a << n == a * 2^n.
+Proof.
+ intros. bitwise.
+ destruct (le_gt_cases n m) as [H|H].
+ now rewrite shiftl_spec_high', mul_pow2_bits_high.
+ now rewrite shiftl_spec_low, mul_pow2_bits_low.
+Qed.
+
+Lemma shiftl_spec_alt : forall a n m, (a << n).[m+n] = a.[m].
+Proof.
+ intros. now rewrite shiftl_mul_pow2, mul_pow2_bits_add.
+Qed.
+
+Instance shiftr_wd : Proper (eq==>eq==>eq) shiftr.
+Proof.
+ intros a a' Ha b b' Hb. now rewrite 2 shiftr_div_pow2, Ha, Hb.
+Qed.
+
+Instance shiftl_wd : Proper (eq==>eq==>eq) shiftl.
+Proof.
+ intros a a' Ha b b' Hb. now rewrite 2 shiftl_mul_pow2, Ha, Hb.
+Qed.
+
+Lemma shiftl_shiftl : forall a n m,
+ (a << n) << m == a << (n+m).
+Proof.
+ intros. now rewrite !shiftl_mul_pow2, pow_add_r, mul_assoc.
+Qed.
+
+Lemma shiftr_shiftr : forall a n m,
+ (a >> n) >> m == a >> (n+m).
+Proof.
+ intros.
+ now rewrite !shiftr_div_pow2, pow_add_r, div_div by order_nz.
+Qed.
+
+Lemma shiftr_shiftl_l : forall a n m, m<=n ->
+ (a << n) >> m == a << (n-m).
+Proof.
+ intros.
+ rewrite shiftr_div_pow2, !shiftl_mul_pow2.
+ rewrite <- (sub_add m n) at 1 by trivial.
+ now rewrite pow_add_r, mul_assoc, div_mul by order_nz.
+Qed.
+
+Lemma shiftr_shiftl_r : forall a n m, n<=m ->
+ (a << n) >> m == a >> (m-n).
+Proof.
+ intros.
+ rewrite !shiftr_div_pow2, shiftl_mul_pow2.
+ rewrite <- (sub_add n m) at 1 by trivial.
+ rewrite pow_add_r, (mul_comm (2^(m-n))).
+ now rewrite <- div_div, div_mul by order_nz.
+Qed.
+
+(** shifts and constants *)
+
+Lemma shiftl_1_l : forall n, 1 << n == 2^n.
+Proof.
+ intros. now rewrite shiftl_mul_pow2, mul_1_l.
+Qed.
+
+Lemma shiftl_0_r : forall a, a << 0 == a.
+Proof.
+ intros. rewrite shiftl_mul_pow2. now nzsimpl.
+Qed.
+
+Lemma shiftr_0_r : forall a, a >> 0 == a.
+Proof.
+ intros. rewrite shiftr_div_pow2. now nzsimpl.
+Qed.
+
+Lemma shiftl_0_l : forall n, 0 << n == 0.
+Proof.
+ intros. rewrite shiftl_mul_pow2. now nzsimpl.
+Qed.
+
+Lemma shiftr_0_l : forall n, 0 >> n == 0.
+Proof.
+ intros. rewrite shiftr_div_pow2. nzsimpl; order_nz.
+Qed.
+
+Lemma shiftl_eq_0_iff : forall a n, a << n == 0 <-> a == 0.
+Proof.
+ intros a n. rewrite shiftl_mul_pow2. rewrite eq_mul_0. split.
+ intros [H | H]; trivial. contradict H; order_nz.
+ intros H. now left.
+Qed.
+
+Lemma shiftr_eq_0_iff : forall a n,
+ a >> n == 0 <-> a==0 \/ (0<a /\ log2 a < n).
+Proof.
+ intros a n.
+ rewrite shiftr_div_pow2, div_small_iff by order_nz.
+ destruct (eq_0_gt_0_cases a) as [EQ|LT].
+ rewrite EQ. split. now left. intros _.
+  assert (H : 2~=0) by order'.
+  generalize (pow_nonzero 2 n H) (le_0_l (2^n)); order.
+ rewrite log2_lt_pow2; trivial.
+ split. right; split; trivial. intros [H|[_ H]]; now order.
+Qed.
+
+Lemma shiftr_eq_0 : forall a n, log2 a < n -> a >> n == 0.
+Proof.
+ intros a n H. rewrite shiftr_eq_0_iff.
+ destruct (eq_0_gt_0_cases a) as [EQ|LT]. now left. right; now split.
+Qed.
+
+(** Properties of [div2]. *)
+
+Lemma div2_div : forall a, div2 a == a/2.
+Proof.
+ intros. rewrite div2_spec, shiftr_div_pow2. now nzsimpl.
+Qed.
+
+Instance div2_wd : Proper (eq==>eq) div2.
+Proof.
+ intros a a' Ha. now rewrite 2 div2_div, Ha.
+Qed.
+
+Lemma div2_odd : forall a, a == 2*(div2 a) + odd a.
+Proof.
+ intros a. rewrite div2_div, <- bit0_odd, bit0_mod.
+ apply div_mod. order'.
+Qed.
+
+(** Properties of [lxor] and others, directly deduced
+    from properties of [xorb] and others. *)
+
+Instance lxor_wd : Proper (eq ==> eq ==> eq) lxor.
+Proof.
+ intros a a' Ha b b' Hb. bitwise. now rewrite Ha, Hb.
+Qed.
+
+Instance land_wd : Proper (eq ==> eq ==> eq) land.
+Proof.
+ intros a a' Ha b b' Hb. bitwise. now rewrite Ha, Hb.
+Qed.
+
+Instance lor_wd : Proper (eq ==> eq ==> eq) lor.
+Proof.
+ intros a a' Ha b b' Hb. bitwise. now rewrite Ha, Hb.
+Qed.
+
+Instance ldiff_wd : Proper (eq ==> eq ==> eq) ldiff.
+Proof.
+ intros a a' Ha b b' Hb. bitwise. now rewrite Ha, Hb.
+Qed.
+
+Lemma lxor_eq : forall a a', lxor a a' == 0 -> a == a'.
+Proof.
+ intros a a' H. bitwise. apply xorb_eq.
+ now rewrite <- lxor_spec, H, bits_0.
+Qed.
+
+Lemma lxor_nilpotent : forall a, lxor a a == 0.
+Proof.
+ intros. bitwise. apply xorb_nilpotent.
+Qed.
+
+Lemma lxor_eq_0_iff : forall a a', lxor a a' == 0 <-> a == a'.
+Proof.
+ split. apply lxor_eq. intros EQ; rewrite EQ; apply lxor_nilpotent.
+Qed.
+
+Lemma lxor_0_l : forall a, lxor 0 a == a.
+Proof.
+ intros. bitwise. apply xorb_false_l.
+Qed.
+
+Lemma lxor_0_r : forall a, lxor a 0 == a.
+Proof.
+ intros. bitwise. apply xorb_false_r.
+Qed.
+
+Lemma lxor_comm : forall a b, lxor a b == lxor b a.
+Proof.
+ intros. bitwise. apply xorb_comm.
+Qed.
+
+Lemma lxor_assoc :
+ forall a b c, lxor (lxor a b) c == lxor a (lxor b c).
+Proof.
+ intros. bitwise. apply xorb_assoc.
+Qed.
+
+Lemma lor_0_l : forall a, lor 0 a == a.
+Proof.
+ intros. bitwise. trivial.
+Qed.
+
+Lemma lor_0_r : forall a, lor a 0 == a.
+Proof.
+ intros. bitwise. apply orb_false_r.
+Qed.
+
+Lemma lor_comm : forall a b, lor a b == lor b a.
+Proof.
+ intros. bitwise. apply orb_comm.
+Qed.
+
+Lemma lor_assoc :
+ forall a b c, lor a (lor b c) == lor (lor a b) c.
+Proof.
+ intros. bitwise. apply orb_assoc.
+Qed.
+
+Lemma lor_diag : forall a, lor a a == a.
+Proof.
+ intros. bitwise. apply orb_diag.
+Qed.
+
+Lemma lor_eq_0_l : forall a b, lor a b == 0 -> a == 0.
+Proof.
+ intros a b H. bitwise.
+ apply (orb_false_iff a.[m] b.[m]).
+ now rewrite <- lor_spec, H, bits_0.
+Qed.
+
+Lemma lor_eq_0_iff : forall a b, lor a b == 0 <-> a == 0 /\ b == 0.
+Proof.
+ intros a b. split.
+ split. now apply lor_eq_0_l in H.
+ rewrite lor_comm in H. now apply lor_eq_0_l in H.
+ intros (EQ,EQ'). now rewrite EQ, lor_0_l.
+Qed.
+
+Lemma land_0_l : forall a, land 0 a == 0.
+Proof.
+ intros. bitwise. trivial.
+Qed.
+
+Lemma land_0_r : forall a, land a 0 == 0.
+Proof.
+ intros. bitwise. apply andb_false_r.
+Qed.
+
+Lemma land_comm : forall a b, land a b == land b a.
+Proof.
+ intros. bitwise. apply andb_comm.
+Qed.
+
+Lemma land_assoc :
+ forall a b c, land a (land b c) == land (land a b) c.
+Proof.
+ intros. bitwise. apply andb_assoc.
+Qed.
+
+Lemma land_diag : forall a, land a a == a.
+Proof.
+ intros. bitwise. apply andb_diag.
+Qed.
+
+Lemma ldiff_0_l : forall a, ldiff 0 a == 0.
+Proof.
+ intros. bitwise. trivial.
+Qed.
+
+Lemma ldiff_0_r : forall a, ldiff a 0 == a.
+Proof.
+ intros. bitwise. now rewrite andb_true_r.
+Qed.
+
+Lemma ldiff_diag : forall a, ldiff a a == 0.
+Proof.
+ intros. bitwise. apply andb_negb_r.
+Qed.
+
+Lemma lor_land_distr_l : forall a b c,
+ lor (land a b) c == land (lor a c) (lor b c).
+Proof.
+ intros. bitwise. apply orb_andb_distrib_l.
+Qed.
+
+Lemma lor_land_distr_r : forall a b c,
+ lor a (land b c) == land (lor a b) (lor a c).
+Proof.
+ intros. bitwise. apply orb_andb_distrib_r.
+Qed.
+
+Lemma land_lor_distr_l : forall a b c,
+ land (lor a b) c == lor (land a c) (land b c).
+Proof.
+ intros. bitwise. apply andb_orb_distrib_l.
+Qed.
+
+Lemma land_lor_distr_r : forall a b c,
+ land a (lor b c) == lor (land a b) (land a c).
+Proof.
+ intros. bitwise. apply andb_orb_distrib_r.
+Qed.
+
+Lemma ldiff_ldiff_l : forall a b c,
+ ldiff (ldiff a b) c == ldiff a (lor b c).
+Proof.
+ intros. bitwise. now rewrite negb_orb, andb_assoc.
+Qed.
+
+Lemma lor_ldiff_and : forall a b,
+ lor (ldiff a b) (land a b) == a.
+Proof.
+ intros. bitwise.
+ now rewrite <- andb_orb_distrib_r, orb_comm, orb_negb_r, andb_true_r.
+Qed.
+
+Lemma land_ldiff : forall a b,
+ land (ldiff a b) b == 0.
+Proof.
+ intros. bitwise.
+ now rewrite <-andb_assoc, (andb_comm (negb _)), andb_negb_r, andb_false_r.
+Qed.
+
+(** Properties of [setbit] and [clearbit] *)
+
+Definition setbit a n := lor a (1<<n).
+Definition clearbit a n := ldiff a (1<<n).
+
+Lemma setbit_spec' : forall a n, setbit a n == lor a (2^n).
+Proof.
+ intros. unfold setbit. now rewrite shiftl_1_l.
+Qed.
+
+Lemma clearbit_spec' : forall a n, clearbit a n == ldiff a (2^n).
+Proof.
+ intros. unfold clearbit. now rewrite shiftl_1_l.
+Qed.
+
+Instance setbit_wd : Proper (eq==>eq==>eq) setbit.
+Proof.
+ intros a a' Ha n n' Hn. unfold setbit. now rewrite Ha, Hn.
+Qed.
+
+Instance clearbit_wd : Proper (eq==>eq==>eq) clearbit.
+Proof.
+ intros a a' Ha n n' Hn. unfold clearbit. now rewrite Ha, Hn.
+Qed.
+
+Lemma pow2_bits_true : forall n, (2^n).[n] = true.
+Proof.
+ intros. rewrite <- (mul_1_l (2^n)). rewrite <- (add_0_l n) at 2.
+ now rewrite mul_pow2_bits_add, bit0_odd, odd_1.
+Qed.
+
+Lemma pow2_bits_false : forall n m, n~=m -> (2^n).[m] = false.
+Proof.
+ intros.
+ rewrite <- (mul_1_l (2^n)).
+ destruct (le_gt_cases n m).
+ rewrite mul_pow2_bits_high; trivial.
+ rewrite <- (succ_pred (m-n)) by (apply sub_gt; order).
+ now rewrite <- div2_bits, div_small, bits_0 by order'.
+ rewrite mul_pow2_bits_low; trivial.
+Qed.
+
+Lemma pow2_bits_eqb : forall n m, (2^n).[m] = eqb n m.
+Proof.
+ intros. apply eq_true_iff_eq. rewrite eqb_eq. split.
+ destruct (eq_decidable n m) as [H|H]. trivial.
+ now rewrite (pow2_bits_false _ _ H).
+ intros EQ. rewrite EQ. apply pow2_bits_true.
+Qed.
+
+Lemma setbit_eqb : forall a n m,
+ (setbit a n).[m] = eqb n m || a.[m].
+Proof.
+ intros. now rewrite setbit_spec', lor_spec, pow2_bits_eqb, orb_comm.
+Qed.
+
+Lemma setbit_iff : forall a n m,
+ (setbit a n).[m] = true <-> n==m \/ a.[m] = true.
+Proof.
+ intros. now rewrite setbit_eqb, orb_true_iff, eqb_eq.
+Qed.
+
+Lemma setbit_eq : forall a n, (setbit a n).[n] = true.
+Proof.
+ intros. apply setbit_iff. now left.
+Qed.
+
+Lemma setbit_neq : forall a n m, n~=m ->
+ (setbit a n).[m] = a.[m].
+Proof.
+ intros a n m H. rewrite setbit_eqb.
+ rewrite <- eqb_eq in H. apply not_true_is_false in H. now rewrite H.
+Qed.
+
+Lemma clearbit_eqb : forall a n m,
+ (clearbit a n).[m] = a.[m] && negb (eqb n m).
+Proof.
+ intros. now rewrite clearbit_spec', ldiff_spec, pow2_bits_eqb.
+Qed.
+
+Lemma clearbit_iff : forall a n m,
+ (clearbit a n).[m] = true <-> a.[m] = true /\ n~=m.
+Proof.
+ intros. rewrite clearbit_eqb, andb_true_iff, <- eqb_eq.
+ now rewrite negb_true_iff, not_true_iff_false.
+Qed.
+
+Lemma clearbit_eq : forall a n, (clearbit a n).[n] = false.
+Proof.
+ intros. rewrite clearbit_eqb, (proj2 (eqb_eq _ _) (eq_refl n)).
+ apply andb_false_r.
+Qed.
+
+Lemma clearbit_neq : forall a n m, n~=m ->
+ (clearbit a n).[m] = a.[m].
+Proof.
+ intros a n m H. rewrite clearbit_eqb.
+ rewrite <- eqb_eq in H. apply not_true_is_false in H. rewrite H.
+ apply andb_true_r.
+Qed.
+
+(** Shifts of bitwise operations *)
+
+Lemma shiftl_lxor : forall a b n,
+ (lxor a b) << n == lxor (a << n) (b << n).
+Proof.
+ intros. bitwise.
+ destruct (le_gt_cases n m).
+ now rewrite !shiftl_spec_high', lxor_spec.
+ now rewrite !shiftl_spec_low.
+Qed.
+
+Lemma shiftr_lxor : forall a b n,
+ (lxor a b) >> n == lxor (a >> n) (b >> n).
+Proof.
+ intros. bitwise. now rewrite !shiftr_spec', lxor_spec.
+Qed.
+
+Lemma shiftl_land : forall a b n,
+ (land a b) << n == land (a << n) (b << n).
+Proof.
+ intros. bitwise.
+ destruct (le_gt_cases n m).
+ now rewrite !shiftl_spec_high', land_spec.
+ now rewrite !shiftl_spec_low.
+Qed.
+
+Lemma shiftr_land : forall a b n,
+ (land a b) >> n == land (a >> n) (b >> n).
+Proof.
+ intros. bitwise. now rewrite !shiftr_spec', land_spec.
+Qed.
+
+Lemma shiftl_lor : forall a b n,
+ (lor a b) << n == lor (a << n) (b << n).
+Proof.
+ intros. bitwise.
+ destruct (le_gt_cases n m).
+ now rewrite !shiftl_spec_high', lor_spec.
+ now rewrite !shiftl_spec_low.
+Qed.
+
+Lemma shiftr_lor : forall a b n,
+ (lor a b) >> n == lor (a >> n) (b >> n).
+Proof.
+ intros. bitwise. now rewrite !shiftr_spec', lor_spec.
+Qed.
+
+Lemma shiftl_ldiff : forall a b n,
+ (ldiff a b) << n == ldiff (a << n) (b << n).
+Proof.
+ intros. bitwise.
+ destruct (le_gt_cases n m).
+ now rewrite !shiftl_spec_high', ldiff_spec.
+ now rewrite !shiftl_spec_low.
+Qed.
+
+Lemma shiftr_ldiff : forall a b n,
+ (ldiff a b) >> n == ldiff (a >> n) (b >> n).
+Proof.
+ intros. bitwise. now rewrite !shiftr_spec', ldiff_spec.
+Qed.
+
+(** We cannot have a function complementing all bits of a number,
+    otherwise it would have an infinity of bit 1. Nonetheless,
+    we can design a bounded complement *)
+
+Definition ones n := P (1 << n).
+
+Definition lnot a n := lxor a (ones n).
+
+Instance ones_wd : Proper (eq==>eq) ones.
+Proof. intros a a' Ha; unfold ones; now rewrite Ha. Qed.
+
+Instance lnot_wd : Proper (eq==>eq==>eq) lnot.
+Proof. intros a a' Ha n n' Hn; unfold lnot; now rewrite Ha, Hn. Qed.
+
+Lemma ones_equiv : forall n, ones n == P (2^n).
+Proof.
+ intros; unfold ones; now rewrite shiftl_1_l.
+Qed.
+
+Lemma ones_add : forall n m, ones (m+n) == 2^m * ones n + ones m.
+Proof.
+ intros n m. rewrite !ones_equiv.
+ rewrite <- !sub_1_r, mul_sub_distr_l, mul_1_r, <- pow_add_r.
+ rewrite add_sub_assoc, sub_add. reflexivity.
+ apply pow_le_mono_r. order'.
+ rewrite <- (add_0_r m) at 1. apply add_le_mono_l, le_0_l.
+ rewrite <- (pow_0_r 2). apply pow_le_mono_r. order'. apply le_0_l.
+Qed.
+
+Lemma ones_div_pow2 : forall n m, m<=n -> ones n / 2^m == ones (n-m).
+Proof.
+ intros n m H. symmetry. apply div_unique with (ones m).
+ rewrite ones_equiv.
+ apply le_succ_l. rewrite succ_pred; order_nz.
+ rewrite <- (sub_add m n H) at 1. rewrite (add_comm _ m).
+ apply ones_add.
+Qed.
+
+Lemma ones_mod_pow2 : forall n m, m<=n -> (ones n) mod (2^m) == ones m.
+Proof.
+ intros n m H. symmetry. apply mod_unique with (ones (n-m)).
+ rewrite ones_equiv.
+ apply le_succ_l. rewrite succ_pred; order_nz.
+ rewrite <- (sub_add m n H) at 1. rewrite (add_comm _ m).
+ apply ones_add.
+Qed.
+
+Lemma ones_spec_low : forall n m, m<n -> (ones n).[m] = true.
+Proof.
+ intros. apply testbit_true. rewrite ones_div_pow2 by order.
+ rewrite <- (pow_1_r 2). rewrite ones_mod_pow2.
+ rewrite ones_equiv. now nzsimpl'.
+ apply le_add_le_sub_r. nzsimpl. now apply le_succ_l.
+Qed.
+
+Lemma ones_spec_high : forall n m, n<=m -> (ones n).[m] = false.
+Proof.
+ intros.
+ destruct (eq_0_gt_0_cases n) as [EQ|LT]; rewrite ones_equiv.
+ now rewrite EQ, pow_0_r, one_succ, pred_succ, bits_0.
+ apply bits_above_log2.
+ rewrite log2_pred_pow2; trivial. rewrite <-le_succ_l, succ_pred; order.
+Qed.
+
+Lemma ones_spec_iff : forall n m, (ones n).[m] = true <-> m<n.
+Proof.
+ intros. split. intros H.
+ apply lt_nge. intro H'. apply ones_spec_high in H'.
+ rewrite H in H'; discriminate.
+ apply ones_spec_low.
+Qed.
+
+Lemma lnot_spec_low : forall a n m, m<n ->
+ (lnot a n).[m] = negb a.[m].
+Proof.
+ intros. unfold lnot. now rewrite lxor_spec, ones_spec_low.
+Qed.
+
+Lemma lnot_spec_high : forall a n m, n<=m ->
+ (lnot a n).[m] = a.[m].
+Proof.
+ intros. unfold lnot. now rewrite lxor_spec, ones_spec_high, xorb_false_r.
+Qed.
+
+Lemma lnot_involutive : forall a n, lnot (lnot a n) n == a.
+Proof.
+ intros a n. bitwise.
+ destruct (le_gt_cases n m).
+ now rewrite 2 lnot_spec_high.
+ now rewrite 2 lnot_spec_low, negb_involutive.
+Qed.
+
+Lemma lnot_0_l : forall n, lnot 0 n == ones n.
+Proof.
+ intros. unfold lnot. apply lxor_0_l.
+Qed.
+
+Lemma lnot_ones : forall n, lnot (ones n) n == 0.
+Proof.
+ intros. unfold lnot. apply lxor_nilpotent.
+Qed.
+
+(** Bounded complement and other operations *)
+
+Lemma lor_ones_low : forall a n, log2 a < n ->
+ lor a (ones n) == ones n.
+Proof.
+ intros a n H. bitwise. destruct (le_gt_cases n m).
+ rewrite ones_spec_high, bits_above_log2; trivial.
+ now apply lt_le_trans with n.
+ now rewrite ones_spec_low, orb_true_r.
+Qed.
+
+Lemma land_ones : forall a n, land a (ones n) == a mod 2^n.
+Proof.
+ intros a n. bitwise. destruct (le_gt_cases n m).
+ now rewrite ones_spec_high, mod_pow2_bits_high, andb_false_r.
+ now rewrite ones_spec_low, mod_pow2_bits_low, andb_true_r.
+Qed.
+
+Lemma land_ones_low : forall a n, log2 a < n ->
+ land a (ones n) == a.
+Proof.
+ intros; rewrite land_ones. apply mod_small.
+ apply log2_lt_cancel. rewrite log2_pow2; trivial using le_0_l.
+Qed.
+
+Lemma ldiff_ones_r : forall a n,
+ ldiff a (ones n) == (a >> n) << n.
+Proof.
+ intros a n. bitwise. destruct (le_gt_cases n m).
+ rewrite ones_spec_high, shiftl_spec_high', shiftr_spec'; trivial.
+ rewrite sub_add; trivial. apply andb_true_r.
+ now rewrite ones_spec_low, shiftl_spec_low, andb_false_r.
+Qed.
+
+Lemma ldiff_ones_r_low : forall a n, log2 a < n ->
+ ldiff a (ones n) == 0.
+Proof.
+ intros a n H. bitwise. destruct (le_gt_cases n m).
+ rewrite ones_spec_high, bits_above_log2; trivial.
+ now apply lt_le_trans with n.
+ now rewrite ones_spec_low, andb_false_r.
+Qed.
+
+Lemma ldiff_ones_l_low : forall a n, log2 a < n ->
+ ldiff (ones n) a == lnot a n.
+Proof.
+ intros a n H. bitwise. destruct (le_gt_cases n m).
+ rewrite ones_spec_high, lnot_spec_high, bits_above_log2; trivial.
+ now apply lt_le_trans with n.
+ now rewrite ones_spec_low, lnot_spec_low.
+Qed.
+
+Lemma lor_lnot_diag : forall a n,
+ lor a (lnot a n) == lor a (ones n).
+Proof.
+ intros a n. bitwise.
+ destruct (le_gt_cases n m).
+ rewrite lnot_spec_high, ones_spec_high; trivial. now destruct a.[m].
+ rewrite lnot_spec_low, ones_spec_low; trivial. now destruct a.[m].
+Qed.
+
+Lemma lor_lnot_diag_low : forall a n, log2 a < n ->
+ lor a (lnot a n) == ones n.
+Proof.
+ intros a n H. now rewrite lor_lnot_diag, lor_ones_low.
+Qed.
+
+Lemma land_lnot_diag : forall a n,
+ land a (lnot a n) == ldiff a (ones n).
+Proof.
+ intros a n. bitwise.
+ destruct (le_gt_cases n m).
+ rewrite lnot_spec_high, ones_spec_high; trivial. now destruct a.[m].
+ rewrite lnot_spec_low, ones_spec_low; trivial. now destruct a.[m].
+Qed.
+
+Lemma land_lnot_diag_low : forall a n, log2 a < n ->
+ land a (lnot a n) == 0.
+Proof.
+ intros. now rewrite land_lnot_diag, ldiff_ones_r_low.
+Qed.
+
+Lemma lnot_lor_low : forall a b n, log2 a < n -> log2 b < n ->
+ lnot (lor a b) n == land (lnot a n) (lnot b n).
+Proof.
+ intros a b n Ha Hb. bitwise. destruct (le_gt_cases n m).
+ rewrite !lnot_spec_high, lor_spec, !bits_above_log2; trivial.
+ now apply lt_le_trans with n.
+ now apply lt_le_trans with n.
+ now rewrite !lnot_spec_low, lor_spec, negb_orb.
+Qed.
+
+Lemma lnot_land_low : forall a b n, log2 a < n -> log2 b < n ->
+ lnot (land a b) n == lor (lnot a n) (lnot b n).
+Proof.
+ intros a b n Ha Hb. bitwise. destruct (le_gt_cases n m).
+ rewrite !lnot_spec_high, land_spec, !bits_above_log2; trivial.
+ now apply lt_le_trans with n.
+ now apply lt_le_trans with n.
+ now rewrite !lnot_spec_low, land_spec, negb_andb.
+Qed.
+
+Lemma ldiff_land_low : forall a b n, log2 a < n ->
+ ldiff a b == land a (lnot b n).
+Proof.
+ intros a b n Ha. bitwise. destruct (le_gt_cases n m).
+ rewrite (bits_above_log2 a m). trivial.
+ now apply lt_le_trans with n.
+ rewrite !lnot_spec_low; trivial.
+Qed.
+
+Lemma lnot_ldiff_low : forall a b n, log2 a < n -> log2 b < n ->
+ lnot (ldiff a b) n == lor (lnot a n) b.
+Proof.
+ intros a b n Ha Hb. bitwise. destruct (le_gt_cases n m).
+ rewrite !lnot_spec_high, ldiff_spec, !bits_above_log2; trivial.
+ now apply lt_le_trans with n.
+ now apply lt_le_trans with n.
+ now rewrite !lnot_spec_low, ldiff_spec, negb_andb, negb_involutive.
+Qed.
+
+Lemma lxor_lnot_lnot : forall a b n,
+ lxor (lnot a n) (lnot b n) == lxor a b.
+Proof.
+ intros a b n. bitwise. destruct (le_gt_cases n m).
+ rewrite !lnot_spec_high; trivial.
+ rewrite !lnot_spec_low, xorb_negb_negb; trivial.
+Qed.
+
+Lemma lnot_lxor_l : forall a b n,
+ lnot (lxor a b) n == lxor (lnot a n) b.
+Proof.
+ intros a b n. bitwise. destruct (le_gt_cases n m).
+ rewrite !lnot_spec_high, lxor_spec; trivial.
+ rewrite !lnot_spec_low, lxor_spec, negb_xorb_l; trivial.
+Qed.
+
+Lemma lnot_lxor_r : forall a b n,
+ lnot (lxor a b) n == lxor a (lnot b n).
+Proof.
+ intros a b n. bitwise. destruct (le_gt_cases n m).
+ rewrite !lnot_spec_high, lxor_spec; trivial.
+ rewrite !lnot_spec_low, lxor_spec, negb_xorb_r; trivial.
+Qed.
+
+Lemma lxor_lor : forall a b, land a b == 0 ->
+ lxor a b == lor a b.
+Proof.
+ intros a b H. bitwise.
+ assert (a.[m] && b.[m] = false)
+   by now rewrite <- land_spec, H, bits_0.
+ now destruct a.[m], b.[m].
+Qed.
+
+(** Bitwise operations and log2 *)
+
+Lemma log2_bits_unique : forall a n,
+ a.[n] = true ->
+ (forall m, n<m -> a.[m] = false) ->
+ log2 a == n.
+Proof.
+ intros a n H H'.
+ destruct (eq_0_gt_0_cases a) as [Ha|Ha].
+ now rewrite Ha, bits_0 in H.
+ apply le_antisymm; apply le_ngt; intros LT.
+ specialize (H' _ LT). now rewrite bit_log2 in H' by order.
+ now rewrite bits_above_log2 in H by order.
+Qed.
+
+Lemma log2_shiftr : forall a n, log2 (a >> n) == log2 a - n.
+Proof.
+ intros a n.
+ destruct (eq_0_gt_0_cases a) as [Ha|Ha].
+ now rewrite Ha, shiftr_0_l, log2_nonpos, sub_0_l by order.
+ destruct (lt_ge_cases (log2 a) n).
+ rewrite shiftr_eq_0, log2_nonpos by order.
+ symmetry. rewrite sub_0_le; order.
+ apply log2_bits_unique.
+ now rewrite shiftr_spec', sub_add, bit_log2 by order.
+ intros m Hm.
+ rewrite shiftr_spec'; trivial. apply bits_above_log2; try order.
+ now apply lt_sub_lt_add_r.
+Qed.
+
+Lemma log2_shiftl : forall a n, a~=0 -> log2 (a << n) == log2 a + n.
+Proof.
+ intros a n Ha.
+ rewrite shiftl_mul_pow2, add_comm by trivial.
+ apply log2_mul_pow2. generalize (le_0_l a); order. apply le_0_l.
+Qed.
+
+Lemma log2_lor : forall a b,
+ log2 (lor a b) == max (log2 a) (log2 b).
+Proof.
+ assert (AUX : forall a b, a<=b -> log2 (lor a b) == log2 b).
+  intros a b H.
+  destruct (eq_0_gt_0_cases a) as [Ha|Ha]. now rewrite Ha, lor_0_l.
+  apply log2_bits_unique.
+  now rewrite lor_spec, bit_log2, orb_true_r by order.
+  intros m Hm. assert (H' := log2_le_mono _ _ H).
+  now rewrite lor_spec, 2 bits_above_log2 by order.
+ (* main *)
+ intros a b. destruct (le_ge_cases a b) as [H|H].
+ rewrite max_r by now apply log2_le_mono.
+ now apply AUX.
+ rewrite max_l by now apply log2_le_mono.
+ rewrite lor_comm. now apply AUX.
+Qed.
+
+Lemma log2_land : forall a b,
+ log2 (land a b) <= min (log2 a) (log2 b).
+Proof.
+ assert (AUX : forall a b, a<=b -> log2 (land a b) <= log2 a).
+  intros a b H.
+  apply le_ngt. intros H'.
+  destruct (eq_decidable (land a b) 0) as [EQ|NEQ].
+  rewrite EQ in H'. apply log2_lt_cancel in H'. generalize (le_0_l a); order.
+  generalize (bit_log2 (land a b) NEQ).
+  now rewrite land_spec, bits_above_log2.
+ (* main *)
+ intros a b.
+ destruct (le_ge_cases a b) as [H|H].
+ rewrite min_l by now apply log2_le_mono. now apply AUX.
+ rewrite min_r by now apply log2_le_mono. rewrite land_comm. now apply AUX.
+Qed.
+
+Lemma log2_lxor : forall a b,
+ log2 (lxor a b) <= max (log2 a) (log2 b).
+Proof.
+ assert (AUX : forall a b, a<=b -> log2 (lxor a b) <= log2 b).
+  intros a b H.
+  apply le_ngt. intros H'.
+  destruct (eq_decidable (lxor a b) 0) as [EQ|NEQ].
+  rewrite EQ in H'. apply log2_lt_cancel in H'. generalize (le_0_l a); order.
+  generalize (bit_log2 (lxor a b) NEQ).
+  rewrite lxor_spec, 2 bits_above_log2; try order. discriminate.
+  apply le_lt_trans with (log2 b); trivial. now apply log2_le_mono.
+ (* main *)
+ intros a b.
+ destruct (le_ge_cases a b) as [H|H].
+ rewrite max_r by now apply log2_le_mono. now apply AUX.
+ rewrite max_l by now apply log2_le_mono. rewrite lxor_comm. now apply AUX.
+Qed.
+
+(** Bitwise operations and arithmetical operations *)
+
+Local Notation xor3 a b c := (xorb (xorb a b) c).
+Local Notation lxor3 a b c := (lxor (lxor a b) c).
+
+Local Notation nextcarry a b c := ((a&&b) || (c && (a||b))).
+Local Notation lnextcarry a b c := (lor (land a b) (land c (lor a b))).
+
+Lemma add_bit0 : forall a b, (a+b).[0] = xorb a.[0] b.[0].
+Proof.
+ intros. now rewrite !bit0_odd, odd_add.
+Qed.
+
+Lemma add3_bit0 : forall a b c,
+ (a+b+c).[0] = xor3 a.[0] b.[0] c.[0].
+Proof.
+ intros. now rewrite !add_bit0.
+Qed.
+
+Lemma add3_bits_div2 : forall (a0 b0 c0 : bool),
+ (a0 + b0 + c0)/2 == nextcarry a0 b0 c0.
+Proof.
+ assert (H : 1+1 == 2) by now nzsimpl'.
+ intros [|] [|] [|]; simpl; rewrite ?add_0_l, ?add_0_r, ?H;
+  (apply div_same; order') || (apply div_small; order') || idtac.
+ symmetry. apply div_unique with 1. order'. now nzsimpl'.
+Qed.
+
+Lemma add_carry_div2 : forall a b (c0:bool),
+ (a + b + c0)/2 == a/2 + b/2 + nextcarry a.[0] b.[0] c0.
+Proof.
+ intros.
+ rewrite <- add3_bits_div2.
+ rewrite (add_comm ((a/2)+_)).
+ rewrite <- div_add by order'.
+ apply div_wd; try easy.
+ rewrite <- !div2_div, mul_comm, mul_add_distr_l.
+ rewrite (div2_odd a), <- bit0_odd at 1. fold (b2n a.[0]).
+ rewrite (div2_odd b), <- bit0_odd at 1. fold (b2n b.[0]).
+ rewrite add_shuffle1.
+ rewrite <-(add_assoc _ _ c0). apply add_comm.
+Qed.
+
+(** The main result concerning addition: we express the bits of the sum
+  in term of bits of [a] and [b] and of some carry stream which is also
+  recursively determined by another equation.
+*)
+
+Lemma add_carry_bits : forall a b (c0:bool), exists c,
+ a+b+c0 == lxor3 a b c /\ c/2 == lnextcarry a b c /\ c.[0] = c0.
+Proof.
+ intros a b c0.
+ (* induction over some n such that [a<2^n] and [b<2^n] *)
+ set (n:=max a b).
+ assert (Ha : a<2^n).
+  apply lt_le_trans with (2^a). apply pow_gt_lin_r, lt_1_2.
+  apply pow_le_mono_r. order'. unfold n.
+  destruct (le_ge_cases a b); [rewrite max_r|rewrite max_l]; order'.
+ assert (Hb : b<2^n).
+  apply lt_le_trans with (2^b). apply pow_gt_lin_r, lt_1_2.
+  apply pow_le_mono_r. order'. unfold n.
+  destruct (le_ge_cases a b); [rewrite max_r|rewrite max_l]; order'.
+ clearbody n.
+ revert a b c0 Ha Hb. induct n.
+ (*base*)
+ intros a b c0. rewrite !pow_0_r, !one_succ, !lt_succ_r. intros Ha Hb.
+ exists c0.
+ setoid_replace a with 0 by (generalize (le_0_l a); order').
+ setoid_replace b with 0 by (generalize (le_0_l b); order').
+ rewrite !add_0_l, !lxor_0_l, !lor_0_r, !land_0_r, !lor_0_r.
+ rewrite b2n_div2, b2n_bit0; now repeat split.
+ (*step*)
+ intros n IH a b c0 Ha Hb.
+ set (c1:=nextcarry a.[0] b.[0] c0).
+ destruct (IH (a/2) (b/2) c1) as (c & IH1 & IH2 & Hc); clear IH.
+ apply div_lt_upper_bound; trivial. order'. now rewrite <- pow_succ_r'.
+ apply div_lt_upper_bound; trivial. order'. now rewrite <- pow_succ_r'.
+ exists (c0 + 2*c). repeat split.
+ (* - add *)
+ bitwise.
+ destruct (zero_or_succ m) as [EQ|[m' EQ]]; rewrite EQ; clear EQ.
+ now rewrite add_b2n_double_bit0, add3_bit0, b2n_bit0.
+ rewrite <- !div2_bits, <- 2 lxor_spec.
+ apply testbit_wd; try easy.
+ rewrite add_b2n_double_div2, <- IH1. apply add_carry_div2.
+ (* - carry *)
+ rewrite add_b2n_double_div2.
+ bitwise.
+ destruct (zero_or_succ m) as [EQ|[m' EQ]]; rewrite EQ; clear EQ.
+ now rewrite add_b2n_double_bit0.
+ rewrite <- !div2_bits, IH2. autorewrite with bitwise.
+ now rewrite add_b2n_double_div2.
+ (* - carry0 *)
+ apply add_b2n_double_bit0.
+Qed.
+
+(** Particular case : the second bit of an addition *)
+
+Lemma add_bit1 : forall a b,
+ (a+b).[1] = xor3 a.[1] b.[1] (a.[0] && b.[0]).
+Proof.
+ intros a b.
+ destruct (add_carry_bits a b false) as (c & EQ1 & EQ2 & Hc).
+ simpl in EQ1; rewrite add_0_r in EQ1. rewrite EQ1.
+ autorewrite with bitwise. f_equal.
+ rewrite one_succ, <- div2_bits, EQ2.
+ autorewrite with bitwise.
+ rewrite Hc. simpl. apply orb_false_r.
+Qed.
+
+(** In an addition, there will be no carries iff there is
+  no common bits in the numbers to add *)
+
+Lemma nocarry_equiv : forall a b c,
+ c/2 == lnextcarry a b c -> c.[0] = false ->
+ (c == 0 <-> land a b == 0).
+Proof.
+ intros a b c H H'.
+ split. intros EQ; rewrite EQ in *.
+ rewrite div_0_l in H by order'.
+ symmetry in H. now apply lor_eq_0_l in H.
+ intros EQ. rewrite EQ, lor_0_l in H.
+ apply bits_inj_0.
+ induct n. trivial.
+ intros n IH.
+ rewrite <- div2_bits, H.
+ autorewrite with bitwise.
+ now rewrite IH.
+Qed.
+
+(** When there is no common bits, the addition is just a xor *)
+
+Lemma add_nocarry_lxor : forall a b, land a b == 0 ->
+ a+b == lxor a b.
+Proof.
+ intros a b H.
+ destruct (add_carry_bits a b false) as (c & EQ1 & EQ2 & Hc).
+ simpl in EQ1; rewrite add_0_r in EQ1. rewrite EQ1.
+ apply (nocarry_equiv a b c) in H; trivial.
+ rewrite H. now rewrite lxor_0_r.
+Qed.
+
+(** A null [ldiff] implies being smaller *)
+
+Lemma ldiff_le : forall a b, ldiff a b == 0 -> a <= b.
+Proof.
+ cut (forall n a b, a < 2^n -> ldiff a b == 0 -> a <= b).
+ intros H a b. apply (H a), pow_gt_lin_r; order'.
+ induct n.
+ intros a b Ha _. rewrite pow_0_r, one_succ, lt_succ_r in Ha.
+ assert (Ha' : a == 0) by (generalize (le_0_l a); order').
+ rewrite Ha'. apply le_0_l.
+ intros n IH a b Ha H.
+ assert (NEQ : 2 ~= 0) by order'.
+ rewrite (div_mod a 2 NEQ), (div_mod b 2 NEQ).
+ apply add_le_mono.
+ apply mul_le_mono_l.
+ apply IH.
+ apply div_lt_upper_bound; trivial. now rewrite <- pow_succ_r'.
+ rewrite <- (pow_1_r 2), <- 2 shiftr_div_pow2.
+ now rewrite <- shiftr_ldiff, H, shiftr_div_pow2, pow_1_r, div_0_l.
+ rewrite <- 2 bit0_mod.
+ apply bits_inj_iff in H. specialize (H 0).
+ rewrite ldiff_spec, bits_0 in H.
+ destruct a.[0], b.[0]; try discriminate; simpl; order'.
+Qed.
+
+(** Subtraction can be a ldiff when the opposite ldiff is null. *)
+
+Lemma sub_nocarry_ldiff : forall a b, ldiff b a == 0 ->
+ a-b == ldiff a b.
+Proof.
+ intros a b H.
+ apply add_cancel_r with b.
+ rewrite sub_add.
+ symmetry.
+ rewrite add_nocarry_lxor.
+ bitwise.
+ apply bits_inj_iff in H. specialize (H m).
+ rewrite ldiff_spec, bits_0 in H.
+ now destruct a.[m], b.[m].
+ apply land_ldiff.
+ now apply ldiff_le.
+Qed.
+
+(** We can express lnot in term of subtraction *)
+
+Lemma add_lnot_diag_low : forall a n, log2 a < n ->
+ a + lnot a n == ones n.
+Proof.
+ intros a n H.
+ assert (H' := land_lnot_diag_low a n H).
+ rewrite add_nocarry_lxor, lxor_lor by trivial.
+ now apply lor_lnot_diag_low.
+Qed.
+
+Lemma lnot_sub_low : forall a n, log2 a < n ->
+ lnot a n == ones n - a.
+Proof.
+ intros a n H.
+ now rewrite <- (add_lnot_diag_low a n H), add_comm, add_sub.
+Qed.
+
+(** Adding numbers with no common bits cannot lead to a much bigger number *)
+
+Lemma add_nocarry_lt_pow2 : forall a b n, land a b == 0 ->
+ a < 2^n -> b < 2^n -> a+b < 2^n.
+Proof.
+ intros a b n H Ha Hb.
+ rewrite add_nocarry_lxor by trivial.
+ apply div_small_iff. order_nz.
+ rewrite <- shiftr_div_pow2, shiftr_lxor, !shiftr_div_pow2.
+ rewrite 2 div_small by trivial.
+ apply lxor_0_l.
+Qed.
+
+Lemma add_nocarry_mod_lt_pow2 : forall a b n, land a b == 0 ->
+ a mod 2^n + b mod 2^n < 2^n.
+Proof.
+ intros a b n H.
+ apply add_nocarry_lt_pow2.
+ bitwise.
+ destruct (le_gt_cases n m).
+ now rewrite mod_pow2_bits_high.
+ now rewrite !mod_pow2_bits_low, <- land_spec, H, bits_0.
+ apply mod_upper_bound; order_nz.
+ apply mod_upper_bound; order_nz.
+Qed.
+
+End NBitsProp.
diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v
index 9110ec036c..47f4096052 100644
--- a/theories/Numbers/Natural/Abstract/NDiv.v
+++ b/theories/Numbers/Natural/Abstract/NDiv.v
@@ -219,6 +219,10 @@ Lemma div_div : forall a b c, b~=0 -> c~=0 ->
  (a/b)/c == a/(b*c).
 Proof. intros. apply div_div; auto'. Qed.
 
+Lemma mod_mul_r : forall a b c, b~=0 -> c~=0 ->
+ a mod (b*c) == a mod b + b*((a/b) mod c).
+Proof. intros. apply mod_mul_r; auto'. Qed.
+
 (** A last inequality: *)
 
 Theorem div_mul_le:
diff --git a/theories/Numbers/Natural/Abstract/NParity.v b/theories/Numbers/Natural/Abstract/NParity.v
index bd65886867..6a1e20ce0b 100644
--- a/theories/Numbers/Natural/Abstract/NParity.v
+++ b/theories/Numbers/Natural/Abstract/NParity.v
@@ -6,172 +6,31 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Bool NSub.
+Require Import Bool NSub NZParity.
 
-(** Properties of [even], [odd]. *)
-
-(** NB: most parts of [NParity] and [ZParity] are common,
-    but it is difficult to share them in NZ, since
-    initial proofs [Even_or_Odd] and [Even_Odd_False] must
-    be proved differently *)
+(** Some additionnal properties of [even], [odd]. *)
 
 Module Type NParityProp (Import N : NAxiomsSig')(Import NP : NSubProp N).
 
-Instance Even_wd : Proper (eq==>iff) Even.
-Proof. unfold Even. solve_predicate_wd. Qed.
-
-Instance Odd_wd : Proper (eq==>iff) Odd.
-Proof. unfold Odd. solve_predicate_wd. Qed.
-
-Instance even_wd : Proper (eq==>Logic.eq) even.
-Proof.
- intros x x' EQ. rewrite eq_iff_eq_true, 2 even_spec. now apply Even_wd.
-Qed.
-
-Instance odd_wd : Proper (eq==>Logic.eq) odd.
-Proof.
- intros x x' EQ. rewrite eq_iff_eq_true, 2 odd_spec. now apply Odd_wd.
-Qed.
-
-Lemma Even_or_Odd : forall x, Even x \/ Odd x.
-Proof.
- induct x.
- left. exists 0. now nzsimpl.
- intros x.
- intros [(y,H)|(y,H)].
- right. exists y. rewrite H. now nzsimpl.
- left. exists (S y). rewrite H. now nzsimpl'.
-Qed.
-
-Lemma double_below : forall n m, n<=m -> 2*n < 2*m+1.
-Proof.
- intros. nzsimpl'. apply lt_succ_r. now apply add_le_mono.
-Qed.
-
-Lemma double_above : forall n m, n<m -> 2*n+1 < 2*m.
-Proof.
- intros. nzsimpl'.
- rewrite <- le_succ_l, <- add_succ_l, <- add_succ_r.
- apply add_le_mono; now apply le_succ_l.
-Qed.
-
-Lemma Even_Odd_False : forall x, Even x -> Odd x -> False.
-Proof.
-intros x (y,E) (z,O). rewrite O in E; clear O.
-destruct (le_gt_cases y z) as [LE|GT].
-generalize (double_below _ _ LE); order.
-generalize (double_above _ _ GT); order.
-Qed.
-
-Lemma orb_even_odd : forall n, orb (even n) (odd n) = true.
-Proof.
- intros.
- destruct (Even_or_Odd n) as [H|H].
- rewrite <- even_spec in H. now rewrite H.
- rewrite <- odd_spec in H. now rewrite H, orb_true_r.
-Qed.
-
-Lemma negb_odd_even : forall n, negb (odd n) = even n.
-Proof.
- intros.
- generalize (Even_or_Odd n) (Even_Odd_False n).
- rewrite <- even_spec, <- odd_spec.
- destruct (odd n), (even n); simpl; intuition.
-Qed.
-
-Lemma negb_even_odd : forall n, negb (even n) = odd n.
-Proof.
- intros. rewrite <- negb_odd_even. apply negb_involutive.
-Qed.
-
-Lemma even_0 : even 0 = true.
-Proof.
- rewrite even_spec. exists 0. now nzsimpl.
-Qed.
+Include NZParityProp N N NP.
 
-Lemma odd_1 : odd 1 = true.
-Proof.
- rewrite odd_spec. exists 0. now nzsimpl'.
-Qed.
-
-Lemma Odd_succ_Even : forall n, Odd (S n) <-> Even n.
-Proof.
- split; intros (m,H).
- exists m. apply succ_inj. now rewrite add_1_r in H.
- exists m. rewrite add_1_r. now apply succ_wd.
-Qed.
-
-Lemma odd_succ_even : forall n, odd (S n) = even n.
-Proof.
- intros. apply eq_iff_eq_true. rewrite even_spec, odd_spec.
- apply Odd_succ_Even.
-Qed.
-
-Lemma even_succ_odd : forall n, even (S n) = odd n.
-Proof.
- intros. now rewrite <- negb_odd_even, odd_succ_even, negb_even_odd.
-Qed.
-
-Lemma Even_succ_Odd : forall n, Even (S n) <-> Odd n.
-Proof.
- intros. now rewrite <- even_spec, even_succ_odd, odd_spec.
-Qed.
-
-Lemma odd_pred_even : forall n, n~=0 -> odd (P n) = even n.
+Lemma odd_pred : forall n, n~=0 -> odd (P n) = even n.
 Proof.
  intros. rewrite <- (succ_pred n) at 2 by trivial.
- symmetry. apply even_succ_odd.
+ symmetry. apply even_succ.
 Qed.
 
-Lemma even_pred_odd : forall n, n~=0 -> even (P n) = odd n.
+Lemma even_pred : forall n, n~=0 -> even (P n) = odd n.
 Proof.
  intros. rewrite <- (succ_pred n) at 2 by trivial.
- symmetry. apply odd_succ_even.
-Qed.
-
-Lemma even_add : forall n m, even (n+m) = Bool.eqb (even n) (even m).
-Proof.
- intros.
- case_eq (even n); case_eq (even m);
-  rewrite <- ?negb_true_iff, ?negb_even_odd, ?odd_spec, ?even_spec;
-  intros (m',Hm) (n',Hn).
- exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm.
- exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_assoc.
- exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_shuffle0.
- exists (n'+m'+1). rewrite Hm,Hn. nzsimpl'. now rewrite add_shuffle1.
-Qed.
-
-Lemma odd_add : forall n m, odd (n+m) = xorb (odd n) (odd m).
-Proof.
- intros. rewrite <- !negb_even_odd. rewrite even_add.
- now destruct (even n), (even m).
-Qed.
-
-Lemma even_mul : forall n m, even (mul n m) = even n || even m.
-Proof.
- intros.
- case_eq (even n); simpl; rewrite ?even_spec.
- intros (n',Hn). exists (n'*m). now rewrite Hn, mul_assoc.
- case_eq (even m); simpl; rewrite ?even_spec.
- intros (m',Hm). exists (n*m'). now rewrite Hm, !mul_assoc, (mul_comm 2).
- (* odd / odd *)
- rewrite <- !negb_true_iff, !negb_even_odd, !odd_spec.
- intros (m',Hm) (n',Hn). exists (n'*2*m' +n'+m').
- rewrite Hn,Hm, !mul_add_distr_l, !mul_add_distr_r, !mul_1_l, !mul_1_r.
- now rewrite add_shuffle1, add_assoc, !mul_assoc.
-Qed.
-
-Lemma odd_mul : forall n m, odd (mul n m) = odd n && odd m.
-Proof.
- intros. rewrite <- !negb_even_odd. rewrite even_mul.
- now destruct (even n), (even m).
+ symmetry. apply odd_succ.
 Qed.
 
 Lemma even_sub : forall n m, m<=n -> even (n-m) = Bool.eqb (even n) (even m).
 Proof.
  intros.
  case_eq (even n); case_eq (even m);
-  rewrite <- ?negb_true_iff, ?negb_even_odd, ?odd_spec, ?even_spec;
+  rewrite <- ?negb_true_iff, ?negb_even, ?odd_spec, ?even_spec;
   intros (m',Hm) (n',Hn).
  exists (n'-m'). now rewrite mul_sub_distr_l, Hn, Hm.
  exists (n'-m'-1).
@@ -197,7 +56,7 @@ Qed.
 
 Lemma odd_sub : forall n m, m<=n -> odd (n-m) = xorb (odd n) (odd m).
 Proof.
- intros. rewrite <- !negb_even_odd. rewrite even_sub by trivial.
+ intros. rewrite <- !negb_even. rewrite even_sub by trivial.
  now destruct (even n), (even m).
 Qed.
 
diff --git a/theories/Numbers/Natural/Abstract/NPow.v b/theories/Numbers/Natural/Abstract/NPow.v
index 275a5c4f5e..68976624e3 100644
--- a/theories/Numbers/Natural/Abstract/NPow.v
+++ b/theories/Numbers/Natural/Abstract/NPow.v
@@ -50,10 +50,21 @@ Proof. wrap pow_mul_l. Qed.
 Lemma pow_mul_r : forall a b c, a^(b*c) == (a^b)^c.
 Proof. wrap pow_mul_r. Qed.
 
-(** Positivity *)
+(** Power and nullity *)
 
-Lemma pow_nonzero : forall a b, a~=0 -> a^b~=0.
-Proof. intros. rewrite neq_0_lt_0. wrap pow_pos_nonneg. Qed.
+Lemma pow_eq_0 : forall a b, b~=0 -> a^b == 0 -> a == 0.
+Proof. intros. apply (pow_eq_0 a b); trivial. auto'. Qed.
+
+Lemma pow_nonzero : forall a b, a~=0 -> a^b ~= 0.
+Proof. wrap pow_nonzero. Qed.
+
+Lemma pow_eq_0_iff : forall a b, a^b == 0 <-> b~=0 /\ a==0.
+Proof.
+ intros a b. split.
+ rewrite pow_eq_0_iff. intros [H |[H H']].
+  generalize (le_0_l b); order. split; order.
+ intros (Hb,Ha). rewrite Ha. now apply pow_0_l'.
+Qed.
 
 (** Monotonicity *)
 
@@ -143,7 +154,7 @@ Qed.
 
 Lemma odd_pow : forall a b, b~=0 -> odd (a^b) = odd a.
 Proof.
- intros. now rewrite <- !negb_even_odd, even_pow.
+ intros. now rewrite <- !negb_even, even_pow.
 Qed.
 
 End NPowProp.
diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v
index 58e3afe78c..1edb6b51f8 100644
--- a/theories/Numbers/Natural/Abstract/NProperties.v
+++ b/theories/Numbers/Natural/Abstract/NProperties.v
@@ -7,10 +7,11 @@
 (************************************************************************)
 
 Require Export NAxioms.
-Require Import NMaxMin NParity NPow NSqrt NLog NDiv NGcd NLcm.
+Require Import NMaxMin NParity NPow NSqrt NLog NDiv NGcd NLcm NBits.
 
 (** This functor summarizes all known facts about N. *)
 
 Module Type NProp (N:NAxiomsSig) :=
  NMaxMinProp N <+ NParityProp N <+ NPowProp N <+ NSqrtProp N
-  <+ NLog2Prop N <+ NDivProp N <+ NGcdProp N <+ NLcmProp N.
+  <+ NLog2Prop N <+ NDivProp N <+ NGcdProp N <+ NLcmProp N
+  <+ NBitsProp N.
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 209bee8c16..315876656d 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -12,7 +12,7 @@
 
 Require Export Int31.
 Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake
-  NProperties NDiv GenericMinMax.
+  NProperties GenericMinMax.
 
 (** The following [BigN] module regroups both the operations and
     all the abstract properties:
@@ -21,8 +21,7 @@ Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake
        w.r.t. ZArith
     - [NTypeIsNAxioms] shows (mainly) that these operations implement
       the interface [NAxioms]
-    - [NPropSig] adds all generic properties derived from [NAxioms]
-    - [NDivPropFunct] provides generic properties of [div] and [mod].
+    - [NProp] adds all generic properties derived from [NAxioms]
     - [MinMax*Properties] provides properties of [min] and [max].
 
 *)
@@ -43,6 +42,7 @@ Bind Scope bigN_scope with BigN.t.
 Bind Scope bigN_scope with BigN.t'.
 (* Bind Scope has no retroactive effect, let's declare scopes by hand. *)
 Arguments Scope BigN.to_Z [bigN_scope].
+Arguments Scope BigN.to_N [bigN_scope].
 Arguments Scope BigN.succ [bigN_scope].
 Arguments Scope BigN.pred [bigN_scope].
 Arguments Scope BigN.square [bigN_scope].
@@ -66,8 +66,21 @@ Arguments Scope BigN.sqrt [bigN_scope].
 Arguments Scope BigN.div_eucl [bigN_scope bigN_scope].
 Arguments Scope BigN.modulo [bigN_scope bigN_scope].
 Arguments Scope BigN.gcd [bigN_scope bigN_scope].
+Arguments Scope BigN.lcm [bigN_scope bigN_scope].
 Arguments Scope BigN.even [bigN_scope].
 Arguments Scope BigN.odd [bigN_scope].
+Arguments Scope BigN.testbit [bigN_scope bigN_scope].
+Arguments Scope BigN.shiftl [bigN_scope bigN_scope].
+Arguments Scope BigN.shiftr [bigN_scope bigN_scope].
+Arguments Scope BigN.lor [bigN_scope bigN_scope].
+Arguments Scope BigN.land [bigN_scope bigN_scope].
+Arguments Scope BigN.ldiff [bigN_scope bigN_scope].
+Arguments Scope BigN.lxor [bigN_scope bigN_scope].
+Arguments Scope BigN.setbit [bigN_scope bigN_scope].
+Arguments Scope BigN.clearbit [bigN_scope bigN_scope].
+Arguments Scope BigN.lnot [bigN_scope bigN_scope].
+Arguments Scope BigN.div2 [bigN_scope].
+Arguments Scope BigN.ones [bigN_scope].
 
 Local Notation "0" := BigN.zero : bigN_scope. (* temporary notation *)
 Local Notation "1" := BigN.one : bigN_scope. (* temporary notation *)
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index 306efc19ca..a55fb59001 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -16,7 +16,7 @@
     representation. The representation-dependent (and macro-generated) part
     is now in [NMake_gen]. *)
 
-Require Import Bool BigNumPrelude ZArith Nnat CyclicAxioms DoubleType
+Require Import Bool BigNumPrelude ZArith Nnat Ndigits CyclicAxioms DoubleType
   Nbasic Wf_nat StreamMemo NSig NMake_gen.
 
 Module Make (W0:CyclicType) <: NType.
@@ -972,6 +972,44 @@ Module Make (W0:CyclicType) <: NType.
  intros; apply spec_gcd_gt; auto with zarith.
  Qed.
 
+ (** * Parity test *)
+
+ Definition even : t -> bool := Eval red_t in
+   iter_t (fun n x => ZnZ.is_even x).
+
+ Definition odd x := negb (even x).
+
+ Lemma even_fold : even = iter_t (fun n x => ZnZ.is_even x).
+ Proof. red_t; reflexivity. Qed.
+
+ Theorem spec_even_aux: forall x,
+   if even x then [x] mod 2 = 0 else [x] mod 2 = 1.
+ Proof.
+ intros x. rewrite even_fold. destr_t x as (n,x).
+ exact (ZnZ.spec_is_even x).
+ Qed.
+
+ Theorem spec_even: forall x, even x = Zeven_bool [x].
+ Proof.
+ intros x. assert (H := spec_even_aux x). symmetry.
+ rewrite (Z_div_mod_eq_full [x] 2); auto with zarith.
+ destruct (even x); rewrite H, ?Zplus_0_r.
+ rewrite Zeven_bool_iff. apply Zeven_2p.
+ apply not_true_is_false. rewrite Zeven_bool_iff.
+ apply Zodd_not_Zeven. apply Zodd_2p_plus_1.
+ Qed.
+
+ Theorem spec_odd: forall x, odd x = Zodd_bool [x].
+ Proof.
+ intros x. unfold odd.
+ assert (H := spec_even_aux x). symmetry.
+ rewrite (Z_div_mod_eq_full [x] 2); auto with zarith.
+ destruct (even x); rewrite H, ?Zplus_0_r; simpl negb.
+ apply not_true_is_false. rewrite Zodd_bool_iff.
+ apply Zeven_not_Zodd. apply Zeven_2p.
+ apply Zodd_bool_iff. apply Zodd_2p_plus_1.
+ Qed.
+
  (** * Conversion *)
 
  Definition pheight p :=
@@ -1212,7 +1250,7 @@ Module Make (W0:CyclicType) <: NType.
    let sub_c := ZnZ.sub_c in
    let add_mul_div := ZnZ.add_mul_div in
    let zzero := ZnZ.zero in
-   fun p x => match sub_c zdigits p with
+   fun x p => match sub_c zdigits p with
    | C0 d => reduce n (add_mul_div d zzero x)
    | C1 _ => zero
    end).
@@ -1236,13 +1274,13 @@ Module Make (W0:CyclicType) <: NType.
    rewrite Zpower_0_r; ring.
  Qed.
 
- Theorem spec_shiftr: forall n x,
-  [shiftr n x] = [x] / 2 ^ [n].
+ Theorem spec_shiftr_pow2 : forall x n,
+  [shiftr x n] = [x] / 2 ^ [n].
  Proof.
   intros x y. rewrite shiftr_fold. apply spec_same_level. clear x y.
-  intros n p x. simpl.
-  assert (Hx := ZnZ.spec_to_Z p).
-  assert (Hy := ZnZ.spec_to_Z x).
+  intros n x p. simpl.
+  assert (Hx := ZnZ.spec_to_Z x).
+  assert (Hy := ZnZ.spec_to_Z p).
   generalize (ZnZ.spec_sub_c (ZnZ.zdigits (dom_op n)) p).
   case ZnZ.sub_c; intros d H; unfold interp_carry in *; simpl.
   (** Subtraction without underflow : [ p <= digits ] *)
@@ -1264,6 +1302,12 @@ Module Make (W0:CyclicType) <: NType.
   generalize (ZnZ.spec_to_Z d); auto with zarith.
  Qed.
 
+ Lemma spec_shiftr: forall x p, [shiftr x p] = Zshiftr [x] [p].
+ Proof.
+  intros.
+  now rewrite spec_shiftr_pow2, Z.shiftr_div_pow2 by apply spec_pos.
+ Qed.
+
  (** * Left shift *)
 
  (** First an unsafe version, working correctly only if
@@ -1273,7 +1317,7 @@ Module Make (W0:CyclicType) <: NType.
    let op := dom_op n in
    let add_mul_div := ZnZ.add_mul_div in
    let zero := ZnZ.zero in
-   fun p x => reduce n (add_mul_div p x zero)).
+   fun x p => reduce n (add_mul_div p x zero)).
 
  Definition unsafe_shiftl : t -> t -> t := Eval red_t in
    same_level unsafe_shiftln.
@@ -1281,20 +1325,20 @@ Module Make (W0:CyclicType) <: NType.
  Lemma unsafe_shiftl_fold : unsafe_shiftl = same_level unsafe_shiftln.
  Proof. red_t; reflexivity. Qed.
 
- Theorem spec_unsafe_shiftl_aux : forall p x K,
+ Theorem spec_unsafe_shiftl_aux : forall x p K,
   0 <= K ->
   [x] < 2^K ->
   [p] + K <= Zpos (digits x) ->
-  [unsafe_shiftl p x] = [x] * 2 ^ [p].
+  [unsafe_shiftl x p] = [x] * 2 ^ [p].
  Proof.
- intros p x.
+ intros x p.
  rewrite unsafe_shiftl_fold. rewrite digits_level.
  apply spec_same_level_dep.
  intros n m z z' r LE H K HK H1 H2. apply (H K); auto.
   transitivity (Zpos (ZnZ.digits (dom_op n))); auto.
   apply digits_dom_op_incr; auto.
- clear p x.
- intros n p x K HK Hx Hp. simpl. rewrite spec_reduce.
+ clear x p.
+ intros n x p K HK Hx Hp. simpl. rewrite spec_reduce.
  destruct (ZnZ.spec_to_Z x).
  destruct (ZnZ.spec_to_Z p).
  rewrite ZnZ.spec_add_mul_div by (omega with *).
@@ -1308,8 +1352,8 @@ Module Make (W0:CyclicType) <: NType.
  apply Zpower_le_monotone2; auto with zarith.
  Qed.
 
- Theorem spec_unsafe_shiftl: forall p x,
-  [p] <= [head0 x] -> [unsafe_shiftl p x] = [x] * 2 ^ [p].
+ Theorem spec_unsafe_shiftl: forall x p,
+  [p] <= [head0 x] -> [unsafe_shiftl x p] = [x] * 2 ^ [p].
  Proof.
  intros.
  destruct (Z_eq_dec [x] 0) as [EQ|NEQ].
@@ -1436,19 +1480,19 @@ Module Make (W0:CyclicType) <: NType.
  (** Finally we iterate [double_size] enough before [unsafe_shiftl]
      in order to get a fully correct [shiftl]. *)
 
- Definition shiftl_aux_body cont n x :=
-   match compare n (head0 x)  with
-      Gt => cont n (double_size x)
-   |  _ => unsafe_shiftl n x
+ Definition shiftl_aux_body cont x n :=
+   match compare n (head0 x) with
+      Gt => cont (double_size x) n
+   |  _ => unsafe_shiftl x n
    end.
 
- Theorem spec_shiftl_aux_body: forall n p x cont,
+ Theorem spec_shiftl_aux_body: forall n x p cont,
        2^ Zpos p  <=  [head0 x]  ->
       (forall x, 2 ^ (Zpos p + 1) <= [head0 x]->
-         [cont n x] = [x] * 2 ^ [n]) ->
-      [shiftl_aux_body cont n x] = [x] * 2 ^ [n].
+         [cont x n] = [x] * 2 ^ [n]) ->
+      [shiftl_aux_body cont x n] = [x] * 2 ^ [n].
  Proof.
- intros n p x cont H1 H2; unfold shiftl_aux_body.
+ intros n x p cont H1 H2; unfold shiftl_aux_body.
  rewrite spec_compare; case Zcompare_spec; intros H.
   apply spec_unsafe_shiftl; auto with zarith.
   apply spec_unsafe_shiftl; auto with zarith.
@@ -1459,22 +1503,22 @@ Module Make (W0:CyclicType) <: NType.
  rewrite Zpower_1_r; apply Zmult_le_compat_l; auto with zarith.
  Qed.
 
- Fixpoint shiftl_aux p cont n x :=
+ Fixpoint shiftl_aux p cont x n :=
    shiftl_aux_body
-       (fun n x => match p with
-        | xH => cont n x
-        | xO p => shiftl_aux p (shiftl_aux p cont) n x
-        | xI p => shiftl_aux p (shiftl_aux p cont) n x
-        end) n x.
+       (fun x n => match p with
+        | xH => cont x n
+        | xO p => shiftl_aux p (shiftl_aux p cont) x n
+        | xI p => shiftl_aux p (shiftl_aux p cont) x n
+        end) x n.
 
- Theorem spec_shiftl_aux: forall p q n x cont,
+ Theorem spec_shiftl_aux: forall p q x n cont,
     2 ^ (Zpos q) <= [head0 x] ->
       (forall x, 2 ^ (Zpos p + Zpos q) <= [head0 x] ->
-         [cont n x] = [x] * 2 ^ [n]) ->
-      [shiftl_aux p cont n x] = [x] * 2 ^ [n].
+         [cont x n] = [x] * 2 ^ [n]) ->
+      [shiftl_aux p cont x n] = [x] * 2 ^ [n].
  Proof.
  intros p; elim p; unfold shiftl_aux; fold shiftl_aux; clear p.
- intros p Hrec q n x cont H1 H2.
+ intros p Hrec q x n cont H1 H2.
  apply spec_shiftl_aux_body with (q); auto.
  intros x1 H3; apply Hrec with (q + 1)%positive; auto.
  intros x2 H4; apply Hrec with (p + q + 1)%positive; auto.
@@ -1501,15 +1545,15 @@ Module Make (W0:CyclicType) <: NType.
  rewrite Zplus_comm; auto.
  Qed.
 
- Definition shiftl n x :=
+ Definition shiftl x n :=
   shiftl_aux_body
    (shiftl_aux_body
-    (shiftl_aux (digits n) unsafe_shiftl)) n x.
+    (shiftl_aux (digits n) unsafe_shiftl)) x n.
 
- Theorem spec_shiftl: forall n x,
-   [shiftl n x] = [x] * 2 ^ [n].
+ Theorem spec_shiftl_pow2 : forall x n,
+   [shiftl x n] = [x] * 2 ^ [n].
  Proof.
- intros n x; unfold shiftl, shiftl_aux_body.
+ intros x n; unfold shiftl, shiftl_aux_body.
  rewrite spec_compare; case Zcompare_spec; intros H.
   apply spec_unsafe_shiftl; auto with zarith.
   apply spec_unsafe_shiftl; auto with zarith.
@@ -1531,42 +1575,64 @@ Module Make (W0:CyclicType) <: NType.
  apply Zpower_le_monotone2; auto with zarith.
  Qed.
 
- (** * Parity test *)
+ Lemma spec_shiftl: forall x p, [shiftl x p] = Zshiftl [x] [p].
+ Proof.
+  intros.
+  now rewrite spec_shiftl_pow2, Z.shiftl_mul_pow2 by apply spec_pos.
+ Qed.
 
- Definition even : t -> bool := Eval red_t in
-   iter_t (fun n x => ZnZ.is_even x).
+ (** Other bitwise operations *)
 
- Definition odd x := negb (even x).
+ Definition testbit x n := odd (shiftr x n).
 
- Lemma even_fold : even = iter_t (fun n x => ZnZ.is_even x).
- Proof. red_t; reflexivity. Qed.
+ Lemma spec_testbit: forall x p, testbit x p = Ztestbit [x] [p].
+ Proof.
+  intros. unfold testbit. symmetry.
+  rewrite spec_odd, spec_shiftr. apply Z.testbit_odd.
+ Qed.
 
- Theorem spec_even_aux: forall x,
-   if even x then [x] mod 2 = 0 else [x] mod 2 = 1.
+ Definition div2 x := shiftr x one.
+
+ Lemma spec_div2: forall x, [div2 x] = Zdiv2' [x].
  Proof.
- intros x. rewrite even_fold. destr_t x as (n,x).
- exact (ZnZ.spec_is_even x).
+  intros. unfold div2. symmetry.
+  rewrite spec_shiftr, spec_1. apply Zdiv2'_spec.
  Qed.
 
- Theorem spec_even: forall x, even x = Zeven_bool [x].
+ (** TODO : provide efficient versions instead of just converting
+   from/to N (see with Laurent) *)
+
+ Definition lor x y := of_N (Nor (to_N x) (to_N y)).
+ Definition land x y := of_N (Nand (to_N x) (to_N y)).
+ Definition ldiff x y := of_N (Ndiff (to_N x) (to_N y)).
+ Definition lxor x y := of_N (Nxor (to_N x) (to_N y)).
+
+ Lemma spec_land: forall x y, [land x y] = Zand [x] [y].
  Proof.
- intros x. assert (H := spec_even_aux x). symmetry.
- rewrite (Z_div_mod_eq_full [x] 2); auto with zarith.
- destruct (even x); rewrite H, ?Zplus_0_r.
- rewrite Zeven_bool_iff. apply Zeven_2p.
- apply not_true_is_false. rewrite Zeven_bool_iff.
- apply Zodd_not_Zeven. apply Zodd_2p_plus_1.
+  intros x y. unfold land. rewrite spec_of_N. unfold to_N.
+  generalize (spec_pos x), (spec_pos y).
+  destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2).
  Qed.
 
- Theorem spec_odd: forall x, odd x = Zodd_bool [x].
+ Lemma spec_lor: forall x y, [lor x y] = Zor [x] [y].
  Proof.
- intros x. unfold odd.
- assert (H := spec_even_aux x). symmetry.
- rewrite (Z_div_mod_eq_full [x] 2); auto with zarith.
- destruct (even x); rewrite H, ?Zplus_0_r; simpl negb.
- apply not_true_is_false. rewrite Zodd_bool_iff.
- apply Zeven_not_Zodd. apply Zeven_2p.
- apply Zodd_bool_iff. apply Zodd_2p_plus_1.
+  intros x y. unfold lor. rewrite spec_of_N. unfold to_N.
+  generalize (spec_pos x), (spec_pos y).
+  destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2).
+ Qed.
+
+ Lemma spec_ldiff: forall x y, [ldiff x y] = Zdiff [x] [y].
+ Proof.
+  intros x y. unfold ldiff. rewrite spec_of_N. unfold to_N.
+  generalize (spec_pos x), (spec_pos y).
+  destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2).
+ Qed.
+
+ Lemma spec_lxor: forall x y, [lxor x y] = Zxor [x] [y].
+ Proof.
+  intros x y. unfold lxor. rewrite spec_of_N. unfold to_N.
+  generalize (spec_pos x), (spec_pos y).
+  destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2).
  Qed.
 
 End Make.
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 2736013c64..8779f4be37 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -711,12 +711,12 @@ pr
    (Pantimon : forall n m z z' r, n <= m -> P m z z' r -> P n z z' r)
    (f : forall n, dom_t n -> dom_t n -> res)
    (Pf: forall n x y, P n (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y)),
-   forall x y, P (level y) [x] [y] (same_level f x y).
+   forall x y, P (level x) [x] [y] (same_level f x y).
  Proof.
  intros res P Pantimon f Pf.
  set (f' := fun n x y => (n, f n x y)).
  set (P' := fun z z' r => P (fst r) z z' (snd r)).
- assert (FST : forall x y, level y <= fst (same_level f' x y))
+ assert (FST : forall x y, level x <= fst (same_level f' x y))
   by (destruct x, y; simpl; omega with * ).
  assert (SND : forall x y, same_level f x y = snd (same_level f' x y))
   by (destruct x, y; reflexivity).
diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index 56dd9c8c56..552002e449 100644
--- a/theories/Numbers/Natural/BigN/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.v
@@ -565,7 +565,7 @@ Axiom spec_same_level_dep :
    (Pantimon : forall n m z z' r, (n <= m)%nat -> P m z z' r -> P n z z' r)
    (f : forall n, dom_t n -> dom_t n -> res)
    (Pf: forall n x y, P n (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y)),
-   forall x y, P (level y) [x] [y] (same_level f x y).
+   forall x y, P (level x) [x] [y] (same_level f x y).
 
 (** [mk_t_S] : building a number of the next level *)
 
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index 1b5d382a32..d2979bcf05 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-Require Import BinPos Ndiv_def Nsqrt_def Ngcd_def.
+Require Import BinPos Ndiv_def Nsqrt_def Ngcd_def Ndigits.
 Require Export BinNat.
 Require Import NAxioms NProperties.
 
@@ -178,6 +178,20 @@ Definition gcd_greatest := Ngcd_greatest.
 Lemma gcd_nonneg : forall a b, 0 <= Ngcd a b.
 Proof. intros. now destruct (Ngcd a b). Qed.
 
+(** Bitwise Operations *)
+
+Definition testbit_spec a n (_:0<=n) := Ntestbit_spec a n.
+Lemma testbit_neg_r a n (H:n<0) : Ntestbit a n = false.
+Proof. now destruct n. Qed.
+Definition shiftl_spec_low := Nshiftl_spec_low.
+Definition shiftl_spec_high a n m (_:0<=m) := Nshiftl_spec_high a n m.
+Definition shiftr_spec a n m (_:0<=m) := Nshiftr_spec a n m.
+Definition lxor_spec := Nxor_spec.
+Definition land_spec := Nand_spec.
+Definition lor_spec := Nor_spec.
+Definition ldiff_spec := Ndiff_spec.
+Definition div2_spec a : Ndiv2 a = Nshiftr a 1 := eq_refl _.
+
 (** The instantiation of operations.
     Placing them at the very end avoids having indirections in above lemmas. *)
 
@@ -207,6 +221,14 @@ Definition sqrt := Nsqrt.
 Definition log2 := Nlog2.
 Definition divide := Ndivide.
 Definition gcd := Ngcd.
+Definition testbit := Ntestbit.
+Definition shiftl := Nshiftl.
+Definition shiftr := Nshiftr.
+Definition lxor := Nxor.
+Definition land := Nand.
+Definition lor := Nor.
+Definition ldiff := Ndiff.
+Definition div2 := Ndiv2.
 
 Include NProp
  <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 60c59b3236..6f72a504cd 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 Require Import
- Bool Peano Peano_dec Compare_dec Plus Mult Minus Le Lt EqNat
+ Bool Peano Peano_dec Compare_dec Plus Mult Minus Le Lt EqNat Div2 Wf_nat
  NAxioms NProperties.
 
 (** Functions not already defined *)
@@ -69,6 +69,21 @@ Proof.
    now rewrite <- !plus_n_Sm, <- !plus_n_O.
 Qed.
 
+Lemma Even_equiv : forall n, Even n <-> Even.even n.
+Proof.
+ split. intros (p,->). apply Even.even_mult_l. do 3 constructor.
+ intros H. destruct (even_2n n H) as (p,->).
+ exists p. unfold double. simpl. now rewrite <- plus_n_O.
+Qed.
+
+Lemma Odd_equiv : forall n, Odd n <-> Even.odd n.
+Proof.
+ split. intros (p,->). rewrite <- plus_n_Sm, <- plus_n_O.
+ apply Even.odd_S. apply Even.even_mult_l. do 3 constructor.
+ intros H. destruct (odd_S2n n H) as (p,->).
+ exists p. unfold double. simpl. now rewrite <- plus_n_Sm, <- !plus_n_O.
+Qed.
+
 (* A linear, tail-recursive, division for nat.
 
    In [divmod], [y] is the predecessor of the actual divisor,
@@ -332,6 +347,191 @@ Proof.
  now rewrite mult_minus_distr_l, mult_assoc, Hu, Hv, minus_plus.
 Qed.
 
+(** * Bitwise operations *)
+
+(** We provide here some bitwise operations for unary numbers.
+  Some might be really naive, they are just there for fullfiling
+  the same interface as other for natural representations. As
+  soon as binary representations such as NArith are available,
+  it is clearly better to convert to/from them and use their ops.
+*)
+
+Fixpoint testbit a n :=
+ match n with
+   | O => odd a
+   | S n => testbit (div2 a) n
+ end.
+
+Definition shiftl a n := iter_nat n _ double a.
+Definition shiftr a n := iter_nat n _ div2 a.
+
+Fixpoint bitwise (op:bool->bool->bool) n a b :=
+ match n with
+  | O => O
+  | S n' =>
+    (if op (odd a) (odd b) then 1 else 0) +
+    2*(bitwise op n' (div2 a) (div2 b))
+ end.
+
+Definition land a b := bitwise andb a a b.
+Definition lor a b := bitwise orb (max a b) a b.
+Definition ldiff a b := bitwise (fun b b' => b && negb b') a a b.
+Definition lxor a b := bitwise xorb (max a b) a b.
+
+Lemma double_twice : forall n, double n = 2*n.
+Proof.
+ simpl; intros. now rewrite <- plus_n_O.
+Qed.
+
+Lemma testbit_0_l : forall n, testbit 0 n = false.
+Proof.
+ now induction n.
+Qed.
+
+Lemma testbit_spec : forall a n,
+ exists l, exists h, 0<=l<2^n /\
+  a = l + ((if testbit a n then 1 else 0) + 2*h)*2^n.
+Proof.
+ intros a n. revert a. induction n; intros a; simpl testbit.
+ exists 0. exists (div2 a).
+ split. simpl.  unfold lt. now split.
+ case_eq (odd a); intros EQ; simpl.
+ rewrite mult_1_r, <- plus_n_O.
+  now apply odd_double, Odd_equiv, odd_spec.
+ rewrite mult_1_r, <- plus_n_O. apply even_double.
+  destruct (Even.even_or_odd a) as [H|H]; trivial.
+  apply Odd_equiv, odd_spec in H. rewrite H in EQ; discriminate.
+ destruct (IHn (div2 a)) as (l & h & (_,H) & EQ).
+ destruct (Even.even_or_odd a) as [EV|OD].
+ exists (double l). exists h.
+ split. split. apply le_O_n.
+ unfold double; simpl. rewrite <- plus_n_O. now apply plus_lt_compat.
+ pattern a at 1. rewrite (even_double a EV).
+ pattern (div2 a) at 1. rewrite EQ.
+ rewrite !double_twice, mult_plus_distr_l. f_equal.
+ rewrite mult_assoc, (mult_comm 2), <- mult_assoc. f_equal.
+ exists (S (double l)). exists h.
+ split. split. apply le_O_n.
+ red. red in H.
+ unfold double; simpl. rewrite <- plus_n_O, plus_n_Sm, <- plus_Sn_m.
+ now apply plus_le_compat.
+ rewrite plus_Sn_m.
+ pattern a at 1. rewrite (odd_double a OD). f_equal.
+ pattern (div2 a) at 1. rewrite EQ.
+ rewrite !double_twice, mult_plus_distr_l. f_equal.
+ rewrite mult_assoc, (mult_comm 2), <- mult_assoc. f_equal.
+Qed.
+
+Lemma shiftr_spec : forall a n m,
+ testbit (shiftr a n) m = testbit a (m+n).
+Proof.
+ induction n; intros m. trivial.
+ now rewrite <- plus_n_O.
+ now rewrite <- plus_n_Sm, <- plus_Sn_m, <- IHn.
+Qed.
+
+Lemma shiftl_spec_high : forall a n m, n<=m ->
+ testbit (shiftl a n) m = testbit a (m-n).
+Proof.
+ induction n; intros m H. trivial.
+ now rewrite <- minus_n_O.
+ destruct m. inversion H.
+ simpl. apply le_S_n in H.
+ change (shiftl a (S n)) with (double (shiftl a n)).
+ rewrite double_twice, div2_double. now apply IHn.
+Qed.
+
+Lemma shiftl_spec_low : forall a n m, m<n ->
+ testbit (shiftl a n) m = false.
+Proof.
+ induction n; intros m H. inversion H.
+ change (shiftl a (S n)) with (double (shiftl a n)).
+ destruct m; simpl.
+ unfold odd. apply negb_false_iff.
+ apply even_spec. exists (shiftl a n). apply double_twice.
+ rewrite double_twice, div2_double. apply IHn.
+ now apply lt_S_n.
+Qed.
+
+Lemma div2_bitwise : forall op n a b,
+ div2 (bitwise op (S n) a b) = bitwise op n (div2 a) (div2 b).
+Proof.
+ intros. unfold bitwise; fold bitwise.
+ destruct (op (odd a) (odd b)).
+ now rewrite div2_double_plus_one.
+ now rewrite plus_O_n, div2_double.
+Qed.
+
+Lemma odd_bitwise : forall op n a b,
+ odd (bitwise op (S n) a b) = op (odd a) (odd b).
+Proof.
+ intros. unfold bitwise; fold bitwise.
+ destruct (op (odd a) (odd b)).
+ apply odd_spec. rewrite plus_comm. eexists; eauto.
+ unfold odd. apply negb_false_iff. apply even_spec.
+ rewrite plus_O_n; eexists; eauto.
+Qed.
+
+Lemma div2_decr : forall a n, a <= S n -> div2 a <= n.
+Proof.
+ destruct a; intros. apply le_0_n.
+ apply le_trans with a.
+ apply lt_n_Sm_le, lt_div2, lt_0_Sn. now apply le_S_n.
+Qed.
+
+Lemma testbit_bitwise_1 : forall op, (forall b, op false b = false) ->
+ forall n m a b, a<=n ->
+ testbit (bitwise op n a b) m = op (testbit a m) (testbit b m).
+Proof.
+ intros op Hop.
+ induction n; intros m a b Ha.
+ simpl. inversion Ha; subst. now rewrite testbit_0_l.
+ destruct m.
+ apply odd_bitwise.
+ unfold testbit; fold testbit. rewrite div2_bitwise.
+ apply IHn; now apply div2_decr.
+Qed.
+
+Lemma testbit_bitwise_2 : forall op, op false false = false ->
+ forall n m a b, a<=n -> b<=n ->
+ testbit (bitwise op n a b) m = op (testbit a m) (testbit b m).
+Proof.
+ intros op Hop.
+ induction n; intros m a b Ha Hb.
+ simpl. inversion Ha; inversion Hb; subst. now rewrite testbit_0_l.
+ destruct m.
+ apply odd_bitwise.
+ unfold testbit; fold testbit. rewrite div2_bitwise.
+ apply IHn; now apply div2_decr.
+Qed.
+
+Lemma land_spec : forall a b n,
+ testbit (land a b) n = testbit a n && testbit b n.
+Proof.
+ intros. unfold land. apply testbit_bitwise_1; trivial.
+Qed.
+
+Lemma ldiff_spec : forall a b n,
+ testbit (ldiff a b) n = testbit a n && negb (testbit b n).
+Proof.
+ intros. unfold ldiff. apply testbit_bitwise_1; trivial.
+Qed.
+
+Lemma lor_spec : forall a b n,
+ testbit (lor a b) n = testbit a n || testbit b n.
+Proof.
+ intros. unfold lor. apply testbit_bitwise_2. trivial.
+ destruct (le_ge_dec a b). now rewrite max_r. now rewrite max_l.
+ destruct (le_ge_dec a b). now rewrite max_r. now rewrite max_l.
+Qed.
+
+Lemma lxor_spec : forall a b n,
+ testbit (lxor a b) n = xorb (testbit a n) (testbit b n).
+Proof.
+ intros. unfold lxor. apply testbit_bitwise_2. trivial.
+ destruct (le_ge_dec a b). now rewrite max_r. now rewrite max_l.
+ destruct (le_ge_dec a b). now rewrite max_r. now rewrite max_l.
+Qed.
 
 (** * Implementation of [NAxiomsSig] by [nat] *)
 
@@ -525,6 +725,27 @@ Definition gcd_greatest := gcd_greatest.
 Lemma gcd_nonneg : forall a b, 0<=gcd a b.
 Proof. intros. apply le_O_n. Qed.
 
+Definition testbit := testbit.
+Definition shiftl := shiftl.
+Definition shiftr := shiftr.
+Definition lxor := lxor.
+Definition land := land.
+Definition lor := lor.
+Definition ldiff := ldiff.
+Definition div2 := div2.
+
+Definition testbit_spec a n (_:0<=n) := testbit_spec a n.
+Lemma testbit_neg_r a n (H:n<0) : testbit a n = false.
+Proof. inversion H. Qed.
+Definition shiftl_spec_low := shiftl_spec_low.
+Definition shiftl_spec_high a n m (_:0<=m) := shiftl_spec_high a n m.
+Definition shiftr_spec a n m (_:0<=m) := shiftr_spec a n m.
+Definition lxor_spec := lxor_spec.
+Definition land_spec := land_spec.
+Definition lor_spec := lor_spec.
+Definition ldiff_spec := ldiff_spec.
+Definition div2_spec a : div2 a = shiftr a 1 := eq_refl _.
+
 (** Generic Properties *)
 
 Include NProp
diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v
index dc2d27fa44..021ac29ee1 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSig.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSig.v
@@ -56,10 +56,16 @@ Module Type NType.
  Parameter div : t -> t -> t.
  Parameter modulo : t -> t -> t.
  Parameter gcd : t -> t -> t.
- Parameter shiftr : t -> t -> t.
- Parameter shiftl : t -> t -> t.
  Parameter even : t -> bool.
  Parameter odd : t -> bool.
+ Parameter testbit : t -> t -> bool.
+ Parameter shiftr : t -> t -> t.
+ Parameter shiftl : t -> t -> t.
+ Parameter land : t -> t -> t.
+ Parameter lor : t -> t -> t.
+ Parameter ldiff : t -> t -> t.
+ Parameter lxor : t -> t -> t.
+ Parameter div2 : t -> t.
 
  Parameter spec_compare: forall x y, compare x y = Zcompare [x] [y].
  Parameter spec_eq_bool: forall x y, eq_bool x y = Zeq_bool [x] [y].
@@ -84,10 +90,16 @@ Module Type NType.
  Parameter spec_div: forall x y, [div x y] = [x] / [y].
  Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y].
  Parameter spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b].
- Parameter spec_shiftr: forall p x, [shiftr p x] = [x] / 2^[p].
- Parameter spec_shiftl: forall p x, [shiftl p x] = [x] * 2^[p].
  Parameter spec_even: forall x, even x = Zeven_bool [x].
  Parameter spec_odd: forall x, odd x = Zodd_bool [x].
+ Parameter spec_testbit: forall x p, testbit x p = Ztestbit [x] [p].
+ Parameter spec_shiftr: forall x p, [shiftr x p] = Zshiftr [x] [p].
+ Parameter spec_shiftl: forall x p, [shiftl x p] = Zshiftl [x] [p].
+ Parameter spec_land: forall x y, [land x y] = Zand [x] [y].
+ Parameter spec_lor: forall x y, [lor x y] = Zor [x] [y].
+ Parameter spec_ldiff: forall x y, [ldiff x y] = Zdiff [x] [y].
+ Parameter spec_lxor: forall x y, [lxor x y] = Zxor [x] [y].
+ Parameter spec_div2: forall x, [div2 x] = Zdiv2' [x].
 
 End NType.
 
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 6760cfc81d..a169c009d2 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import ZArith Nnat NAxioms NDiv NSig.
+Require Import ZArith Nnat Ndigits NAxioms NDiv NSig.
 
 (** * The interface [NSig.NType] implies the interface [NAxiomsSig] *)
 
@@ -17,7 +17,8 @@ Hint Rewrite
  spec_0 spec_1 spec_2 spec_succ spec_add spec_mul spec_pred spec_sub
  spec_div spec_modulo spec_gcd spec_compare spec_eq_bool spec_sqrt
  spec_log2 spec_max spec_min spec_pow_pos spec_pow_N spec_pow
- spec_even spec_odd
+ spec_even spec_odd spec_testbit spec_shiftl spec_shiftr
+ spec_land spec_lor spec_ldiff spec_lxor spec_div2 spec_of_N
  : nsimpl.
 Ltac nsimpl := autorewrite with nsimpl.
 Ltac ncongruence := unfold eq, to_N; repeat red; intros; nsimpl; congruence.
@@ -219,7 +220,7 @@ Qed.
 
 Lemma pow_N_pow : forall a b, pow_N a b == a^(of_N b).
 Proof.
- intros. zify. f_equal. symmetry. apply spec_of_N.
+ intros. now zify.
 Qed.
 
 Lemma pow_pos_N : forall a p, pow_pos a p == pow_N a (Npos p).
@@ -266,7 +267,7 @@ Proof.
  rewrite Zeven_bool_iff, Zeven_ex_iff.
  split; intros (m,Hm).
  exists (of_N (Zabs_N m)).
- zify. rewrite spec_of_N, Z_of_N_abs, Zabs_eq; auto.
+ zify. rewrite Z_of_N_abs, Zabs_eq; trivial.
  generalize (spec_pos n); auto with zarith.
  exists [m]. revert Hm. now zify.
 Qed.
@@ -277,7 +278,7 @@ Proof.
  rewrite Zodd_bool_iff, Zodd_ex_iff.
  split; intros (m,Hm).
  exists (of_N (Zabs_N m)).
- zify. rewrite spec_of_N, Z_of_N_abs, Zabs_eq; auto.
+ zify. rewrite Z_of_N_abs, Zabs_eq; trivial.
  generalize (spec_pos n); auto with zarith.
  exists [m]. revert Hm. now zify.
 Qed.
@@ -308,7 +309,7 @@ Proof.
  intros n m. split.
  intros (p,H). exists [p]. revert H; now zify.
  intros (z,H). exists (of_N (Zabs_N z)). zify.
- rewrite spec_of_N, Z_of_N_abs.
+ rewrite Z_of_N_abs.
  rewrite <- (Zabs_eq [n]) by apply spec_pos.
  rewrite <- Zabs_Zmult, H.
  apply Zabs_eq, spec_pos.
@@ -334,6 +335,82 @@ Proof.
  intros. zify. apply Zgcd_nonneg.
 Qed.
 
+(** Bitwise operations *)
+
+Lemma testbit_spec : forall a n, 0<=n ->
+  exists l, exists h, (0<=l /\ l<2^n) /\
+    a == l + ((if testbit a n then 1 else 0) + 2*h)*2^n.
+Proof.
+ intros a n _. zify.
+ assert (Ha := spec_pos a).
+ assert (Hn := spec_pos n).
+ destruct (Ntestbit_spec (Zabs_N [a]) (Zabs_N [n])) as (l & h & (_,Hl) & EQ).
+ exists (of_N l), (of_N h).
+ zify.
+ apply Z_of_N_lt in Hl.
+ apply Z_of_N_eq in EQ.
+ revert Hl EQ.
+ rewrite <- Ztestbit_of_N.
+ rewrite Z_of_N_plus, Z_of_N_mult, <- !Zpower_Npow, Z_of_N_plus,
+  Z_of_N_mult, !Z_of_N_abs, !Zabs_eq by trivial.
+ simpl (Z_of_N 2).
+ repeat split; trivial using Z_of_N_le_0.
+ destruct Ztestbit; now zify.
+Qed.
+
+Lemma testbit_neg_r : forall a n, n<0 -> testbit a n = false.
+Proof.
+ intros a n. zify. apply Ztestbit_neg_r.
+Qed.
+
+Lemma shiftr_spec : forall a n m, 0<=m ->
+ testbit (shiftr a n) m = testbit a (m+n).
+Proof.
+ intros a n m. zify. apply Zshiftr_spec.
+Qed.
+
+Lemma shiftl_spec_high : forall a n m, 0<=m -> n<=m ->
+ testbit (shiftl a n) m = testbit a (m-n).
+Proof.
+ intros a n m. zify. intros Hn H. rewrite Zmax_r by auto with zarith.
+ now apply Zshiftl_spec_high.
+Qed.
+
+Lemma shiftl_spec_low : forall a n m, m<n ->
+ testbit (shiftl a n) m = false.
+Proof.
+ intros a n m. zify. intros H. now apply Zshiftl_spec_low.
+Qed.
+
+Lemma land_spec : forall a b n,
+ testbit (land a b) n = testbit a n && testbit b n.
+Proof.
+ intros a n m. zify. now apply Zand_spec.
+Qed.
+
+Lemma lor_spec : forall a b n,
+ testbit (lor a b) n = testbit a n || testbit b n.
+Proof.
+ intros a n m. zify. now apply Zor_spec.
+Qed.
+
+Lemma ldiff_spec : forall a b n,
+ testbit (ldiff a b) n = testbit a n && negb (testbit b n).
+Proof.
+ intros a n m. zify. now apply Zdiff_spec.
+Qed.
+
+Lemma lxor_spec : forall a b n,
+ testbit (lxor a b) n = xorb (testbit a n) (testbit b n).
+Proof.
+ intros a n m. zify. now apply Zxor_spec.
+Qed.
+
+Lemma div2_spec : forall a, div2 a == shiftr a 1.
+Proof.
+ intros a. zify. now apply Zdiv2'_spec.
+Qed.
+
 (** Recursion *)
 
 Definition recursion (A : Type) (a : A) (f : N.t -> A -> A) (n : N.t) :=