Ndigits.v

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

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

Require Import Bool Morphisms Setoid Bvector BinPos BinNat PeanoNat Pnat Nnat
        Basics ByteVector.

Local Open Scope N_scope.
Local Open Scope program_scope.

This file is mostly obsolete, see directly BinNat now.

Compatibility names for some bitwise operations

Notation Pxor := Pos.lxor (only parsing).
Notation Nxor := N.lxor (only parsing).
Notation Pbit := Pos.testbit_nat (only parsing).
Notation Nbit := N.testbit_nat (only parsing).

Notation Nxor_eq := N.lxor_eq (only parsing).
Notation Nxor_comm := N.lxor_comm (only parsing).
Notation Nxor_assoc := N.lxor_assoc (only parsing).
Notation Nxor_neutral_left := N.lxor_0_l (only parsing).
Notation Nxor_neutral_right := N.lxor_0_r (only parsing).
Notation Nxor_nilpotent := N.lxor_nilpotent (only parsing).

Equivalence of bit-testing functions, either with index in N or in nat.

Lemma Ptestbit_Pbit :
 forall p n, Pos.testbit p (N.of_nat n) = Pos.testbit_nat p n.forall (p : positive) (n : nat),
Pos.testbit p (N.of_nat n) = Pos.testbit_nat p n
Proof.forall (p : positive) (n : nat),
Pos.testbit p (N.of_nat n) = Pos.testbit_nat p n
 induction p as [p IH|p IH| ]; intros [|n]; simpl; trivial;
  rewrite <- IH; f_equal; rewrite (pred_Sn n) at 2; now rewrite Nat2N.inj_pred.
Qed.

Lemma Ntestbit_Nbit : forall a n, N.testbit a (N.of_nat n) = N.testbit_nat a n.forall (a : N) (n : nat),
N.testbit a (N.of_nat n) = N.testbit_nat a n
Proof.forall (a : N) (n : nat),
N.testbit a (N.of_nat n) = N.testbit_nat a n
 destruct a.forall n : nat,
N.testbit 0 (N.of_nat n) = N.testbit_nat 0 n
p:positive
forall n : nat,
N.testbit (N.pos p) (N.of_nat n) =
N.testbit_nat (N.pos p) n trivial.p:positive
forall n : nat,
N.testbit (N.pos p) (N.of_nat n) =
N.testbit_nat (N.pos p) n apply Ptestbit_Pbit.
Qed.

Lemma Pbit_Ptestbit :
 forall p n, Pos.testbit_nat p (N.to_nat n) = Pos.testbit p n.forall (p : positive) (n : N),
Pos.testbit_nat p (N.to_nat n) = Pos.testbit p n
Proof.forall (p : positive) (n : N),
Pos.testbit_nat p (N.to_nat n) = Pos.testbit p n
 intros; now rewrite <- Ptestbit_Pbit, N2Nat.id.
Qed.

Lemma Nbit_Ntestbit :
 forall a n, N.testbit_nat a (N.to_nat n) = N.testbit a n.forall a n : N,
N.testbit_nat a (N.to_nat n) = N.testbit a n
Proof.forall a n : N,
N.testbit_nat a (N.to_nat n) = N.testbit a n
 destruct a.forall n : N,
N.testbit_nat 0 (N.to_nat n) = N.testbit 0 n
p:positive
forall n : N,
N.testbit_nat (N.pos p) (N.to_nat n) =
N.testbit (N.pos p) n trivial.p:positive
forall n : N,
N.testbit_nat (N.pos p) (N.to_nat n) =
N.testbit (N.pos p) n apply Pbit_Ptestbit.
Qed.

Equivalence of shifts, index in N or nat

Lemma Nshiftr_nat_S : forall a n,
 N.shiftr_nat a (S n) = N.div2 (N.shiftr_nat a n).forall (a : N) (n : nat),
N.shiftr_nat a (S n) = N.div2 (N.shiftr_nat a n)
Proof.forall (a : N) (n : nat),
N.shiftr_nat a (S n) = N.div2 (N.shiftr_nat a n)
 reflexivity.
Qed.

Lemma Nshiftl_nat_S : forall a n,
 N.shiftl_nat a (S n) = N.double (N.shiftl_nat a n).forall (a : N) (n : nat),
N.shiftl_nat a (S n) = N.double (N.shiftl_nat a n)
Proof.forall (a : N) (n : nat),
N.shiftl_nat a (S n) = N.double (N.shiftl_nat a n)
 reflexivity.
Qed.

Lemma Nshiftr_nat_equiv :
 forall a n, N.shiftr_nat a (N.to_nat n) = N.shiftr a n.forall a n : N,
N.shiftr_nat a (N.to_nat n) = N.shiftr a n
Proof.forall a n : N,
N.shiftr_nat a (N.to_nat n) = N.shiftr a n
 intros a [|n]; simpl.a:N
a = a
a:N
n:positive
N.shiftr_nat a (Pos.to_nat n) = Pos.iter N.div2 a n unfold N.shiftr_nat.a:N
a = a
a:N
n:positive
N.shiftr_nat a (Pos.to_nat n) = Pos.iter N.div2 a n
 trivial.a:N
n:positive
N.shiftr_nat a (Pos.to_nat n) = Pos.iter N.div2 a n
 symmetry.a:N
n:positive
Pos.iter N.div2 a n = N.shiftr_nat a (Pos.to_nat n) apply Pos2Nat.inj_iter.
Qed.

Lemma Nshiftr_equiv_nat :
 forall a n, N.shiftr a (N.of_nat n) = N.shiftr_nat a n.forall (a : N) (n : nat),
N.shiftr a (N.of_nat n) = N.shiftr_nat a n
Proof.forall (a : N) (n : nat),
N.shiftr a (N.of_nat n) = N.shiftr_nat a n
 intros.a:N
n:nat
N.shiftr a (N.of_nat n) = N.shiftr_nat a n now rewrite <- Nshiftr_nat_equiv, Nat2N.id.
Qed.

Lemma Nshiftl_nat_equiv :
 forall a n, N.shiftl_nat a (N.to_nat n) = N.shiftl a n.forall a n : N,
N.shiftl_nat a (N.to_nat n) = N.shiftl a n
Proof.forall a n : N,
N.shiftl_nat a (N.to_nat n) = N.shiftl a n
 intros [|a] [|n]; simpl; unfold N.shiftl_nat; trivial.n:positive
nat_rect (fun _ : nat => N) 0
  (fun _ : nat => N.double) (Pos.to_nat n) = 0
a, n:positive
nat_rect (fun _ : nat => N) (N.pos a)
  (fun _ : nat => N.double) (Pos.to_nat n) =
N.pos (Pos.iter xO a n)
 induction (Pos.to_nat n) as [|? H]; simpl; now try rewrite H.a, n:positive
nat_rect (fun _ : nat => N) (N.pos a)
  (fun _ : nat => N.double) (Pos.to_nat n) =
N.pos (Pos.iter xO a n)
 rewrite <- Pos2Nat.inj_iter.a, n:positive
Pos.iter N.double (N.pos a) n =
N.pos (Pos.iter xO a n) symmetry.a, n:positive
N.pos (Pos.iter xO a n) =
Pos.iter N.double (N.pos a) n now apply Pos.iter_swap_gen.
Qed.

Lemma Nshiftl_equiv_nat :
 forall a n, N.shiftl a (N.of_nat n) = N.shiftl_nat a n.forall (a : N) (n : nat),
N.shiftl a (N.of_nat n) = N.shiftl_nat a n
Proof.forall (a : N) (n : nat),
N.shiftl a (N.of_nat n) = N.shiftl_nat a n
 intros.a:N
n:nat
N.shiftl a (N.of_nat n) = N.shiftl_nat a n now rewrite <- Nshiftl_nat_equiv, Nat2N.id.
Qed.

Correctness proofs for shifts, nat version

Lemma Nshiftr_nat_spec : forall a n m,
  N.testbit_nat (N.shiftr_nat a n) m = N.testbit_nat a (m+n).forall (a : N) (n m : nat),
N.testbit_nat (N.shiftr_nat a n) m =
N.testbit_nat a (m + n)
Proof.forall (a : N) (n m : nat),
N.testbit_nat (N.shiftr_nat a n) m =
N.testbit_nat a (m + n)
 induction n; intros m.a:N
m:nat
N.testbit_nat (N.shiftr_nat a 0) m =
N.testbit_nat a (m + 0)
a:N
n:nat
IHn:forall m0 : nat,
N.testbit_nat (N.shiftr_nat a n) m0 = N.testbit_nat a (m0 + n)
m:nat
N.testbit_nat (N.shiftr_nat a (S n)) m =
N.testbit_nat a (m + S n)
 now rewrite <- plus_n_O.a:N
n:nat
IHn:forall m0 : nat,
N.testbit_nat (N.shiftr_nat a n) m0 = N.testbit_nat a (m0 + n)
m:nat
N.testbit_nat (N.shiftr_nat a (S n)) m =
N.testbit_nat a (m + S n)
 simpl.a:N
n:nat
IHn:forall m0 : nat,
N.testbit_nat (N.shiftr_nat a n) m0 = N.testbit_nat a (m0 + n)
m:nat
N.testbit_nat (N.div2 (N.shiftr_nat a n)) m =
N.testbit_nat a (m + S n) rewrite <- plus_n_Sm, <- plus_Sn_m, <- IHn.a:N
n:nat
IHn:forall m0 : nat,
N.testbit_nat (N.shiftr_nat a n) m0 = N.testbit_nat a (m0 + n)
m:nat
N.testbit_nat (N.div2 (N.shiftr_nat a n)) m =
N.testbit_nat (N.shiftr_nat a n) (S m)
 destruct (N.shiftr_nat a n) as [|[p|p|]]; simpl; trivial.
Qed.

Lemma Nshiftl_nat_spec_high : forall a n m, (n<=m)%nat ->
  N.testbit_nat (N.shiftl_nat a n) m = N.testbit_nat a (m-n).forall (a : N) (n m : nat),
(n <= m)%nat ->
N.testbit_nat (N.shiftl_nat a n) m =
N.testbit_nat a (m - n)
Proof.forall (a : N) (n m : nat),
(n <= m)%nat ->
N.testbit_nat (N.shiftl_nat a n) m =
N.testbit_nat a (m - n)
 induction n; intros m H.a:N
m:nat
H:(0 <= m)%nat
N.testbit_nat (N.shiftl_nat a 0) m =
N.testbit_nat a (m - 0)
a:N
n:nat
IHn:forall m0 : nat,
(n <= m0)%nat ->
N.testbit_nat (N.shiftl_nat a n) m0 = N.testbit_nat a (m0 - n)
m:nat
H:(S n <= m)%nat
N.testbit_nat (N.shiftl_nat a (S n)) m =
N.testbit_nat a (m - S n)
 -a:N
m:nat
H:(0 <= m)%nat
N.testbit_nat (N.shiftl_nat a 0) m =
N.testbit_nat a (m - 0) now rewrite Nat.sub_0_r.
 -a:N
n:nat
IHn:forall m0 : nat,
(n <= m0)%nat ->
N.testbit_nat (N.shiftl_nat a n) m0 = N.testbit_nat a (m0 - n)
m:nat
H:(S n <= m)%nat
N.testbit_nat (N.shiftl_nat a (S n)) m =
N.testbit_nat a (m - S n) destruct m.a:N
n:nat
IHn:forall m : nat,
(n <= m)%nat -> N.testbit_nat (N.shiftl_nat a n) m = N.testbit_nat a (m - n)
H:(S n <= 0)%nat
N.testbit_nat (N.shiftl_nat a (S n)) 0 =
N.testbit_nat a (0 - S n)
a:N
n:nat
IHn:forall m0 : nat,
(n <= m0)%nat ->
N.testbit_nat (N.shiftl_nat a n) m0 = N.testbit_nat a (m0 - n)
m:nat
H:(S n <= S m)%nat
N.testbit_nat (N.shiftl_nat a (S n)) (S m) =
N.testbit_nat a (S m - S n)
   +a:N
n:nat
IHn:forall m : nat,
(n <= m)%nat -> N.testbit_nat (N.shiftl_nat a n) m = N.testbit_nat a (m - n)
H:(S n <= 0)%nat
N.testbit_nat (N.shiftl_nat a (S n)) 0 =
N.testbit_nat a (0 - S n) inversion H.
   +a:N
n:nat
IHn:forall m0 : nat,
(n <= m0)%nat ->
N.testbit_nat (N.shiftl_nat a n) m0 = N.testbit_nat a (m0 - n)
m:nat
H:(S n <= S m)%nat
N.testbit_nat (N.shiftl_nat a (S n)) (S m) =
N.testbit_nat a (S m - S n) apply le_S_n in H.a:N
n:nat
IHn:forall m0 : nat,
(n <= m0)%nat ->
N.testbit_nat (N.shiftl_nat a n) m0 = N.testbit_nat a (m0 - n)
m:nat
H:(n <= m)%nat
N.testbit_nat (N.shiftl_nat a (S n)) (S m) =
N.testbit_nat a (S m - S n)
     simpl.a:N
n:nat
IHn:forall m0 : nat,
(n <= m0)%nat ->
N.testbit_nat (N.shiftl_nat a n) m0 = N.testbit_nat a (m0 - n)
m:nat
H:(n <= m)%nat
N.testbit_nat (N.double (N.shiftl_nat a n)) (S m) =
N.testbit_nat a (m - n) rewrite <- IHn; trivial.a:N
n:nat
IHn:forall m0 : nat,
(n <= m0)%nat ->
N.testbit_nat (N.shiftl_nat a n) m0 = N.testbit_nat a (m0 - n)
m:nat
H:(n <= m)%nat
N.testbit_nat (N.double (N.shiftl_nat a n)) (S m) =
N.testbit_nat (N.shiftl_nat a n) m
     destruct (N.shiftl_nat a n) as [|[p|p|]]; simpl; trivial.
Qed.

Lemma Nshiftl_nat_spec_low : forall a n m, (m<n)%nat ->
 N.testbit_nat (N.shiftl_nat a n) m = false.forall (a : N) (n m : nat),
(m < n)%nat ->
N.testbit_nat (N.shiftl_nat a n) m = false
Proof.forall (a : N) (n m : nat),
(m < n)%nat ->
N.testbit_nat (N.shiftl_nat a n) m = false
 induction n; intros m H.a:N
m:nat
H:(m < 0)%nat
N.testbit_nat (N.shiftl_nat a 0) m = false
a:N
n:nat
IHn:forall m0 : nat, (m0 < n)%nat -> N.testbit_nat (N.shiftl_nat a n) m0 = false
m:nat
H:(m < S n)%nat
N.testbit_nat (N.shiftl_nat a (S n)) m = false inversion H.a:N
n:nat
IHn:forall m0 : nat, (m0 < n)%nat -> N.testbit_nat (N.shiftl_nat a n) m0 = false
m:nat
H:(m < S n)%nat
N.testbit_nat (N.shiftl_nat a (S n)) m = false
 rewrite Nshiftl_nat_S.a:N
n:nat
IHn:forall m0 : nat, (m0 < n)%nat -> N.testbit_nat (N.shiftl_nat a n) m0 = false
m:nat
H:(m < S n)%nat
N.testbit_nat (N.double (N.shiftl_nat a n)) m = false
 destruct m.a:N
n:nat
IHn:forall m : nat, (m < n)%nat -> N.testbit_nat (N.shiftl_nat a n) m = false
H:(0 < S n)%nat
N.testbit_nat (N.double (N.shiftl_nat a n)) 0 = false
a:N
n:nat
IHn:forall m0 : nat, (m0 < n)%nat -> N.testbit_nat (N.shiftl_nat a n) m0 = false
m:nat
H:(S m < S n)%nat
N.testbit_nat (N.double (N.shiftl_nat a n)) (S m) =
false
 -a:N
n:nat
IHn:forall m : nat, (m < n)%nat -> N.testbit_nat (N.shiftl_nat a n) m = false
H:(0 < S n)%nat
N.testbit_nat (N.double (N.shiftl_nat a n)) 0 = false destruct (N.shiftl_nat a n); trivial.
 -a:N
n:nat
IHn:forall m0 : nat, (m0 < n)%nat -> N.testbit_nat (N.shiftl_nat a n) m0 = false
m:nat
H:(S m < S n)%nat
N.testbit_nat (N.double (N.shiftl_nat a n)) (S m) =
false apply Lt.lt_S_n in H.a:N
n:nat
IHn:forall m0 : nat, (m0 < n)%nat -> N.testbit_nat (N.shiftl_nat a n) m0 = false
m:nat
H:(m < n)%nat
N.testbit_nat (N.double (N.shiftl_nat a n)) (S m) =
false
   specialize (IHn m H).a:N
n, m:nat
IHn:N.testbit_nat (N.shiftl_nat a n) m = false
H:(m < n)%nat
N.testbit_nat (N.double (N.shiftl_nat a n)) (S m) =
false
   destruct (N.shiftl_nat a n); trivial.
Qed.

A left shift for positive numbers (used in BigN)

Lemma Pshiftl_nat_0 : forall p, Pos.shiftl_nat p 0 = p.forall p : positive, Pos.shiftl_nat p 0 = p
Proof.forall p : positive, Pos.shiftl_nat p 0 = p reflexivity. Qed.

Lemma Pshiftl_nat_S :
 forall p n, Pos.shiftl_nat p (S n) = xO (Pos.shiftl_nat p n).forall (p : positive) (n : nat),
Pos.shiftl_nat p (S n) =
((Pos.shiftl_nat p n)~0)%positive
Proof.forall (p : positive) (n : nat),
Pos.shiftl_nat p (S n) =
((Pos.shiftl_nat p n)~0)%positive reflexivity. Qed.

Lemma Pshiftl_nat_N :
 forall p n, Npos (Pos.shiftl_nat p n) = N.shiftl_nat (Npos p) n.forall (p : positive) (n : nat),
N.pos (Pos.shiftl_nat p n) = N.shiftl_nat (N.pos p) n
Proof.forall (p : positive) (n : nat),
N.pos (Pos.shiftl_nat p n) = N.shiftl_nat (N.pos p) n
 unfold Pos.shiftl_nat, N.shiftl_nat.forall (p : positive) (n : nat),
N.pos
  (nat_rect (fun _ : nat => positive) p
     (fun _ : nat => xO) n) =
nat_rect (fun _ : nat => N) (N.pos p)
  (fun _ : nat => N.double) n
 induction n; simpl; auto.p:positive
n:nat
IHn:N.pos (nat_rect (fun _ : nat => positive) p (fun _ : nat => xO) n) =
nat_rect (fun _ : nat => N) (N.pos p) (fun _ : nat => N.double) n
N.pos
  (nat_rect (fun _ : nat => positive) p
     (fun _ : nat => xO) n)~0 =
N.double
  (nat_rect (fun _ : nat => N) (N.pos p)
     (fun _ : nat => N.double) n) now rewrite <- IHn.
Qed.

Lemma Pshiftl_nat_plus : forall n m p,
  Pos.shiftl_nat p (m + n) = Pos.shiftl_nat (Pos.shiftl_nat p n) m.forall (n m : nat) (p : positive),
Pos.shiftl_nat p (m + n) =
Pos.shiftl_nat (Pos.shiftl_nat p n) m
Proof.forall (n m : nat) (p : positive),
Pos.shiftl_nat p (m + n) =
Pos.shiftl_nat (Pos.shiftl_nat p n) m
 induction m; simpl; intros.n:nat
p:positive
Pos.shiftl_nat p n = Pos.shiftl_nat p n
n, m:nat
IHm:forall p0 : positive,
Pos.shiftl_nat p0 (m + n) = Pos.shiftl_nat (Pos.shiftl_nat p0 n) m
p:positive
((Pos.shiftl_nat p (m + n))~0)%positive =
((Pos.shiftl_nat (Pos.shiftl_nat p n) m)~0)%positive reflexivity.n, m:nat
IHm:forall p0 : positive,
Pos.shiftl_nat p0 (m + n) = Pos.shiftl_nat (Pos.shiftl_nat p0 n) m
p:positive
((Pos.shiftl_nat p (m + n))~0)%positive =
((Pos.shiftl_nat (Pos.shiftl_nat p n) m)~0)%positive
 now f_equal.
Qed.

Semantics of bitwise operations with respect to N.testbit_nat

Lemma Pxor_semantics p p' n :
 N.testbit_nat (Pos.lxor p p') n = xorb (Pos.testbit_nat p n) (Pos.testbit_nat p' n).p, p':positive
n:nat
N.testbit_nat (Pos.lxor p p') n =
xorb (Pos.testbit_nat p n) (Pos.testbit_nat p' n)
Proof.p, p':positive
n:nat
N.testbit_nat (Pos.lxor p p') n =
xorb (Pos.testbit_nat p n) (Pos.testbit_nat p' n)
 rewrite <- Ntestbit_Nbit, <- !Ptestbit_Pbit.p, p':positive
n:nat
N.testbit (Pos.lxor p p') (N.of_nat n) =
xorb (Pos.testbit p (N.of_nat n))
  (Pos.testbit p' (N.of_nat n)) apply N.pos_lxor_spec.
Qed.

Lemma Nxor_semantics a a' n :
 N.testbit_nat (N.lxor a a') n = xorb (N.testbit_nat a n) (N.testbit_nat a' n).a, a':N
n:nat
N.testbit_nat (N.lxor a a') n =
xorb (N.testbit_nat a n) (N.testbit_nat a' n)
Proof.a, a':N
n:nat
N.testbit_nat (N.lxor a a') n =
xorb (N.testbit_nat a n) (N.testbit_nat a' n)
 rewrite <- !Ntestbit_Nbit.a, a':N
n:nat
N.testbit (N.lxor a a') (N.of_nat n) =
xorb (N.testbit a (N.of_nat n))
  (N.testbit a' (N.of_nat n)) apply N.lxor_spec.
Qed.

Lemma Por_semantics p p' n :
 Pos.testbit_nat (Pos.lor p p') n = (Pos.testbit_nat p n) || (Pos.testbit_nat p' n).p, p':positive
n:nat
Pos.testbit_nat (Pos.lor p p') n =
Pos.testbit_nat p n || Pos.testbit_nat p' n
Proof.p, p':positive
n:nat
Pos.testbit_nat (Pos.lor p p') n =
Pos.testbit_nat p n || Pos.testbit_nat p' n
 rewrite <- !Ptestbit_Pbit.p, p':positive
n:nat
Pos.testbit (Pos.lor p p') (N.of_nat n) =
Pos.testbit p (N.of_nat n)
|| Pos.testbit p' (N.of_nat n) apply N.pos_lor_spec.
Qed.

Lemma Nor_semantics a a' n :
 N.testbit_nat (N.lor a a') n = (N.testbit_nat a n) || (N.testbit_nat a' n).a, a':N
n:nat
N.testbit_nat (N.lor a a') n =
N.testbit_nat a n || N.testbit_nat a' n
Proof.a, a':N
n:nat
N.testbit_nat (N.lor a a') n =
N.testbit_nat a n || N.testbit_nat a' n
 rewrite <- !Ntestbit_Nbit.a, a':N
n:nat
N.testbit (N.lor a a') (N.of_nat n) =
N.testbit a (N.of_nat n) || N.testbit a' (N.of_nat n) apply N.lor_spec.
Qed.

Lemma Pand_semantics p p' n :
 N.testbit_nat (Pos.land p p') n = (Pos.testbit_nat p n) && (Pos.testbit_nat p' n).p, p':positive
n:nat
N.testbit_nat (Pos.land p p') n =
Pos.testbit_nat p n && Pos.testbit_nat p' n
Proof.p, p':positive
n:nat
N.testbit_nat (Pos.land p p') n =
Pos.testbit_nat p n && Pos.testbit_nat p' n
 rewrite <- Ntestbit_Nbit, <- !Ptestbit_Pbit.p, p':positive
n:nat
N.testbit (Pos.land p p') (N.of_nat n) =
Pos.testbit p (N.of_nat n) &&
Pos.testbit p' (N.of_nat n) apply N.pos_land_spec.
Qed.

Lemma Nand_semantics a a' n :
 N.testbit_nat (N.land a a') n = (N.testbit_nat a n) && (N.testbit_nat a' n).a, a':N
n:nat
N.testbit_nat (N.land a a') n =
N.testbit_nat a n && N.testbit_nat a' n
Proof.a, a':N
n:nat
N.testbit_nat (N.land a a') n =
N.testbit_nat a n && N.testbit_nat a' n
 rewrite <- !Ntestbit_Nbit.a, a':N
n:nat
N.testbit (N.land a a') (N.of_nat n) =
N.testbit a (N.of_nat n) && N.testbit a' (N.of_nat n) apply N.land_spec.
Qed.

Lemma Pdiff_semantics p p' n :
 N.testbit_nat (Pos.ldiff p p') n = (Pos.testbit_nat p n) && negb (Pos.testbit_nat p' n).p, p':positive
n:nat
N.testbit_nat (Pos.ldiff p p') n =
Pos.testbit_nat p n && negb (Pos.testbit_nat p' n)
Proof.p, p':positive
n:nat
N.testbit_nat (Pos.ldiff p p') n =
Pos.testbit_nat p n && negb (Pos.testbit_nat p' n)
 rewrite <- Ntestbit_Nbit, <- !Ptestbit_Pbit.p, p':positive
n:nat
N.testbit (Pos.ldiff p p') (N.of_nat n) =
Pos.testbit p (N.of_nat n) &&
negb (Pos.testbit p' (N.of_nat n)) apply N.pos_ldiff_spec.
Qed.

Lemma Ndiff_semantics a a' n :
 N.testbit_nat (N.ldiff a a') n = (N.testbit_nat a n) && negb (N.testbit_nat a' n).a, a':N
n:nat
N.testbit_nat (N.ldiff a a') n =
N.testbit_nat a n && negb (N.testbit_nat a' n)
Proof.a, a':N
n:nat
N.testbit_nat (N.ldiff a a') n =
N.testbit_nat a n && negb (N.testbit_nat a' n)
 rewrite <- !Ntestbit_Nbit.a, a':N
n:nat
N.testbit (N.ldiff a a') (N.of_nat n) =
N.testbit a (N.of_nat n) &&
negb (N.testbit a' (N.of_nat n)) apply N.ldiff_spec.
Qed.

Equality over functional streams of bits

Definition eqf (f g:nat -> bool) := forall n:nat, f n = g n.

Instance eqf_equiv : Equivalence eqf.

Local Infix "==" := eqf (at level 70, no associativity).

If two numbers produce the same stream of bits, they are equal.

Notation Step H := (fun n => H (S n)).

Lemma Pbit_faithful_0 : forall p, ~(Pos.testbit_nat p == (fun _ => false)).forall p : positive,
~ Pos.testbit_nat p == (fun _ : nat => false)
Proof.forall p : positive,
~ Pos.testbit_nat p == (fun _ : nat => false)
 induction p as [p IHp|p IHp| ]; intros H; try discriminate (H O).p:positive
IHp:~ Pos.testbit_nat p == (fun _ : nat => false)
H:Pos.testbit_nat p~0 == (fun _ : nat => false)
False
  apply (IHp (Step H)).
Qed.

Lemma Pbit_faithful : forall p p', Pos.testbit_nat p == Pos.testbit_nat p' -> p = p'.forall p p' : positive,
Pos.testbit_nat p == Pos.testbit_nat p' -> p = p'
Proof.forall p p' : positive,
Pos.testbit_nat p == Pos.testbit_nat p' -> p = p'
 induction p as [p IHp|p IHp| ]; intros [p'|p'|] H; trivial;
  try discriminate (H O).p:positive
IHp:forall p'0 : positive, Pos.testbit_nat p == Pos.testbit_nat p'0 -> p = p'0
p':positive
H:Pos.testbit_nat p~1 == Pos.testbit_nat p'~1
(p~1)%positive = (p'~1)%positive
p:positive
IHp:forall p' : positive, Pos.testbit_nat p == Pos.testbit_nat p' -> p = p'
H:Pos.testbit_nat p~1 == Pos.testbit_nat 1
(p~1)%positive = 1%positive
p:positive
IHp:forall p'0 : positive, Pos.testbit_nat p == Pos.testbit_nat p'0 -> p = p'0
p':positive
H:Pos.testbit_nat p~0 == Pos.testbit_nat p'~0
(p~0)%positive = (p'~0)%positive
p':positive
H:Pos.testbit_nat 1 == Pos.testbit_nat p'~1
1%positive = (p'~1)%positive
 f_equal.p:positive
IHp:forall p'0 : positive, Pos.testbit_nat p == Pos.testbit_nat p'0 -> p = p'0
p':positive
H:Pos.testbit_nat p~1 == Pos.testbit_nat p'~1
p = p'
p:positive
IHp:forall p' : positive, Pos.testbit_nat p == Pos.testbit_nat p' -> p = p'
H:Pos.testbit_nat p~1 == Pos.testbit_nat 1
(p~1)%positive = 1%positive
p:positive
IHp:forall p'0 : positive, Pos.testbit_nat p == Pos.testbit_nat p'0 -> p = p'0
p':positive
H:Pos.testbit_nat p~0 == Pos.testbit_nat p'~0
(p~0)%positive = (p'~0)%positive
p':positive
H:Pos.testbit_nat 1 == Pos.testbit_nat p'~1
1%positive = (p'~1)%positive apply (IHp _ (Step H)).p:positive
IHp:forall p' : positive, Pos.testbit_nat p == Pos.testbit_nat p' -> p = p'
H:Pos.testbit_nat p~1 == Pos.testbit_nat 1
(p~1)%positive = 1%positive
p:positive
IHp:forall p'0 : positive, Pos.testbit_nat p == Pos.testbit_nat p'0 -> p = p'0
p':positive
H:Pos.testbit_nat p~0 == Pos.testbit_nat p'~0
(p~0)%positive = (p'~0)%positive
p':positive
H:Pos.testbit_nat 1 == Pos.testbit_nat p'~1
1%positive = (p'~1)%positive
 destruct (Pbit_faithful_0 _ (Step H)).p:positive
IHp:forall p'0 : positive, Pos.testbit_nat p == Pos.testbit_nat p'0 -> p = p'0
p':positive
H:Pos.testbit_nat p~0 == Pos.testbit_nat p'~0
(p~0)%positive = (p'~0)%positive
p':positive
H:Pos.testbit_nat 1 == Pos.testbit_nat p'~1
1%positive = (p'~1)%positive
 f_equal.p:positive
IHp:forall p'0 : positive, Pos.testbit_nat p == Pos.testbit_nat p'0 -> p = p'0
p':positive
H:Pos.testbit_nat p~0 == Pos.testbit_nat p'~0
p = p'
p':positive
H:Pos.testbit_nat 1 == Pos.testbit_nat p'~1
1%positive = (p'~1)%positive apply (IHp _ (Step H)).p':positive
H:Pos.testbit_nat 1 == Pos.testbit_nat p'~1
1%positive = (p'~1)%positive
 symmetry in H.p':positive
H:Pos.testbit_nat p'~1 == Pos.testbit_nat 1
1%positive = (p'~1)%positive destruct (Pbit_faithful_0 _ (Step H)).
Qed.

Lemma Nbit_faithful : forall n n', N.testbit_nat n == N.testbit_nat n' -> n = n'.forall n n' : N,
N.testbit_nat n == N.testbit_nat n' -> n = n'
Proof.forall n n' : N,
N.testbit_nat n == N.testbit_nat n' -> n = n'
 intros [|p] [|p'] H; trivial.p':positive
H:N.testbit_nat 0 == N.testbit_nat (N.pos p')
0 = N.pos p'
p:positive
H:N.testbit_nat (N.pos p) == N.testbit_nat 0
N.pos p = 0
p, p':positive
H:N.testbit_nat (N.pos p) ==
N.testbit_nat (N.pos p')
N.pos p = N.pos p'
 symmetry in H.p':positive
H:N.testbit_nat (N.pos p') == N.testbit_nat 0
0 = N.pos p'
p:positive
H:N.testbit_nat (N.pos p) == N.testbit_nat 0
N.pos p = 0
p, p':positive
H:N.testbit_nat (N.pos p) ==
N.testbit_nat (N.pos p')
N.pos p = N.pos p' destruct (Pbit_faithful_0 _ H).p:positive
H:N.testbit_nat (N.pos p) == N.testbit_nat 0
N.pos p = 0
p, p':positive
H:N.testbit_nat (N.pos p) ==
N.testbit_nat (N.pos p')
N.pos p = N.pos p'
 destruct (Pbit_faithful_0 _ H).p, p':positive
H:N.testbit_nat (N.pos p) ==
N.testbit_nat (N.pos p')
N.pos p = N.pos p'
 f_equal.p, p':positive
H:N.testbit_nat (N.pos p) ==
N.testbit_nat (N.pos p')
p = p' apply Pbit_faithful, H.
Qed.

Lemma Nbit_faithful_iff : forall n n', N.testbit_nat n == N.testbit_nat n' <-> n = n'.forall n n' : N,
N.testbit_nat n == N.testbit_nat n' <-> n = n'
Proof.forall n n' : N,
N.testbit_nat n == N.testbit_nat n' <-> n = n'
 split.n, n':N
N.testbit_nat n == N.testbit_nat n' -> n = n'
n, n':N
n = n' -> N.testbit_nat n == N.testbit_nat n' apply Nbit_faithful.n, n':N
n = n' -> N.testbit_nat n == N.testbit_nat n' intros; now subst.
Qed.

Local Close Scope N_scope.

Checking whether a number is odd, i.e. if its lower bit is set.

Notation Nbit0 := N.odd (only parsing).

Definition Nodd (n:N) := N.odd n = true.
Definition Neven (n:N) := N.odd n = false.

Lemma Nbit0_correct : forall n:N, N.testbit_nat n 0 = N.odd n.forall n : N, N.testbit_nat n 0 = N.odd n
Proof.forall n : N, N.testbit_nat n 0 = N.odd n
  destruct n; trivial.p:positive
N.testbit_nat (N.pos p) 0 = N.odd (N.pos p)
  destruct p; trivial.
Qed.

Lemma Ndouble_bit0 : forall n:N, N.odd (N.double n) = false.forall n : N, N.odd (N.double n) = false
Proof.forall n : N, N.odd (N.double n) = false
  destruct n; trivial.
Qed.

Lemma Ndouble_plus_one_bit0 :
 forall n:N, N.odd (N.succ_double n) = true.forall n : N, N.odd (N.succ_double n) = true
Proof.forall n : N, N.odd (N.succ_double n) = true
  destruct n; trivial.
Qed.

Lemma Ndiv2_double :
 forall n:N, Neven n -> N.double (N.div2 n) = n.forall n : N, Neven n -> N.double (N.div2 n) = n
Proof.forall n : N, Neven n -> N.double (N.div2 n) = n
  destruct n.Neven 0 -> N.double (N.div2 0) = 0%N
p:positive
Neven (N.pos p) ->
N.double (N.div2 (N.pos p)) = N.pos p trivial.p:positive
Neven (N.pos p) ->
N.double (N.div2 (N.pos p)) = N.pos p destruct p.p:positive
Neven (N.pos p~1) ->
N.double (N.div2 (N.pos p~1)) = N.pos p~1
p:positive
Neven (N.pos p~0) ->
N.double (N.div2 (N.pos p~0)) = N.pos p~0
Neven 1 -> N.double (N.div2 1) = 1%N intro H.p:positive
H:Neven (N.pos p~1)
N.double (N.div2 (N.pos p~1)) = N.pos p~1
p:positive
Neven (N.pos p~0) ->
N.double (N.div2 (N.pos p~0)) = N.pos p~0
Neven 1 -> N.double (N.div2 1) = 1%N discriminate H.p:positive
Neven (N.pos p~0) ->
N.double (N.div2 (N.pos p~0)) = N.pos p~0
Neven 1 -> N.double (N.div2 1) = 1%N
  intros.p:positive
H:Neven (N.pos p~0)
N.double (N.div2 (N.pos p~0)) = N.pos p~0
Neven 1 -> N.double (N.div2 1) = 1%N reflexivity.Neven 1 -> N.double (N.div2 1) = 1%N
  intro H.H:Neven 1
N.double (N.div2 1) = 1%N discriminate H.
Qed.

Lemma Ndiv2_double_plus_one :
 forall n:N, Nodd n -> N.succ_double (N.div2 n) = n.forall n : N, Nodd n -> N.succ_double (N.div2 n) = n
Proof.forall n : N, Nodd n -> N.succ_double (N.div2 n) = n
  destruct n.Nodd 0 -> N.succ_double (N.div2 0) = 0%N
p:positive
Nodd (N.pos p) ->
N.succ_double (N.div2 (N.pos p)) = N.pos p intro.H:Nodd 0
N.succ_double (N.div2 0) = 0%N
p:positive
Nodd (N.pos p) ->
N.succ_double (N.div2 (N.pos p)) = N.pos p discriminate H.p:positive
Nodd (N.pos p) ->
N.succ_double (N.div2 (N.pos p)) = N.pos p
  destruct p.p:positive
Nodd (N.pos p~1) ->
N.succ_double (N.div2 (N.pos p~1)) = N.pos p~1
p:positive
Nodd (N.pos p~0) ->
N.succ_double (N.div2 (N.pos p~0)) = N.pos p~0
Nodd 1 -> N.succ_double (N.div2 1) = 1%N intros.p:positive
H:Nodd (N.pos p~1)
N.succ_double (N.div2 (N.pos p~1)) = N.pos p~1
p:positive
Nodd (N.pos p~0) ->
N.succ_double (N.div2 (N.pos p~0)) = N.pos p~0
Nodd 1 -> N.succ_double (N.div2 1) = 1%N reflexivity.p:positive
Nodd (N.pos p~0) ->
N.succ_double (N.div2 (N.pos p~0)) = N.pos p~0
Nodd 1 -> N.succ_double (N.div2 1) = 1%N
  intro H.p:positive
H:Nodd (N.pos p~0)
N.succ_double (N.div2 (N.pos p~0)) = N.pos p~0
Nodd 1 -> N.succ_double (N.div2 1) = 1%N discriminate H.Nodd 1 -> N.succ_double (N.div2 1) = 1%N
  intro.H:Nodd 1
N.succ_double (N.div2 1) = 1%N reflexivity.
Qed.

Lemma Ndiv2_correct :
 forall (a:N) (n:nat), N.testbit_nat (N.div2 a) n = N.testbit_nat a (S n).forall (a : N) (n : nat),
N.testbit_nat (N.div2 a) n = N.testbit_nat a (S n)
Proof.forall (a : N) (n : nat),
N.testbit_nat (N.div2 a) n = N.testbit_nat a (S n)
  destruct a; trivial.p:positive
forall n : nat,
N.testbit_nat (N.div2 (N.pos p)) n =
N.testbit_nat (N.pos p) (S n)
  destruct p; trivial.
Qed.

Lemma Nxor_bit0 :
 forall a a':N, N.odd (N.lxor a a') = xorb (N.odd a) (N.odd a').forall a a' : N,
N.odd (N.lxor a a') = xorb (N.odd a) (N.odd a')
Proof.forall a a' : N,
N.odd (N.lxor a a') = xorb (N.odd a) (N.odd a')
  intros.a, a':N
N.odd (N.lxor a a') = xorb (N.odd a) (N.odd a') rewrite <- Nbit0_correct, (Nxor_semantics a a' O).a, a':N
xorb (N.testbit_nat a 0) (N.testbit_nat a' 0) =
xorb (N.odd a) (N.odd a')
  rewrite Nbit0_correct, Nbit0_correct.a, a':N
xorb (N.odd a) (N.odd a') = xorb (N.odd a) (N.odd a') reflexivity.
Qed.

Lemma Nxor_div2 :
 forall a a':N, N.div2 (N.lxor a a') = N.lxor (N.div2 a) (N.div2 a').forall a a' : N,
N.div2 (N.lxor a a') = N.lxor (N.div2 a) (N.div2 a')
Proof.forall a a' : N,
N.div2 (N.lxor a a') = N.lxor (N.div2 a) (N.div2 a')
  intros.a, a':N
N.div2 (N.lxor a a') = N.lxor (N.div2 a) (N.div2 a') apply Nbit_faithful.a, a':N
N.testbit_nat (N.div2 (N.lxor a a')) ==
N.testbit_nat (N.lxor (N.div2 a) (N.div2 a')) unfold eqf.a, a':N
forall n : nat,
N.testbit_nat (N.div2 (N.lxor a a')) n =
N.testbit_nat (N.lxor (N.div2 a) (N.div2 a')) n intro.a, a':N
n:nat
N.testbit_nat (N.div2 (N.lxor a a')) n =
N.testbit_nat (N.lxor (N.div2 a) (N.div2 a')) n
  rewrite (Nxor_semantics (N.div2 a) (N.div2 a') n), Ndiv2_correct, (Nxor_semantics a a' (S n)).a, a':N
n:nat
xorb (N.testbit_nat a (S n)) (N.testbit_nat a' (S n)) =
xorb (N.testbit_nat (N.div2 a) n)
  (N.testbit_nat (N.div2 a') n)
  rewrite 2! Ndiv2_correct.a, a':N
n:nat
xorb (N.testbit_nat a (S n)) (N.testbit_nat a' (S n)) =
xorb (N.testbit_nat a (S n)) (N.testbit_nat a' (S n))
  reflexivity.
Qed.

Lemma Nneg_bit0 :
 forall a a':N,
   N.odd (N.lxor a a') = true -> N.odd a = negb (N.odd a').forall a a' : N,
N.odd (N.lxor a a') = true ->
N.odd a = negb (N.odd a')
Proof.forall a a' : N,
N.odd (N.lxor a a') = true ->
N.odd a = negb (N.odd a')
  intros.a, a':N
H:N.odd (N.lxor a a') = true
N.odd a = negb (N.odd a')
  rewrite <- true_xorb, <- H, Nxor_bit0, xorb_assoc, 
    xorb_nilpotent, xorb_false.a, a':N
H:N.odd (N.lxor a a') = true
N.odd a = N.odd a
  reflexivity.
Qed.

Lemma Nneg_bit0_1 :
 forall a a':N, N.lxor a a' = Npos 1 -> N.odd a = negb (N.odd a').forall a a' : N,
N.lxor a a' = 1%N -> N.odd a = negb (N.odd a')
Proof.forall a a' : N,
N.lxor a a' = 1%N -> N.odd a = negb (N.odd a')
  intros.a, a':N
H:N.lxor a a' = 1%N
N.odd a = negb (N.odd a') apply Nneg_bit0.a, a':N
H:N.lxor a a' = 1%N
N.odd (N.lxor a a') = true rewrite H.a, a':N
H:N.lxor a a' = 1%N
N.odd 1 = true reflexivity.
Qed.

Lemma Nneg_bit0_2 :
 forall (a a':N) (p:positive),
   N.lxor a a' = Npos (xI p) -> N.odd a = negb (N.odd a').forall (a a' : N) (p : positive),
N.lxor a a' = N.pos p~1 -> N.odd a = negb (N.odd a')
Proof.forall (a a' : N) (p : positive),
N.lxor a a' = N.pos p~1 -> N.odd a = negb (N.odd a')
  intros.a, a':N
p:positive
H:N.lxor a a' = N.pos p~1
N.odd a = negb (N.odd a') apply Nneg_bit0.a, a':N
p:positive
H:N.lxor a a' = N.pos p~1
N.odd (N.lxor a a') = true rewrite H.a, a':N
p:positive
H:N.lxor a a' = N.pos p~1
N.odd (N.pos p~1) = true reflexivity.
Qed.

Lemma Nsame_bit0 :
 forall (a a':N) (p:positive),
   N.lxor a a' = Npos (xO p) -> N.odd a = N.odd a'.forall (a a' : N) (p : positive),
N.lxor a a' = N.pos p~0 -> N.odd a = N.odd a'
Proof.forall (a a' : N) (p : positive),
N.lxor a a' = N.pos p~0 -> N.odd a = N.odd a'
  intros.a, a':N
p:positive
H:N.lxor a a' = N.pos p~0
N.odd a = N.odd a' rewrite <- (xorb_false (N.odd a)).a, a':N
p:positive
H:N.lxor a a' = N.pos p~0
xorb (N.odd a) false = N.odd a'
  assert (H0: N.odd (Npos (xO p)) = false) by reflexivity.a, a':N
p:positive
H:N.lxor a a' = N.pos p~0
H0:N.odd (N.pos p~0) = false
xorb (N.odd a) false = N.odd a'
  rewrite <- H0, <- H, Nxor_bit0, <- xorb_assoc, xorb_nilpotent, false_xorb.a, a':N
p:positive
H:N.lxor a a' = N.pos p~0
H0:N.odd (N.pos p~0) = false
N.odd a' = N.odd a'
    reflexivity.
Qed.

a lexicographic order on bits, starting from the lowest bit

Fixpoint Nless_aux (a a':N) (p:positive) : bool :=
  match p with
  | xO p' => Nless_aux (N.div2 a) (N.div2 a') p'
  | _ => andb (negb (N.odd a)) (N.odd a')
  end.

Definition Nless (a a':N) :=
  match N.lxor a a' with
  | N0 => false
  | Npos p => Nless_aux a a' p
  end.

Lemma Nbit0_less :
 forall a a',
   N.odd a = false -> N.odd a' = true -> Nless a a' = true.forall a a' : N,
N.odd a = false ->
N.odd a' = true -> Nless a a' = true
Proof.forall a a' : N,
N.odd a = false ->
N.odd a' = true -> Nless a a' = true
  intros.a, a':N
H:N.odd a = false
H0:N.odd a' = true
Nless a a' = true destruct (N.discr (N.lxor a a')) as [(p,H2)|H1].a, a':N
H:N.odd a = false
H0:N.odd a' = true
p:positive
H2:N.lxor a a' = N.pos p
Nless a a' = true
a, a':N
H:N.odd a = false
H0:N.odd a' = true
H1:N.lxor a a' = 0%N
Nless a a' = true unfold Nless.a, a':N
H:N.odd a = false
H0:N.odd a' = true
p:positive
H2:N.lxor a a' = N.pos p
match N.lxor a a' with
| 0%N => false
| N.pos p0 => Nless_aux a a' p0
end = true
a, a':N
H:N.odd a = false
H0:N.odd a' = true
H1:N.lxor a a' = 0%N
Nless a a' = true
  rewrite H2.a, a':N
H:N.odd a = false
H0:N.odd a' = true
p:positive
H2:N.lxor a a' = N.pos p
Nless_aux a a' p = true
a, a':N
H:N.odd a = false
H0:N.odd a' = true
H1:N.lxor a a' = 0%N
Nless a a' = true destruct p.a, a':N
H:N.odd a = false
H0:N.odd a' = true
p:positive
H2:N.lxor a a' = N.pos p~1
Nless_aux a a' p~1 = true
a, a':N
H:N.odd a = false
H0:N.odd a' = true
p:positive
H2:N.lxor a a' = N.pos p~0
Nless_aux a a' p~0 = true
a, a':N
H:N.odd a = false
H0:N.odd a' = true
H2:N.lxor a a' = 1%N
Nless_aux a a' 1 = true
a, a':N
H:N.odd a = false
H0:N.odd a' = true
H1:N.lxor a a' = 0%N
Nless a a' = true simpl.a, a':N
H:N.odd a = false
H0:N.odd a' = true
p:positive
H2:N.lxor a a' = N.pos p~1
negb (N.odd a) && N.odd a' = true
a, a':N
H:N.odd a = false
H0:N.odd a' = true
p:positive
H2:N.lxor a a' = N.pos p~0
Nless_aux a a' p~0 = true
a, a':N
H:N.odd a = false
H0:N.odd a' = true
H2:N.lxor a a' = 1%N
Nless_aux a a' 1 = true
a, a':N
H:N.odd a = false
H0:N.odd a' = true
H1:N.lxor a a' = 0%N
Nless a a' = true rewrite H, H0.a, a':N
H:N.odd a = false
H0:N.odd a' = true
p:positive
H2:N.lxor a a' = N.pos p~1
negb false && true = true
a, a':N
H:N.odd a = false
H0:N.odd a' = true
p:positive
H2:N.lxor a a' = N.pos p~0
Nless_aux a a' p~0 = true
a, a':N
H:N.odd a = false
H0:N.odd a' = true
H2:N.lxor a a' = 1%N
Nless_aux a a' 1 = true
a, a':N
H:N.odd a = false
H0:N.odd a' = true
H1:N.lxor a a' = 0%N
Nless a a' = true reflexivity.a, a':N
H:N.odd a = false
H0:N.odd a' = true
p:positive
H2:N.lxor a a' = N.pos p~0
Nless_aux a a' p~0 = true
a, a':N
H:N.odd a = false
H0:N.odd a' = true
H2:N.lxor a a' = 1%N
Nless_aux a a' 1 = true
a, a':N
H:N.odd a = false
H0:N.odd a' = true
H1:N.lxor a a' = 0%N
Nless a a' = true
  assert (H1: N.odd (N.lxor a a') = false) by (rewrite H2; reflexivity).a, a':N
H:N.odd a = false
H0:N.odd a' = true
p:positive
H2:N.lxor a a' = N.pos p~0
H1:N.odd (N.lxor a a') = false
Nless_aux a a' p~0 = true
a, a':N
H:N.odd a = false
H0:N.odd a' = true
H2:N.lxor a a' = 1%N
Nless_aux a a' 1 = true
a, a':N
H:N.odd a = false
H0:N.odd a' = true
H1:N.lxor a a' = 0%N
Nless a a' = true
  rewrite (Nxor_bit0 a a'), H, H0 in H1.a, a':N
H:N.odd a = false
H0:N.odd a' = true
p:positive
H2:N.lxor a a' = N.pos p~0
H1:xorb false true = false
Nless_aux a a' p~0 = true
a, a':N
H:N.odd a = false
H0:N.odd a' = true
H2:N.lxor a a' = 1%N
Nless_aux a a' 1 = true
a, a':N
H:N.odd a = false
H0:N.odd a' = true
H1:N.lxor a a' = 0%N
Nless a a' = true discriminate H1.a, a':N
H:N.odd a = false
H0:N.odd a' = true
H2:N.lxor a a' = 1%N
Nless_aux a a' 1 = true
a, a':N
H:N.odd a = false
H0:N.odd a' = true
H1:N.lxor a a' = 0%N
Nless a a' = true
  simpl.a, a':N
H:N.odd a = false
H0:N.odd a' = true
H2:N.lxor a a' = 1%N
negb (N.odd a) && N.odd a' = true
a, a':N
H:N.odd a = false
H0:N.odd a' = true
H1:N.lxor a a' = 0%N
Nless a a' = true rewrite H, H0.a, a':N
H:N.odd a = false
H0:N.odd a' = true
H2:N.lxor a a' = 1%N
negb false && true = true
a, a':N
H:N.odd a = false
H0:N.odd a' = true
H1:N.lxor a a' = 0%N
Nless a a' = true reflexivity.a, a':N
H:N.odd a = false
H0:N.odd a' = true
H1:N.lxor a a' = 0%N
Nless a a' = true
  assert (H2: N.odd (N.lxor a a') = false) by (rewrite H1; reflexivity).a, a':N
H:N.odd a = false
H0:N.odd a' = true
H1:N.lxor a a' = 0%N
H2:N.odd (N.lxor a a') = false
Nless a a' = true
  rewrite (Nxor_bit0 a a'), H, H0 in H2.a, a':N
H:N.odd a = false
H0:N.odd a' = true
H1:N.lxor a a' = 0%N
H2:xorb false true = false
Nless a a' = true discriminate H2.
Qed.

Lemma Nbit0_gt :
 forall a a',
   N.odd a = true -> N.odd a' = false -> Nless a a' = false.forall a a' : N,
N.odd a = true ->
N.odd a' = false -> Nless a a' = false
Proof.forall a a' : N,
N.odd a = true ->
N.odd a' = false -> Nless a a' = false
  intros.a, a':N
H:N.odd a = true
H0:N.odd a' = false
Nless a a' = false destruct (N.discr (N.lxor a a')) as [(p,H2)|H1].a, a':N
H:N.odd a = true
H0:N.odd a' = false
p:positive
H2:N.lxor a a' = N.pos p
Nless a a' = false
a, a':N
H:N.odd a = true
H0:N.odd a' = false
H1:N.lxor a a' = 0%N
Nless a a' = false unfold Nless.a, a':N
H:N.odd a = true
H0:N.odd a' = false
p:positive
H2:N.lxor a a' = N.pos p
match N.lxor a a' with
| 0%N => false
| N.pos p0 => Nless_aux a a' p0
end = false
a, a':N
H:N.odd a = true
H0:N.odd a' = false
H1:N.lxor a a' = 0%N
Nless a a' = false
  rewrite H2.a, a':N
H:N.odd a = true
H0:N.odd a' = false
p:positive
H2:N.lxor a a' = N.pos p
Nless_aux a a' p = false
a, a':N
H:N.odd a = true
H0:N.odd a' = false
H1:N.lxor a a' = 0%N
Nless a a' = false destruct p.a, a':N
H:N.odd a = true
H0:N.odd a' = false
p:positive
H2:N.lxor a a' = N.pos p~1
Nless_aux a a' p~1 = false
a, a':N
H:N.odd a = true
H0:N.odd a' = false
p:positive
H2:N.lxor a a' = N.pos p~0
Nless_aux a a' p~0 = false
a, a':N
H:N.odd a = true
H0:N.odd a' = false
H2:N.lxor a a' = 1%N
Nless_aux a a' 1 = false
a, a':N
H:N.odd a = true
H0:N.odd a' = false
H1:N.lxor a a' = 0%N
Nless a a' = false simpl.a, a':N
H:N.odd a = true
H0:N.odd a' = false
p:positive
H2:N.lxor a a' = N.pos p~1
negb (N.odd a) && N.odd a' = false
a, a':N
H:N.odd a = true
H0:N.odd a' = false
p:positive
H2:N.lxor a a' = N.pos p~0
Nless_aux a a' p~0 = false
a, a':N
H:N.odd a = true
H0:N.odd a' = false
H2:N.lxor a a' = 1%N
Nless_aux a a' 1 = false
a, a':N
H:N.odd a = true
H0:N.odd a' = false
H1:N.lxor a a' = 0%N
Nless a a' = false rewrite H, H0.a, a':N
H:N.odd a = true
H0:N.odd a' = false
p:positive
H2:N.lxor a a' = N.pos p~1
negb true && false = false
a, a':N
H:N.odd a = true
H0:N.odd a' = false
p:positive
H2:N.lxor a a' = N.pos p~0
Nless_aux a a' p~0 = false
a, a':N
H:N.odd a = true
H0:N.odd a' = false
H2:N.lxor a a' = 1%N
Nless_aux a a' 1 = false
a, a':N
H:N.odd a = true
H0:N.odd a' = false
H1:N.lxor a a' = 0%N
Nless a a' = false reflexivity.a, a':N
H:N.odd a = true
H0:N.odd a' = false
p:positive
H2:N.lxor a a' = N.pos p~0
Nless_aux a a' p~0 = false
a, a':N
H:N.odd a = true
H0:N.odd a' = false
H2:N.lxor a a' = 1%N
Nless_aux a a' 1 = false
a, a':N
H:N.odd a = true
H0:N.odd a' = false
H1:N.lxor a a' = 0%N
Nless a a' = false
  assert (H1: N.odd (N.lxor a a') = false) by (rewrite H2; reflexivity).a, a':N
H:N.odd a = true
H0:N.odd a' = false
p:positive
H2:N.lxor a a' = N.pos p~0
H1:N.odd (N.lxor a a') = false
Nless_aux a a' p~0 = false
a, a':N
H:N.odd a = true
H0:N.odd a' = false
H2:N.lxor a a' = 1%N
Nless_aux a a' 1 = false
a, a':N
H:N.odd a = true
H0:N.odd a' = false
H1:N.lxor a a' = 0%N
Nless a a' = false
  rewrite (Nxor_bit0 a a'), H, H0 in H1.a, a':N
H:N.odd a = true
H0:N.odd a' = false
p:positive
H2:N.lxor a a' = N.pos p~0
H1:xorb true false = false
Nless_aux a a' p~0 = false
a, a':N
H:N.odd a = true
H0:N.odd a' = false
H2:N.lxor a a' = 1%N
Nless_aux a a' 1 = false
a, a':N
H:N.odd a = true
H0:N.odd a' = false
H1:N.lxor a a' = 0%N
Nless a a' = false discriminate H1.a, a':N
H:N.odd a = true
H0:N.odd a' = false
H2:N.lxor a a' = 1%N
Nless_aux a a' 1 = false
a, a':N
H:N.odd a = true
H0:N.odd a' = false
H1:N.lxor a a' = 0%N
Nless a a' = false
  simpl.a, a':N
H:N.odd a = true
H0:N.odd a' = false
H2:N.lxor a a' = 1%N
negb (N.odd a) && N.odd a' = false
a, a':N
H:N.odd a = true
H0:N.odd a' = false
H1:N.lxor a a' = 0%N
Nless a a' = false rewrite H, H0.a, a':N
H:N.odd a = true
H0:N.odd a' = false
H2:N.lxor a a' = 1%N
negb true && false = false
a, a':N
H:N.odd a = true
H0:N.odd a' = false
H1:N.lxor a a' = 0%N
Nless a a' = false reflexivity.a, a':N
H:N.odd a = true
H0:N.odd a' = false
H1:N.lxor a a' = 0%N
Nless a a' = false
  assert (H2: N.odd (N.lxor a a') = false) by (rewrite H1; reflexivity).a, a':N
H:N.odd a = true
H0:N.odd a' = false
H1:N.lxor a a' = 0%N
H2:N.odd (N.lxor a a') = false
Nless a a' = false
  rewrite (Nxor_bit0 a a'), H, H0 in H2.a, a':N
H:N.odd a = true
H0:N.odd a' = false
H1:N.lxor a a' = 0%N
H2:xorb true false = false
Nless a a' = false discriminate H2.
Qed.

Lemma Nless_not_refl : forall a, Nless a a = false.forall a : N, Nless a a = false
Proof.forall a : N, Nless a a = false
  intro.a:N
Nless a a = false unfold Nless.a:N
match N.lxor a a with
| 0%N => false
| N.pos p => Nless_aux a a p
end = false rewrite (N.lxor_nilpotent a).a:N
false = false reflexivity.
Qed.

Lemma Nless_def_1 :
 forall a a', Nless (N.double a) (N.double a') = Nless a a'.forall a a' : N,
Nless (N.double a) (N.double a') = Nless a a'
Proof.forall a a' : N,
Nless (N.double a) (N.double a') = Nless a a'
  destruct a; destruct a'.Nless (N.double 0) (N.double 0) = Nless 0 0
p:positive
Nless (N.double 0) (N.double (N.pos p)) =
Nless 0 (N.pos p)
p:positive
Nless (N.double (N.pos p)) (N.double 0) =
Nless (N.pos p) 0
p, p0:positive
Nless (N.double (N.pos p)) (N.double (N.pos p0)) =
Nless (N.pos p) (N.pos p0) reflexivity.p:positive
Nless (N.double 0) (N.double (N.pos p)) =
Nless 0 (N.pos p)
p:positive
Nless (N.double (N.pos p)) (N.double 0) =
Nless (N.pos p) 0
p, p0:positive
Nless (N.double (N.pos p)) (N.double (N.pos p0)) =
Nless (N.pos p) (N.pos p0)
  trivial.p:positive
Nless (N.double (N.pos p)) (N.double 0) =
Nless (N.pos p) 0
p, p0:positive
Nless (N.double (N.pos p)) (N.double (N.pos p0)) =
Nless (N.pos p) (N.pos p0)
  unfold Nless.p:positive
match N.lxor (N.double (N.pos p)) (N.double 0) with
| 0%N => false
| N.pos p0 =>
    Nless_aux (N.double (N.pos p)) (N.double 0) p0
end =
match N.lxor (N.pos p) 0 with
| 0%N => false
| N.pos p0 => Nless_aux (N.pos p) 0 p0
end
p, p0:positive
Nless (N.double (N.pos p)) (N.double (N.pos p0)) =
Nless (N.pos p) (N.pos p0) simpl.p:positive
Nless_aux (N.pos p) 0 p = Nless_aux (N.pos p) 0 p
p, p0:positive
Nless (N.double (N.pos p)) (N.double (N.pos p0)) =
Nless (N.pos p) (N.pos p0) destruct p; trivial.p, p0:positive
Nless (N.double (N.pos p)) (N.double (N.pos p0)) =
Nless (N.pos p) (N.pos p0)
  unfold Nless.p, p0:positive
match
  N.lxor (N.double (N.pos p)) (N.double (N.pos p0))
with
| 0%N => false
| N.pos p1 =>
    Nless_aux (N.double (N.pos p))
      (N.double (N.pos p0)) p1
end =
match N.lxor (N.pos p) (N.pos p0) with
| 0%N => false
| N.pos p1 => Nless_aux (N.pos p) (N.pos p0) p1
end simpl.p, p0:positive
match Pos.Ndouble (Pos.lxor p p0) with
| 0%N => false
| N.pos p1 => Nless_aux (N.pos p~0) (N.pos p0~0) p1
end =
match Pos.lxor p p0 with
| 0%N => false
| N.pos p1 => Nless_aux (N.pos p) (N.pos p0) p1
end destruct (Pos.lxor p p0).p, p0:positive
match Pos.Ndouble 0 with
| 0%N => false
| N.pos p1 => Nless_aux (N.pos p~0) (N.pos p0~0) p1
end = false
p, p0, p1:positive
match Pos.Ndouble (N.pos p1) with
| 0%N => false
| N.pos p2 => Nless_aux (N.pos p~0) (N.pos p0~0) p2
end = Nless_aux (N.pos p) (N.pos p0) p1 reflexivity.p, p0, p1:positive
match Pos.Ndouble (N.pos p1) with
| 0%N => false
| N.pos p2 => Nless_aux (N.pos p~0) (N.pos p0~0) p2
end = Nless_aux (N.pos p) (N.pos p0) p1
  trivial.
Qed.

Lemma Nless_def_2 :
 forall a a',
   Nless (N.succ_double a) (N.succ_double a') = Nless a a'.forall a a' : N,
Nless (N.succ_double a) (N.succ_double a') =
Nless a a'
Proof.forall a a' : N,
Nless (N.succ_double a) (N.succ_double a') =
Nless a a'
  destruct a; destruct a'.Nless (N.succ_double 0) (N.succ_double 0) = Nless 0 0
p:positive
Nless (N.succ_double 0) (N.succ_double (N.pos p)) =
Nless 0 (N.pos p)
p:positive
Nless (N.succ_double (N.pos p)) (N.succ_double 0) =
Nless (N.pos p) 0
p, p0:positive
Nless (N.succ_double (N.pos p))
  (N.succ_double (N.pos p0)) =
Nless (N.pos p) (N.pos p0) reflexivity.p:positive
Nless (N.succ_double 0) (N.succ_double (N.pos p)) =
Nless 0 (N.pos p)
p:positive
Nless (N.succ_double (N.pos p)) (N.succ_double 0) =
Nless (N.pos p) 0
p, p0:positive
Nless (N.succ_double (N.pos p))
  (N.succ_double (N.pos p0)) =
Nless (N.pos p) (N.pos p0)
  trivial.p:positive
Nless (N.succ_double (N.pos p)) (N.succ_double 0) =
Nless (N.pos p) 0
p, p0:positive
Nless (N.succ_double (N.pos p))
  (N.succ_double (N.pos p0)) =
Nless (N.pos p) (N.pos p0)
  unfold Nless.p:positive
match
  N.lxor (N.succ_double (N.pos p)) (N.succ_double 0)
with
| 0%N => false
| N.pos p0 =>
    Nless_aux (N.succ_double (N.pos p))
      (N.succ_double 0) p0
end =
match N.lxor (N.pos p) 0 with
| 0%N => false
| N.pos p0 => Nless_aux (N.pos p) 0 p0
end
p, p0:positive
Nless (N.succ_double (N.pos p))
  (N.succ_double (N.pos p0)) =
Nless (N.pos p) (N.pos p0) simpl.p:positive
Nless_aux (N.pos p) 0 p = Nless_aux (N.pos p) 0 p
p, p0:positive
Nless (N.succ_double (N.pos p))
  (N.succ_double (N.pos p0)) =
Nless (N.pos p) (N.pos p0) destruct p; trivial.p, p0:positive
Nless (N.succ_double (N.pos p))
  (N.succ_double (N.pos p0)) =
Nless (N.pos p) (N.pos p0)
  unfold Nless.p, p0:positive
match
  N.lxor (N.succ_double (N.pos p))
    (N.succ_double (N.pos p0))
with
| 0%N => false
| N.pos p1 =>
    Nless_aux (N.succ_double (N.pos p))
      (N.succ_double (N.pos p0)) p1
end =
match N.lxor (N.pos p) (N.pos p0) with
| 0%N => false
| N.pos p1 => Nless_aux (N.pos p) (N.pos p0) p1
end simpl.p, p0:positive
match Pos.Ndouble (Pos.lxor p p0) with
| 0%N => false
| N.pos p1 => Nless_aux (N.pos p~1) (N.pos p0~1) p1
end =
match Pos.lxor p p0 with
| 0%N => false
| N.pos p1 => Nless_aux (N.pos p) (N.pos p0) p1
end destruct (Pos.lxor p p0).p, p0:positive
match Pos.Ndouble 0 with
| 0%N => false
| N.pos p1 => Nless_aux (N.pos p~1) (N.pos p0~1) p1
end = false
p, p0, p1:positive
match Pos.Ndouble (N.pos p1) with
| 0%N => false
| N.pos p2 => Nless_aux (N.pos p~1) (N.pos p0~1) p2
end = Nless_aux (N.pos p) (N.pos p0) p1 reflexivity.p, p0, p1:positive
match Pos.Ndouble (N.pos p1) with
| 0%N => false
| N.pos p2 => Nless_aux (N.pos p~1) (N.pos p0~1) p2
end = Nless_aux (N.pos p) (N.pos p0) p1
  trivial.
Qed.

Lemma Nless_def_3 :
 forall a a', Nless (N.double a) (N.succ_double a') = true.forall a a' : N,
Nless (N.double a) (N.succ_double a') = true
Proof.forall a a' : N,
Nless (N.double a) (N.succ_double a') = true
  intros.a, a':N
Nless (N.double a) (N.succ_double a') = true apply Nbit0_less.a, a':N
N.odd (N.double a) = false
a, a':N
N.odd (N.succ_double a') = true apply Ndouble_bit0.a, a':N
N.odd (N.succ_double a') = true
  apply Ndouble_plus_one_bit0.
Qed.

Lemma Nless_def_4 :
 forall a a', Nless (N.succ_double a) (N.double a') = false.forall a a' : N,
Nless (N.succ_double a) (N.double a') = false
Proof.forall a a' : N,
Nless (N.succ_double a) (N.double a') = false
  intros.a, a':N
Nless (N.succ_double a) (N.double a') = false apply Nbit0_gt.a, a':N
N.odd (N.succ_double a) = true
a, a':N
N.odd (N.double a') = false apply Ndouble_plus_one_bit0.a, a':N
N.odd (N.double a') = false
  apply Ndouble_bit0.
Qed.

Lemma Nless_z : forall a, Nless a N0 = false.forall a : N, Nless a 0 = false
Proof.forall a : N, Nless a 0 = false
  induction a.Nless 0 0 = false
p:positive
Nless (N.pos p) 0 = false reflexivity.p:positive
Nless (N.pos p) 0 = false
  unfold Nless.p:positive
match N.lxor (N.pos p) 0 with
| 0%N => false
| N.pos p0 => Nless_aux (N.pos p) 0 p0
end = false rewrite (N.lxor_0_r (Npos p)).p:positive
Nless_aux (N.pos p) 0 p = false induction p; trivial.
Qed.

Lemma N0_less_1 :
 forall a, Nless N0 a = true -> {p : positive | a = Npos p}.forall a : N,
Nless 0 a = true -> {p : positive | a = N.pos p}
Proof.forall a : N,
Nless 0 a = true -> {p : positive | a = N.pos p}
  destruct a.Nless 0 0 = true -> {p : positive | 0%N = N.pos p}
p:positive
Nless 0 (N.pos p) = true ->
{p0 : positive | N.pos p = N.pos p0} discriminate.p:positive
Nless 0 (N.pos p) = true ->
{p0 : positive | N.pos p = N.pos p0}
  intros.p:positive
H:Nless 0 (N.pos p) = true
{p0 : positive | N.pos p = N.pos p0} exists p.p:positive
H:Nless 0 (N.pos p) = true
N.pos p = N.pos p reflexivity.
Qed.

Lemma N0_less_2 : forall a, Nless N0 a = false -> a = N0.forall a : N, Nless 0 a = false -> a = 0%N
Proof.forall a : N, Nless 0 a = false -> a = 0%N
  induction a as [|p]; intro H.H:Nless 0 0 = false
0%N = 0%N
p:positive
H:Nless 0 (N.pos p) = false
N.pos p = 0%N trivial.p:positive
H:Nless 0 (N.pos p) = false
N.pos p = 0%N
  exfalso.p:positive
H:Nless 0 (N.pos p) = false
False induction p as [|p IHp|]; discriminate || simpl; auto using IHp.
Qed.

Lemma Nless_trans :
 forall a a' a'',
   Nless a a' = true -> Nless a' a'' = true -> Nless a a'' = true.forall a a' a'' : N,
Nless a a' = true ->
Nless a' a'' = true -> Nless a a'' = true
Proof.forall a a' a'' : N,
Nless a a' = true ->
Nless a' a'' = true -> Nless a a'' = true
  induction a as [|a IHa|a IHa] using N.binary_ind; intros a' a'' H H0.a', a'':N
H:Nless 0 a' = true
H0:Nless a' a'' = true
Nless 0 a'' = true
a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless (N.double a) a' = true
H0:Nless a' a'' = true
Nless (N.double a) a'' = true
a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless (N.succ_double a) a' = true
H0:Nless a' a'' = true
Nless (N.succ_double a) a'' = true
  -a', a'':N
H:Nless 0 a' = true
H0:Nless a' a'' = true
Nless 0 a'' = true case_eq (Nless N0 a'') ; intros Heqn.a', a'':N
H:Nless 0 a' = true
H0:Nless a' a'' = true
Heqn:Nless 0 a'' = true
true = true
a', a'':N
H:Nless 0 a' = true
H0:Nless a' a'' = true
Heqn:Nless 0 a'' = false
false = true
    +a', a'':N
H:Nless 0 a' = true
H0:Nless a' a'' = true
Heqn:Nless 0 a'' = true
true = true trivial.
    +a', a'':N
H:Nless 0 a' = true
H0:Nless a' a'' = true
Heqn:Nless 0 a'' = false
false = true rewrite (N0_less_2 a'' Heqn), (Nless_z a') in H0.a', a'':N
H:Nless 0 a' = true
H0:false = true
Heqn:Nless 0 a'' = false
false = true discriminate H0.
  -a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless (N.double a) a' = true
H0:Nless a' a'' = true
Nless (N.double a) a'' = true induction a' as [|a' _|a' _] using N.binary_ind.a:N
IHa:forall a' a''0 : N,
Nless a a' = true -> Nless a' a''0 = true -> Nless a a''0 = true
a'':N
H:Nless (N.double a) 0 = true
H0:Nless 0 a'' = true
Nless (N.double a) a'' = true
a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless (N.double a) (N.double a') = true
H0:Nless (N.double a') a'' = true
Nless (N.double a) a'' = true
a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless (N.double a) (N.succ_double a') = true
H0:Nless (N.succ_double a') a'' = true
Nless (N.double a) a'' = true
    +a:N
IHa:forall a' a''0 : N,
Nless a a' = true -> Nless a' a''0 = true -> Nless a a''0 = true
a'':N
H:Nless (N.double a) 0 = true
H0:Nless 0 a'' = true
Nless (N.double a) a'' = true rewrite (Nless_z (N.double a)) in H.a:N
IHa:forall a' a''0 : N,
Nless a a' = true -> Nless a' a''0 = true -> Nless a a''0 = true
a'':N
H:false = true
H0:Nless 0 a'' = true
Nless (N.double a) a'' = true discriminate H.
    +a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless (N.double a) (N.double a') = true
H0:Nless (N.double a') a'' = true
Nless (N.double a) a'' = true rewrite (Nless_def_1 a a') in H.a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless a a' = true
H0:Nless (N.double a') a'' = true
Nless (N.double a) a'' = true
      induction a'' using N.binary_ind.a:N
IHa:forall a'0 a'' : N,
Nless a a'0 = true -> Nless a'0 a'' = true -> Nless a a'' = true
a':N
H:Nless a a' = true
H0:Nless (N.double a') 0 = true
Nless (N.double a) 0 = true
a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless a a' = true
H0:Nless (N.double a') (N.double a'') = true
IHa'':Nless (N.double a') a'' = true ->
Nless (N.double a) a'' = true
Nless (N.double a) (N.double a'') = true
a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true ->
Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless a a' = true
H0:Nless (N.double a') (N.succ_double a'') = true
IHa'':Nless (N.double a') a'' = true ->
Nless (N.double a) a'' = true
Nless (N.double a) (N.succ_double a'') = true
      *a:N
IHa:forall a'0 a'' : N,
Nless a a'0 = true -> Nless a'0 a'' = true -> Nless a a'' = true
a':N
H:Nless a a' = true
H0:Nless (N.double a') 0 = true
Nless (N.double a) 0 = true rewrite (Nless_z (N.double a')) in H0.a:N
IHa:forall a'0 a'' : N,
Nless a a'0 = true -> Nless a'0 a'' = true -> Nless a a'' = true
a':N
H:Nless a a' = true
H0:false = true
Nless (N.double a) 0 = true discriminate H0.
      *a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless a a' = true
H0:Nless (N.double a') (N.double a'') = true
IHa'':Nless (N.double a') a'' = true ->
Nless (N.double a) a'' = true
Nless (N.double a) (N.double a'') = true rewrite (Nless_def_1 a' a'') in H0.a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless a a' = true
H0:Nless a' a'' = true
IHa'':Nless (N.double a') a'' = true ->
Nless (N.double a) a'' = true
Nless (N.double a) (N.double a'') = true rewrite (Nless_def_1 a a'').a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless a a' = true
H0:Nless a' a'' = true
IHa'':Nless (N.double a') a'' = true ->
Nless (N.double a) a'' = true
Nless a a'' = true
        exact (IHa _ _ H H0).
      *a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless a a' = true
H0:Nless (N.double a') (N.succ_double a'') = true
IHa'':Nless (N.double a') a'' = true ->
Nless (N.double a) a'' = true
Nless (N.double a) (N.succ_double a'') = true apply Nless_def_3.
    +a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless (N.double a) (N.succ_double a') = true
H0:Nless (N.succ_double a') a'' = true
Nless (N.double a) a'' = true induction a'' as [|a'' _|a'' _] using N.binary_ind.a:N
IHa:forall a'0 a'' : N,
Nless a a'0 = true -> Nless a'0 a'' = true -> Nless a a'' = true
a':N
H:Nless (N.double a) (N.succ_double a') = true
H0:Nless (N.succ_double a') 0 = true
Nless (N.double a) 0 = true
a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless (N.double a) (N.succ_double a') = true
H0:Nless (N.succ_double a') (N.double a'') = true
Nless (N.double a) (N.double a'') = true
a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless (N.double a) (N.succ_double a') = true
H0:Nless (N.succ_double a') (N.succ_double a'') =
true
Nless (N.double a) (N.succ_double a'') = true
      *a:N
IHa:forall a'0 a'' : N,
Nless a a'0 = true -> Nless a'0 a'' = true -> Nless a a'' = true
a':N
H:Nless (N.double a) (N.succ_double a') = true
H0:Nless (N.succ_double a') 0 = true
Nless (N.double a) 0 = true rewrite (Nless_z (N.succ_double a')) in H0.a:N
IHa:forall a'0 a'' : N,
Nless a a'0 = true -> Nless a'0 a'' = true -> Nless a a'' = true
a':N
H:Nless (N.double a) (N.succ_double a') = true
H0:false = true
Nless (N.double a) 0 = true discriminate H0.
      *a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless (N.double a) (N.succ_double a') = true
H0:Nless (N.succ_double a') (N.double a'') = true
Nless (N.double a) (N.double a'') = true rewrite (Nless_def_4 a' a'') in H0.a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless (N.double a) (N.succ_double a') = true
H0:false = true
Nless (N.double a) (N.double a'') = true discriminate H0.
      *a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless (N.double a) (N.succ_double a') = true
H0:Nless (N.succ_double a') (N.succ_double a'') =
true
Nless (N.double a) (N.succ_double a'') = true apply Nless_def_3.
  -a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless (N.succ_double a) a' = true
H0:Nless a' a'' = true
Nless (N.succ_double a) a'' = true induction a' as [|a' _|a' _] using N.binary_ind.a:N
IHa:forall a' a''0 : N,
Nless a a' = true -> Nless a' a''0 = true -> Nless a a''0 = true
a'':N
H:Nless (N.succ_double a) 0 = true
H0:Nless 0 a'' = true
Nless (N.succ_double a) a'' = true
a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless (N.succ_double a) (N.double a') = true
H0:Nless (N.double a') a'' = true
Nless (N.succ_double a) a'' = true
a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless (N.succ_double a) (N.succ_double a') = true
H0:Nless (N.succ_double a') a'' = true
Nless (N.succ_double a) a'' = true
    +a:N
IHa:forall a' a''0 : N,
Nless a a' = true -> Nless a' a''0 = true -> Nless a a''0 = true
a'':N
H:Nless (N.succ_double a) 0 = true
H0:Nless 0 a'' = true
Nless (N.succ_double a) a'' = true rewrite (Nless_z (N.succ_double a)) in H.a:N
IHa:forall a' a''0 : N,
Nless a a' = true -> Nless a' a''0 = true -> Nless a a''0 = true
a'':N
H:false = true
H0:Nless 0 a'' = true
Nless (N.succ_double a) a'' = true discriminate H.
    +a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless (N.succ_double a) (N.double a') = true
H0:Nless (N.double a') a'' = true
Nless (N.succ_double a) a'' = true rewrite (Nless_def_4 a a') in H.a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:false = true
H0:Nless (N.double a') a'' = true
Nless (N.succ_double a) a'' = true discriminate H.
    +a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless (N.succ_double a) (N.succ_double a') = true
H0:Nless (N.succ_double a') a'' = true
Nless (N.succ_double a) a'' = true induction a'' using N.binary_ind.a:N
IHa:forall a'0 a'' : N,
Nless a a'0 = true -> Nless a'0 a'' = true -> Nless a a'' = true
a':N
H:Nless (N.succ_double a) (N.succ_double a') = true
H0:Nless (N.succ_double a') 0 = true
Nless (N.succ_double a) 0 = true
a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless (N.succ_double a) (N.succ_double a') = true
H0:Nless (N.succ_double a') (N.double a'') = true
IHa'':Nless (N.succ_double a') a'' = true ->
Nless (N.succ_double a) a'' = true
Nless (N.succ_double a) (N.double a'') = true
a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true ->
Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless (N.succ_double a) (N.succ_double a') = true
H0:Nless (N.succ_double a') (N.succ_double a'') =
true
IHa'':Nless (N.succ_double a') a'' = true ->
Nless (N.succ_double a) a'' = true
Nless (N.succ_double a) (N.succ_double a'') = true
      *a:N
IHa:forall a'0 a'' : N,
Nless a a'0 = true -> Nless a'0 a'' = true -> Nless a a'' = true
a':N
H:Nless (N.succ_double a) (N.succ_double a') = true
H0:Nless (N.succ_double a') 0 = true
Nless (N.succ_double a) 0 = true rewrite (Nless_z (N.succ_double a')) in H0.a:N
IHa:forall a'0 a'' : N,
Nless a a'0 = true -> Nless a'0 a'' = true -> Nless a a'' = true
a':N
H:Nless (N.succ_double a) (N.succ_double a') = true
H0:false = true
Nless (N.succ_double a) 0 = true discriminate H0.
      *a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless (N.succ_double a) (N.succ_double a') = true
H0:Nless (N.succ_double a') (N.double a'') = true
IHa'':Nless (N.succ_double a') a'' = true ->
Nless (N.succ_double a) a'' = true
Nless (N.succ_double a) (N.double a'') = true rewrite (Nless_def_4 a' a'') in H0.a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless (N.succ_double a) (N.succ_double a') = true
H0:false = true
IHa'':Nless (N.succ_double a') a'' = true ->
Nless (N.succ_double a) a'' = true
Nless (N.succ_double a) (N.double a'') = true discriminate H0.
      *a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless (N.succ_double a) (N.succ_double a') = true
H0:Nless (N.succ_double a') (N.succ_double a'') =
true
IHa'':Nless (N.succ_double a') a'' = true ->
Nless (N.succ_double a) a'' = true
Nless (N.succ_double a) (N.succ_double a'') = true rewrite (Nless_def_2 a' a'') in H0.a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless (N.succ_double a) (N.succ_double a') = true
H0:Nless a' a'' = true
IHa'':Nless (N.succ_double a') a'' = true ->
Nless (N.succ_double a) a'' = true
Nless (N.succ_double a) (N.succ_double a'') = true rewrite (Nless_def_2 a a') in H.a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless a a' = true
H0:Nless a' a'' = true
IHa'':Nless (N.succ_double a') a'' = true ->
Nless (N.succ_double a) a'' = true
Nless (N.succ_double a) (N.succ_double a'') = true
        rewrite (Nless_def_2 a a'').a:N
IHa:forall a'0 a''0 : N,
Nless a a'0 = true -> Nless a'0 a''0 = true -> Nless a a''0 = true
a', a'':N
H:Nless a a' = true
H0:Nless a' a'' = true
IHa'':Nless (N.succ_double a') a'' = true ->
Nless (N.succ_double a) a'' = true
Nless a a'' = true exact (IHa _ _ H H0).
Qed.

Lemma Nless_total :
 forall a a', {Nless a a' = true} + {Nless a' a = true} + {a = a'}.forall a a' : N,
{Nless a a' = true} + {Nless a' a = true} + {a = a'}
Proof.forall a a' : N,
{Nless a a' = true} + {Nless a' a = true} + {a = a'}
  induction a using N.binary_rec; intro a'.a':N
{Nless 0 a' = true} + {Nless a' 0 = true} + {0%N = a'}
a:N
IHa:forall a'0 : N, {Nless a a'0 = true} + {Nless a'0 a = true} + {a = a'0}
a':N
{Nless (N.double a) a' = true} +
{Nless a' (N.double a) = true} + {N.double a = a'}
a:N
IHa:forall a'0 : N, {Nless a a'0 = true} + {Nless a'0 a = true} + {a = a'0}
a':N
{Nless (N.succ_double a) a' = true} +
{Nless a' (N.succ_double a) = true} +
{N.succ_double a = a'}
  -a':N
{Nless 0 a' = true} + {Nless a' 0 = true} + {0%N = a'} case_eq (Nless N0 a') ; intros Heqb.a':N
Heqb:Nless 0 a' = true
{true = true} + {Nless a' 0 = true} + {0%N = a'}
a':N
Heqb:Nless 0 a' = false
{false = true} + {Nless a' 0 = true} + {0%N = a'}
    +a':N
Heqb:Nless 0 a' = true
{true = true} + {Nless a' 0 = true} + {0%N = a'} left.a':N
Heqb:Nless 0 a' = true
{true = true} + {Nless a' 0 = true} left.a':N
Heqb:Nless 0 a' = true
true = true auto.
    +a':N
Heqb:Nless 0 a' = false
{false = true} + {Nless a' 0 = true} + {0%N = a'} right.a':N
Heqb:Nless 0 a' = false
0%N = a' rewrite (N0_less_2 a' Heqb).a':N
Heqb:Nless 0 a' = false
0%N = 0%N reflexivity.
  -a:N
IHa:forall a'0 : N, {Nless a a'0 = true} + {Nless a'0 a = true} + {a = a'0}
a':N
{Nless (N.double a) a' = true} +
{Nless a' (N.double a) = true} + {N.double a = a'} induction a' as [|a' _|a' _] using N.binary_rec.a:N
IHa:forall a' : N, {Nless a a' = true} + {Nless a' a = true} + {a = a'}
{Nless (N.double a) 0 = true} +
{Nless 0 (N.double a) = true} + {N.double a = 0%N}
a:N
IHa:forall a'0 : N, {Nless a a'0 = true} + {Nless a'0 a = true} + {a = a'0}
a':N
{Nless (N.double a) (N.double a') = true} +
{Nless (N.double a') (N.double a) = true} +
{N.double a = N.double a'}
a:N
IHa:forall a'0 : N, {Nless a a'0 = true} + {Nless a'0 a = true} + {a = a'0}
a':N
{Nless (N.double a) (N.succ_double a') = true} +
{Nless (N.succ_double a') (N.double a) = true} +
{N.double a = N.succ_double a'}
    +a:N
IHa:forall a' : N, {Nless a a' = true} + {Nless a' a = true} + {a = a'}
{Nless (N.double a) 0 = true} +
{Nless 0 (N.double a) = true} + {N.double a = 0%N} case_eq (Nless N0 (N.double a)) ; intros Heqb.a:N
IHa:forall a' : N, {Nless a a' = true} + {Nless a' a = true} + {a = a'}
Heqb:Nless 0 (N.double a) = true
{Nless (N.double a) 0 = true} + {true = true} +
{N.double a = 0%N}
a:N
IHa:forall a' : N,
{Nless a a' = true} + {Nless a' a = true} +
{a = a'}
Heqb:Nless 0 (N.double a) = false
{Nless (N.double a) 0 = true} + {false = true} +
{N.double a = 0%N}
      *a:N
IHa:forall a' : N, {Nless a a' = true} + {Nless a' a = true} + {a = a'}
Heqb:Nless 0 (N.double a) = true
{Nless (N.double a) 0 = true} + {true = true} +
{N.double a = 0%N} left.a:N
IHa:forall a' : N, {Nless a a' = true} + {Nless a' a = true} + {a = a'}
Heqb:Nless 0 (N.double a) = true
{Nless (N.double a) 0 = true} + {true = true} right.a:N
IHa:forall a' : N, {Nless a a' = true} + {Nless a' a = true} + {a = a'}
Heqb:Nless 0 (N.double a) = true
true = true auto.
      *a:N
IHa:forall a' : N, {Nless a a' = true} + {Nless a' a = true} + {a = a'}
Heqb:Nless 0 (N.double a) = false
{Nless (N.double a) 0 = true} + {false = true} +
{N.double a = 0%N} right.a:N
IHa:forall a' : N, {Nless a a' = true} + {Nless a' a = true} + {a = a'}
Heqb:Nless 0 (N.double a) = false
N.double a = 0%N exact (N0_less_2 _  Heqb).
    +a:N
IHa:forall a'0 : N, {Nless a a'0 = true} + {Nless a'0 a = true} + {a = a'0}
a':N
{Nless (N.double a) (N.double a') = true} +
{Nless (N.double a') (N.double a) = true} +
{N.double a = N.double a'} rewrite 2!Nless_def_1.a:N
IHa:forall a'0 : N, {Nless a a'0 = true} + {Nless a'0 a = true} + {a = a'0}
a':N
{Nless a a' = true} + {Nless a' a = true} +
{N.double a = N.double a'} destruct (IHa a') as [ | ->].a:N
IHa:forall a'0 : N, {Nless a a'0 = true} + {Nless a'0 a = true} + {a = a'0}
a':N
s:{Nless a a' = true} + {Nless a' a = true}
{Nless a a' = true} + {Nless a' a = true} +
{N.double a = N.double a'}
a':N
IHa:forall a'0 : N, {Nless a' a'0 = true} + {Nless a'0 a' = true} + {a' = a'0}
{Nless a' a' = true} + {Nless a' a' = true} +
{N.double a' = N.double a'}
      *a:N
IHa:forall a'0 : N, {Nless a a'0 = true} + {Nless a'0 a = true} + {a = a'0}
a':N
s:{Nless a a' = true} + {Nless a' a = true}
{Nless a a' = true} + {Nless a' a = true} +
{N.double a = N.double a'} left.a:N
IHa:forall a'0 : N, {Nless a a'0 = true} + {Nless a'0 a = true} + {a = a'0}
a':N
s:{Nless a a' = true} + {Nless a' a = true}
{Nless a a' = true} + {Nless a' a = true} assumption.
      *a':N
IHa:forall a'0 : N, {Nless a' a'0 = true} + {Nless a'0 a' = true} + {a' = a'0}
{Nless a' a' = true} + {Nless a' a' = true} +
{N.double a' = N.double a'} right.a':N
IHa:forall a'0 : N, {Nless a' a'0 = true} + {Nless a'0 a' = true} + {a' = a'0}
N.double a' = N.double a' reflexivity.
    +a:N
IHa:forall a'0 : N, {Nless a a'0 = true} + {Nless a'0 a = true} + {a = a'0}
a':N
{Nless (N.double a) (N.succ_double a') = true} +
{Nless (N.succ_double a') (N.double a) = true} +
{N.double a = N.succ_double a'} left.a:N
IHa:forall a'0 : N, {Nless a a'0 = true} + {Nless a'0 a = true} + {a = a'0}
a':N
{Nless (N.double a) (N.succ_double a') = true} +
{Nless (N.succ_double a') (N.double a) = true} left.a:N
IHa:forall a'0 : N, {Nless a a'0 = true} + {Nless a'0 a = true} + {a = a'0}
a':N
Nless (N.double a) (N.succ_double a') = true apply Nless_def_3.
  -a:N
IHa:forall a'0 : N, {Nless a a'0 = true} + {Nless a'0 a = true} + {a = a'0}
a':N
{Nless (N.succ_double a) a' = true} +
{Nless a' (N.succ_double a) = true} +
{N.succ_double a = a'} induction a' as [|a' _|a' _] using N.binary_rec.a:N
IHa:forall a' : N, {Nless a a' = true} + {Nless a' a = true} + {a = a'}
{Nless (N.succ_double a) 0 = true} +
{Nless 0 (N.succ_double a) = true} +
{N.succ_double a = 0%N}
a:N
IHa:forall a'0 : N, {Nless a a'0 = true} + {Nless a'0 a = true} + {a = a'0}
a':N
{Nless (N.succ_double a) (N.double a') = true} +
{Nless (N.double a') (N.succ_double a) = true} +
{N.succ_double a = N.double a'}
a:N
IHa:forall a'0 : N, {Nless a a'0 = true} + {Nless a'0 a = true} + {a = a'0}
a':N
{Nless (N.succ_double a) (N.succ_double a') = true} +
{Nless (N.succ_double a') (N.succ_double a) = true} +
{N.succ_double a = N.succ_double a'}
    +a:N
IHa:forall a' : N, {Nless a a' = true} + {Nless a' a = true} + {a = a'}
{Nless (N.succ_double a) 0 = true} +
{Nless 0 (N.succ_double a) = true} +
{N.succ_double a = 0%N} left.a:N
IHa:forall a' : N, {Nless a a' = true} + {Nless a' a = true} + {a = a'}
{Nless (N.succ_double a) 0 = true} +
{Nless 0 (N.succ_double a) = true} right.a:N
IHa:forall a' : N, {Nless a a' = true} + {Nless a' a = true} + {a = a'}
Nless 0 (N.succ_double a) = true destruct a; reflexivity.
    +a:N
IHa:forall a'0 : N, {Nless a a'0 = true} + {Nless a'0 a = true} + {a = a'0}
a':N
{Nless (N.succ_double a) (N.double a') = true} +
{Nless (N.double a') (N.succ_double a) = true} +
{N.succ_double a = N.double a'} left.a:N
IHa:forall a'0 : N, {Nless a a'0 = true} + {Nless a'0 a = true} + {a = a'0}
a':N
{Nless (N.succ_double a) (N.double a') = true} +
{Nless (N.double a') (N.succ_double a) = true} right.a:N
IHa:forall a'0 : N, {Nless a a'0 = true} + {Nless a'0 a = true} + {a = a'0}
a':N
Nless (N.double a') (N.succ_double a) = true apply Nless_def_3.
    +a:N
IHa:forall a'0 : N, {Nless a a'0 = true} + {Nless a'0 a = true} + {a = a'0}
a':N
{Nless (N.succ_double a) (N.succ_double a') = true} +
{Nless (N.succ_double a') (N.succ_double a) = true} +
{N.succ_double a = N.succ_double a'} rewrite 2!Nless_def_2.a:N
IHa:forall a'0 : N, {Nless a a'0 = true} + {Nless a'0 a = true} + {a = a'0}
a':N
{Nless a a' = true} + {Nless a' a = true} +
{N.succ_double a = N.succ_double a'} destruct (IHa a') as [ | ->].a:N
IHa:forall a'0 : N, {Nless a a'0 = true} + {Nless a'0 a = true} + {a = a'0}
a':N
s:{Nless a a' = true} + {Nless a' a = true}
{Nless a a' = true} + {Nless a' a = true} +
{N.succ_double a = N.succ_double a'}
a':N
IHa:forall a'0 : N, {Nless a' a'0 = true} + {Nless a'0 a' = true} + {a' = a'0}
{Nless a' a' = true} + {Nless a' a' = true} +
{N.succ_double a' = N.succ_double a'}
      *a:N
IHa:forall a'0 : N, {Nless a a'0 = true} + {Nless a'0 a = true} + {a = a'0}
a':N
s:{Nless a a' = true} + {Nless a' a = true}
{Nless a a' = true} + {Nless a' a = true} +
{N.succ_double a = N.succ_double a'} left.a:N
IHa:forall a'0 : N, {Nless a a'0 = true} + {Nless a'0 a = true} + {a = a'0}
a':N
s:{Nless a a' = true} + {Nless a' a = true}
{Nless a a' = true} + {Nless a' a = true} assumption.
      *a':N
IHa:forall a'0 : N, {Nless a' a'0 = true} + {Nless a'0 a' = true} + {a' = a'0}
{Nless a' a' = true} + {Nless a' a' = true} +
{N.succ_double a' = N.succ_double a'} right.a':N
IHa:forall a'0 : N, {Nless a' a'0 = true} + {Nless a'0 a' = true} + {a' = a'0}
N.succ_double a' = N.succ_double a' reflexivity.
Qed.

Number of digits in a number

Notation Nsize := N.size_nat (only parsing).

conversions between N and bit vectors.

Fixpoint P2Bv (p:positive) : Bvector (Pos.size_nat p) :=
 match p return Bvector (Pos.size_nat p) with
   | xH => Bvect_true 1%nat
   | xO p => Bcons false (Pos.size_nat p) (P2Bv p)
   | xI p => Bcons true (Pos.size_nat p) (P2Bv p)
 end.

Definition N2Bv (n:N) : Bvector (N.size_nat n) :=
  match n as n0 return Bvector (N.size_nat n0) with
    | N0 => Bnil
    | Npos p => P2Bv p
  end.

Fixpoint P2Bv_sized (m : nat) (p : positive) : Bvector m :=
  match m with
  | O => []
  | S m =>
    match p with
    | xI p => true  :: P2Bv_sized  m p
    | xO p => false :: P2Bv_sized  m p
    | xH   => true  :: Bvect_false m
    end
  end.

Definition N2Bv_sized (m : nat) (n : N) : Bvector m :=
  match n with
  | N0     => Bvect_false m
  | Npos p => P2Bv_sized  m p
  end.

Definition N2ByteV_sized (m : nat) : N -> ByteVector m :=
  of_Bvector ∘ N2Bv_sized (m * 8).

Fixpoint Bv2N (n:nat)(bv:Bvector n) : N :=
  match bv with
    | Vector.nil _ => N0
    | Vector.cons _ false n bv => N.double (Bv2N n bv)
    | Vector.cons _ true n bv => N.succ_double (Bv2N n bv)
  end.

Arguments Bv2N {n} bv, n bv.

Definition ByteV2N {n : nat} : ByteVector n -> N :=
  Bv2N ∘ to_Bvector.

Lemma Bv2N_N2Bv : forall n, Bv2N _ (N2Bv n) = n.forall n : N, Bv2N (N2Bv n) = n
Proof.forall n : N, Bv2N (N2Bv n) = n
destruct n.Bv2N (N2Bv 0) = 0%N
p:positive
Bv2N (N2Bv (N.pos p)) = N.pos p
simpl; auto.p:positive
Bv2N (N2Bv (N.pos p)) = N.pos p
induction p; simpl in *; auto; rewrite IHp; simpl; auto.
Qed.

The opposite composition is not so simple: if the considered bit vector has some zeros on its right, they will disappear during the return Bv2N translation:

Lemma Bv2N_Nsize : forall n (bv:Bvector n), N.size_nat (Bv2N n bv) <= n.forall (n : nat) (bv : Bvector n),
N.size_nat (Bv2N bv) <= n
Proof.forall (n : nat) (bv : Bvector n),
N.size_nat (Bv2N bv) <= n
induction bv; intros.N.size_nat (Bv2N []) <= 0
h:bool
n:nat
bv:VectorDef.t bool n
IHbv:N.size_nat (Bv2N bv) <= n
N.size_nat (Bv2N (h :: bv)) <= S n
auto.h:bool
n:nat
bv:VectorDef.t bool n
IHbv:N.size_nat (Bv2N bv) <= n
N.size_nat (Bv2N (h :: bv)) <= S n
simpl.h:bool
n:nat
bv:VectorDef.t bool n
IHbv:N.size_nat (Bv2N bv) <= n
N.size_nat
  (if h
   then N.succ_double (Bv2N bv)
   else N.double (Bv2N bv)) <= S n
destruct h;
 destruct (Bv2N n bv);
 simpl ; auto with arith.
Qed.

In the previous lemma, we can only replace the inequality by an equality whenever the highest bit is non-null.

Lemma Bv2N_Nsize_1 : forall n (bv:Bvector (S n)),
  Bsign _ bv = true <->
  N.size_nat (Bv2N _ bv) = (S n).forall (n : nat) (bv : Bvector (S n)),
Bsign n bv = true <-> N.size_nat (Bv2N bv) = S n
Proof.forall (n : nat) (bv : Bvector (S n)),
Bsign n bv = true <-> N.size_nat (Bv2N bv) = S n
apply Vector.rectS ; intros ; simpl.a:bool
a = true <-> N.size_nat (if a then 1%N else 0%N) = 1
a:bool
n:nat
v:Vector.t bool (S n)
H:Bsign n v = true <-> N.size_nat (Bv2N v) = S n
Bsign n v = true <->
N.size_nat
  (if a
   then N.succ_double (Bv2N v)
   else N.double (Bv2N v)) = S (S n)
destruct a ; compute ; split ; intros x ; now inversion x.a:bool
n:nat
v:Vector.t bool (S n)
H:Bsign n v = true <-> N.size_nat (Bv2N v) = S n
Bsign n v = true <->
N.size_nat
  (if a
   then N.succ_double (Bv2N v)
   else N.double (Bv2N v)) = S (S n)
 destruct a, (Bv2N (S n) v) ;
  simpl ;intuition ; try discriminate.
Qed.

Lemma Bv2N_upper_bound (n : nat) (bv : Bvector n) :
    (Bv2N bv < N.shiftl_nat 1 n)%N.n:nat
bv:Bvector n
(Bv2N bv < N.shiftl_nat 1 n)%N
Proof with simpl; auto.n:nat
bv:Bvector n
(Bv2N bv < N.shiftl_nat 1 n)%N
  induction bv...(0 < 1)%N
h:bool
n:nat
bv:VectorDef.t bool n
IHbv:(Bv2N bv < N.shiftl_nat 1 n)%N
((if h
  then N.succ_double (Bv2N bv)
  else N.double (Bv2N bv)) <
 N.double (N.shiftl_nat 1 n))%N
  -(0 < 1)%N constructor.
  -h:bool
n:nat
bv:VectorDef.t bool n
IHbv:(Bv2N bv < N.shiftl_nat 1 n)%N
((if h
  then N.succ_double (Bv2N bv)
  else N.double (Bv2N bv)) <
 N.double (N.shiftl_nat 1 n))%N destruct h.n:nat
bv:VectorDef.t bool n
IHbv:(Bv2N bv < N.shiftl_nat 1 n)%N
(N.succ_double (Bv2N bv) < N.double (N.shiftl_nat 1 n))%N
n:nat
bv:VectorDef.t bool n
IHbv:(Bv2N bv < N.shiftl_nat 1 n)%N
(N.double (Bv2N bv) < N.double (N.shiftl_nat 1 n))%N
    +n:nat
bv:VectorDef.t bool n
IHbv:(Bv2N bv < N.shiftl_nat 1 n)%N
(N.succ_double (Bv2N bv) < N.double (N.shiftl_nat 1 n))%N apply N.succ_double_lt...
    +n:nat
bv:VectorDef.t bool n
IHbv:(Bv2N bv < N.shiftl_nat 1 n)%N
(N.double (Bv2N bv) < N.double (N.shiftl_nat 1 n))%N apply N.double_lt_mono...
Qed.

Corollary ByteV2N_upper_bound (n : nat) (v : ByteVector n) :
  (ByteV2N v < N.shiftl_nat 1 (n * 8))%N.n:nat
v:ByteVector n
(ByteV2N v < N.shiftl_nat 1 (n * 8))%N
Proof.n:nat
v:ByteVector n
(ByteV2N v < N.shiftl_nat 1 (n * 8))%N
  unfold ByteV2N, compose.n:nat
v:ByteVector n
(Bv2N (to_Bvector v) < N.shiftl_nat 1 (n * 8))%N
  apply Bv2N_upper_bound.
Qed.

To state nonetheless a second result about composition of conversions, we define a conversion on a given number of bits :

#[deprecated(since = "8.9.0", note = "Use N2Bv_sized instead.")]
Fixpoint N2Bv_gen (n:nat)(a:N) : Bvector n :=
 match n return Bvector n with
   | 0 => Bnil
   | S n => match a with
       | N0 => Bvect_false (S n)
       | Npos xH => Bcons true _ (Bvect_false n)
       | Npos (xO p) => Bcons false _ (N2Bv_gen n (Npos p))
       | Npos (xI p) => Bcons true _ (N2Bv_gen n (Npos p))
      end
  end.

The first N2Bv is then a special case of N2Bv_gen

Lemma N2Bv_N2Bv_gen : forall (a:N), N2Bv a = N2Bv_gen (N.size_nat a) a.forall a : N, N2Bv a = N2Bv_gen (N.size_nat a) a
Proof.forall a : N, N2Bv a = N2Bv_gen (N.size_nat a) a
destruct a; simpl.Bnil = Bnil
p:positive
P2Bv p = N2Bv_gen (Pos.size_nat p) (N.pos p)
auto.p:positive
P2Bv p = N2Bv_gen (Pos.size_nat p) (N.pos p)
induction p; simpl; intros; auto; congruence.
Qed.

In fact, if k is large enough, N2Bv_gen k a contains all digits of a plus some zeros.

Lemma N2Bv_N2Bv_gen_above : forall (a:N)(k:nat),
 N2Bv_gen (N.size_nat a + k) a = Vector.append (N2Bv a) (Bvect_false k).forall (a : N) (k : nat),
N2Bv_gen (N.size_nat a + k) a =
N2Bv a ++ Bvect_false k
Proof.forall (a : N) (k : nat),
N2Bv_gen (N.size_nat a + k) a =
N2Bv a ++ Bvect_false k
destruct a; simpl.forall k : nat, N2Bv_gen k 0 = Bvect_false k
p:positive
forall k : nat,
N2Bv_gen (Pos.size_nat p + k) (N.pos p) =
P2Bv p ++ Bvect_false k
destruct k; simpl; auto.p:positive
forall k : nat,
N2Bv_gen (Pos.size_nat p + k) (N.pos p) =
P2Bv p ++ Bvect_false k
induction p; simpl; intros;unfold Bcons; f_equal; auto.
Qed.

Here comes now the second composition result.

Lemma N2Bv_Bv2N : forall n (bv:Bvector n),
   N2Bv_gen n (Bv2N n bv) = bv.forall (n : nat) (bv : Bvector n),
N2Bv_gen n (Bv2N bv) = bv
Proof.forall (n : nat) (bv : Bvector n),
N2Bv_gen n (Bv2N bv) = bv
induction bv; intros.N2Bv_gen 0 (Bv2N []) = []
h:bool
n:nat
bv:VectorDef.t bool n
IHbv:N2Bv_gen n (Bv2N bv) = bv
N2Bv_gen (S n) (Bv2N (h :: bv)) = h :: bv
auto.h:bool
n:nat
bv:VectorDef.t bool n
IHbv:N2Bv_gen n (Bv2N bv) = bv
N2Bv_gen (S n) (Bv2N (h :: bv)) = h :: bv
simpl.h:bool
n:nat
bv:VectorDef.t bool n
IHbv:N2Bv_gen n (Bv2N bv) = bv
match
  (if h
   then N.succ_double (Bv2N bv)
   else N.double (Bv2N bv))
with
| 0%N => false :: Bvect_false n
| N.pos (p~1)%positive =>
    Bcons true n (N2Bv_gen n (N.pos p))
| N.pos (p~0)%positive =>
    Bcons false n (N2Bv_gen n (N.pos p))
| 1%N => Bcons true n (Bvect_false n)
end = h :: bv
generalize IHbv; clear IHbv.h:bool
n:nat
bv:VectorDef.t bool n
N2Bv_gen n (Bv2N bv) = bv ->
match
  (if h
   then N.succ_double (Bv2N bv)
   else N.double (Bv2N bv))
with
| 0%N => false :: Bvect_false n
| N.pos (p~1)%positive =>
    Bcons true n (N2Bv_gen n (N.pos p))
| N.pos (p~0)%positive =>
    Bcons false n (N2Bv_gen n (N.pos p))
| 1%N => Bcons true n (Bvect_false n)
end = h :: bv
unfold Bcons.h:bool
n:nat
bv:VectorDef.t bool n
N2Bv_gen n (Bv2N bv) = bv ->
match
  (if h
   then N.succ_double (Bv2N bv)
   else N.double (Bv2N bv))
with
| 0%N => false :: Bvect_false n
| N.pos (p~1)%positive => true :: N2Bv_gen n (N.pos p)
| N.pos (p~0)%positive =>
    false :: N2Bv_gen n (N.pos p)
| 1%N => true :: Bvect_false n
end = h :: bv
destruct (Bv2N _ bv);
 destruct h; intro H; rewrite <- H; simpl; trivial;
  induction n; simpl; auto.
Qed.

accessing some precise bits.

Lemma Nbit0_Blow : forall n, forall (bv:Bvector (S n)),
  N.odd (Bv2N _ bv) = Blow _ bv.forall (n : nat) (bv : Bvector (S n)),
N.odd (Bv2N bv) = Blow n bv
Proof.forall (n : nat) (bv : Bvector (S n)),
N.odd (Bv2N bv) = Blow n bv
apply Vector.caseS.forall (h : bool) (n : nat) (t : Vector.t bool n),
N.odd (Bv2N (h :: t)) = Blow n (h :: t)
intros.h:bool
n:nat
t:Vector.t bool n
N.odd (Bv2N (h :: t)) = Blow n (h :: t)
unfold Blow.h:bool
n:nat
t:Vector.t bool n
N.odd (Bv2N (h :: t)) = Vector.hd (h :: t)
simpl.h:bool
n:nat
t:Vector.t bool n
N.odd
  (if h
   then N.succ_double (Bv2N t)
   else N.double (Bv2N t)) = h
destruct (Bv2N n t); simpl;
 destruct h; auto.
Qed.

Notation Bnth := (@Vector.nth_order bool).

Lemma Bnth_Nbit : forall n (bv:Bvector n) p (H:p<n),
  Bnth bv H = N.testbit_nat (Bv2N _ bv) p.forall (n : nat) (bv : Bvector n) (p : nat)
  (H : p < n), Bnth bv H = N.testbit_nat (Bv2N bv) p
Proof.forall (n : nat) (bv : Bvector n) (p : nat)
  (H : p < n), Bnth bv H = N.testbit_nat (Bv2N bv) p
induction bv; intros.p:nat
H:p < 0
Bnth [] H = N.testbit_nat (Bv2N []) p
h:bool
n:nat
bv:VectorDef.t bool n
IHbv:forall (p0 : nat) (H0 : p0 < n),
Bnth bv H0 = N.testbit_nat (Bv2N bv) p0
p:nat
H:p < S n
Bnth (h :: bv) H = N.testbit_nat (Bv2N (h :: bv)) p
inversion H.h:bool
n:nat
bv:VectorDef.t bool n
IHbv:forall (p0 : nat) (H0 : p0 < n),
Bnth bv H0 = N.testbit_nat (Bv2N bv) p0
p:nat
H:p < S n
Bnth (h :: bv) H = N.testbit_nat (Bv2N (h :: bv)) p
destruct p ; simpl.h:bool
n:nat
bv:VectorDef.t bool n
IHbv:forall (p : nat) (H0 : p < n),
Bnth bv H0 = N.testbit_nat (Bv2N bv) p
H:0 < S n
Bnth (h :: bv) H =
N.testbit_nat
  (if h
   then N.succ_double (Bv2N bv)
   else N.double (Bv2N bv)) 0
h:bool
n:nat
bv:VectorDef.t bool n
IHbv:forall (p0 : nat) (H0 : p0 < n),
Bnth bv H0 = N.testbit_nat (Bv2N bv) p0
p:nat
H:S p < S n
Bnth (h :: bv) H =
N.testbit_nat
  (if h
   then N.succ_double (Bv2N bv)
   else N.double (Bv2N bv)) 
  (S p)
  destruct (Bv2N n bv); destruct h; simpl in *; auto.h:bool
n:nat
bv:VectorDef.t bool n
IHbv:forall (p0 : nat) (H0 : p0 < n),
Bnth bv H0 = N.testbit_nat (Bv2N bv) p0
p:nat
H:S p < S n
Bnth (h :: bv) H =
N.testbit_nat
  (if h
   then N.succ_double (Bv2N bv)
   else N.double (Bv2N bv)) 
  (S p)
  specialize IHbv with p (Lt.lt_S_n _ _ H).h:bool
n:nat
bv:VectorDef.t bool n
p:nat
H:S p < S n
IHbv:Bnth bv (Lt.lt_S_n p n H) =
N.testbit_nat (Bv2N bv) p
Bnth (h :: bv) H =
N.testbit_nat
  (if h
   then N.succ_double (Bv2N bv)
   else N.double (Bv2N bv)) 
  (S p)
    simpl in * ; destruct (Bv2N n bv); destruct h; simpl in *; auto.
Qed.

Lemma Nbit_Nsize : forall n p, N.size_nat n <= p -> N.testbit_nat n p = false.forall (n : N) (p : nat),
N.size_nat n <= p -> N.testbit_nat n p = false
Proof.forall (n : N) (p : nat),
N.size_nat n <= p -> N.testbit_nat n p = false
destruct n as [|n].forall p : nat,
N.size_nat 0 <= p -> N.testbit_nat 0 p = false
n:positive
forall p : nat,
N.size_nat (N.pos n) <= p ->
N.testbit_nat (N.pos n) p = false
simpl; auto.n:positive
forall p : nat,
N.size_nat (N.pos n) <= p ->
N.testbit_nat (N.pos n) p = false
induction n; simpl in *; intros; destruct p; auto with arith.n:positive
IHn:forall p : nat, Pos.size_nat n <= p -> Pos.testbit_nat n p = false
H:S (Pos.size_nat n) <= 0
true = false
H:1 <= 0
true = false
inversion H.H:1 <= 0
true = false
inversion H.
Qed.

Lemma Nbit_Bth: forall n p (H:p < N.size_nat n),
  N.testbit_nat n p = Bnth (N2Bv n) H.forall (n : N) (p : nat) (H : p < N.size_nat n),
N.testbit_nat n p = Bnth (N2Bv n) H
Proof.forall (n : N) (p : nat) (H : p < N.size_nat n),
N.testbit_nat n p = Bnth (N2Bv n) H
destruct n as [|n].forall (p : nat) (H : p < N.size_nat 0),
N.testbit_nat 0 p = Bnth (N2Bv 0) H
n:positive
forall (p : nat) (H : p < N.size_nat (N.pos n)),
N.testbit_nat (N.pos n) p = Bnth (N2Bv (N.pos n)) H
inversion H.n:positive
forall (p : nat) (H : p < N.size_nat (N.pos n)),
N.testbit_nat (N.pos n) p = Bnth (N2Bv (N.pos n)) H
induction n ; destruct p ; unfold Vector.nth_order in *; simpl in * ; auto.p:nat
forall H : S p < 1,
false =
match
  Fin.of_nat_lt (Lt.lt_S_n p 0 H) in (Fin.t m')
  return (Vector.t bool m' -> bool)
with
| @Fin.F1 n =>
    Vector.caseS
      (fun (n0 : nat) (_ : Vector.t bool (S n0)) =>
       bool)
      (fun (h : bool) (n0 : nat)
         (_ : Vector.t bool n0) => h)
| @Fin.FS n p' =>
    fun v : Vector.t bool (S n) =>
    Vector.caseS
      (fun (n0 : nat) (_ : Vector.t bool (S n0)) =>
       Fin.t n0 -> bool)
      (fun (_ : bool) (n0 : nat)
         (t : Vector.t bool n0) (p0 : Fin.t n0) =>
       t[@p0]) v p'
end []
intros H ; destruct (Lt.lt_n_O _ (Lt.lt_S_n _ _ H)).
Qed.

Binary bitwise operations are the same in the two worlds.

Lemma Nxor_BVxor : forall n (bv bv' : Bvector n),
  Bv2N _ (BVxor _ bv bv') = N.lxor (Bv2N _ bv) (Bv2N _ bv').forall (n : nat) (bv bv' : Bvector n),
Bv2N (BVxor n bv bv') = N.lxor (Bv2N bv) (Bv2N bv')
Proof.forall (n : nat) (bv bv' : Bvector n),
Bv2N (BVxor n bv bv') = N.lxor (Bv2N bv) (Bv2N bv')
apply Vector.rect2 ; intros.Bv2N (BVxor 0 [] []) = N.lxor (Bv2N []) (Bv2N [])
n:nat
v1, v2:Vector.t bool n
H:Bv2N (BVxor n v1 v2) = N.lxor (Bv2N v1) (Bv2N v2)
a, b:bool
Bv2N (BVxor (S n) (a :: v1) (b :: v2)) =
N.lxor (Bv2N (a :: v1)) (Bv2N (b :: v2))
now simpl.n:nat
v1, v2:Vector.t bool n
H:Bv2N (BVxor n v1 v2) = N.lxor (Bv2N v1) (Bv2N v2)
a, b:bool
Bv2N (BVxor (S n) (a :: v1) (b :: v2)) =
N.lxor (Bv2N (a :: v1)) (Bv2N (b :: v2))
simpl.n:nat
v1, v2:Vector.t bool n
H:Bv2N (BVxor n v1 v2) = N.lxor (Bv2N v1) (Bv2N v2)
a, b:bool
(if xorb a b
 then N.succ_double (Bv2N (BVxor n v1 v2))
 else N.double (Bv2N (BVxor n v1 v2))) =
N.lxor
  (if a
   then N.succ_double (Bv2N v1)
   else N.double (Bv2N v1))
  (if b
   then N.succ_double (Bv2N v2)
   else N.double (Bv2N v2))
destruct a, b, (Bv2N n v1), (Bv2N n v2); simpl in *; rewrite H ; now simpl.
Qed.

Lemma Nand_BVand : forall n (bv bv' : Bvector n),
  Bv2N _ (BVand _ bv bv') = N.land (Bv2N _ bv) (Bv2N _ bv').forall (n : nat) (bv bv' : Bvector n),
Bv2N (BVand n bv bv') = N.land (Bv2N bv) (Bv2N bv')
Proof.forall (n : nat) (bv bv' : Bvector n),
Bv2N (BVand n bv bv') = N.land (Bv2N bv) (Bv2N bv')
refine (@Vector.rect2 _ _ _ _ _); simpl; intros; auto.n:nat
v1, v2:Vector.t bool n
H:Bv2N (BVand n v1 v2) = N.land (Bv2N v1) (Bv2N v2)
a, b:bool
(if a && b
 then N.succ_double (Bv2N (BVand n v1 v2))
 else N.double (Bv2N (BVand n v1 v2))) =
N.land
  (if a
   then N.succ_double (Bv2N v1)
   else N.double (Bv2N v1))
  (if b
   then N.succ_double (Bv2N v2)
   else N.double (Bv2N v2))
rewrite H.n:nat
v1, v2:Vector.t bool n
H:Bv2N (BVand n v1 v2) = N.land (Bv2N v1) (Bv2N v2)
a, b:bool
(if a && b
 then N.succ_double (N.land (Bv2N v1) (Bv2N v2))
 else N.double (N.land (Bv2N v1) (Bv2N v2))) =
N.land
  (if a
   then N.succ_double (Bv2N v1)
   else N.double (Bv2N v1))
  (if b
   then N.succ_double (Bv2N v2)
   else N.double (Bv2N v2))
destruct a, b, (Bv2N n v1), (Bv2N n v2);
 simpl; auto.
Qed.

Lemma N2Bv_sized_Nsize (n : N) :
  N2Bv_sized (N.size_nat n) n = N2Bv n.n:N
N2Bv_sized (N.size_nat n) n = N2Bv n
Proof with simpl; auto.n:N
N2Bv_sized (N.size_nat n) n = N2Bv n
  destruct n...p:positive
P2Bv_sized (Pos.size_nat p) p = P2Bv p
  induction p...p:positive
IHp:P2Bv_sized (Pos.size_nat p) p = P2Bv p
true :: P2Bv_sized (Pos.size_nat p) p =
Bcons true (Pos.size_nat p) (P2Bv p)
p:positive
IHp:P2Bv_sized (Pos.size_nat p) p = P2Bv p
false :: P2Bv_sized (Pos.size_nat p) p =
Bcons false (Pos.size_nat p) (P2Bv p)
  all: rewrite IHp...
Qed.

Lemma N2Bv_sized_Bv2N (n : nat) (v : Bvector n) :
  N2Bv_sized n (Bv2N n v) = v.n:nat
v:Bvector n
N2Bv_sized n (Bv2N v) = v
Proof with simpl; auto.n:nat
v:Bvector n
N2Bv_sized n (Bv2N v) = v
  induction v...h:bool
n:nat
v:VectorDef.t bool n
IHv:N2Bv_sized n (Bv2N v) = v
N2Bv_sized (S n)
  (if h
   then N.succ_double (Bv2N v)
   else N.double (Bv2N v)) = h :: v
  destruct h;
  unfold N2Bv_sized;
  destruct (Bv2N n v) as [|[]];
  rewrite <- IHv...
Qed.

Lemma N2Bv_N2Bv_sized_above (a : N) (k : nat) :
  N2Bv_sized (N.size_nat a + k) a = N2Bv a ++ Bvect_false k.a:N
k:nat
N2Bv_sized (N.size_nat a + k) a =
N2Bv a ++ Bvect_false k
Proof with auto.a:N
k:nat
N2Bv_sized (N.size_nat a + k) a =
N2Bv a ++ Bvect_false k
  destruct a...p:positive
k:nat
N2Bv_sized (N.size_nat (N.pos p) + k) (N.pos p) =
N2Bv (N.pos p) ++ Bvect_false k
  induction p; simpl; f_equal...
Qed.