Ndist.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 Arith.
Require Import Min.
Require Import BinPos.
Require Import BinNat.
Require Import Ndigits.

An ultrametric distance over N numbers

Inductive natinf : Set :=
  | infty : natinf
  | ni : nat -> natinf.

Fixpoint Pplength (p:positive) : nat :=
  match p with
  | xH => 0
  | xI _ => 0
  | xO p' => S (Pplength p')
  end.

Definition Nplength (a:N) :=
  match a with
  | N0 => infty
  | Npos p => ni (Pplength p)
  end.

Lemma Nplength_infty : forall a:N, Nplength a = infty -> a = N0.forall a : N, Nplength a = infty -> a = 0%N
Proof.forall a : N, Nplength a = infty -> a = 0%N
  simple induction a; trivial.a:N
forall p : positive,
Nplength (N.pos p) = infty -> N.pos p = 0%N
  unfold Nplength; intros; discriminate H.
Qed.

Lemma Nplength_zeros :
 forall (a:N) (n:nat),
   Nplength a = ni n -> forall k:nat, k < n -> N.testbit_nat a k = false.forall (a : N) (n : nat),
Nplength a = ni n ->
forall k : nat, k < n -> N.testbit_nat a k = false
Proof.forall (a : N) (n : nat),
Nplength a = ni n ->
forall k : nat, k < n -> N.testbit_nat a k = false
  simple induction a; trivial.a:N
forall (p : positive) (n : nat),
Nplength (N.pos p) = ni n ->
forall k : nat,
k < n -> N.testbit_nat (N.pos p) k = false
  simple induction p.a:N
p:positive
forall p0 : positive,
(forall n : nat,
 Nplength (N.pos p0) = ni n ->
 forall k : nat,
 k < n -> N.testbit_nat (N.pos p0) k = false) ->
forall n : nat,
Nplength (N.pos p0~1) = ni n ->
forall k : nat,
k < n -> N.testbit_nat (N.pos p0~1) k = false
a:N
p:positive
forall p0 : positive,
(forall n : nat,
 Nplength (N.pos p0) = ni n ->
 forall k : nat,
 k < n -> N.testbit_nat (N.pos p0) k = false) ->
forall n : nat,
Nplength (N.pos p0~0) = ni n ->
forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
a:N
p:positive
forall n : nat,
Nplength 1 = ni n ->
forall k : nat, k < n -> N.testbit_nat 1 k = false simple induction n.a:N
p, p0:positive
H:forall n0 : nat,
Nplength (N.pos p0) = ni n0 ->
forall k : nat,
k < n0 -> N.testbit_nat (N.pos p0) k = false
n:nat
Nplength (N.pos p0~1) = ni 0 ->
forall k : nat,
k < 0 -> N.testbit_nat (N.pos p0~1) k = false
a:N
p, p0:positive
H:forall n0 : nat,
Nplength (N.pos p0) = ni n0 ->
forall k : nat,
k < n0 -> N.testbit_nat (N.pos p0) k = false
n:nat
forall n0 : nat,
(Nplength (N.pos p0~1) = ni n0 ->
 forall k : nat,
 k < n0 -> N.testbit_nat (N.pos p0~1) k = false) ->
Nplength (N.pos p0~1) = ni (S n0) ->
forall k : nat,
k < S n0 -> N.testbit_nat (N.pos p0~1) k = false
a:N
p:positive
forall p0 : positive,
(forall n : nat,
 Nplength (N.pos p0) = ni n ->
 forall k : nat,
 k < n -> N.testbit_nat (N.pos p0) k = false) ->
forall n : nat,
Nplength (N.pos p0~0) = ni n ->
forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
a:N
p:positive
forall n : nat,
Nplength 1 = ni n ->
forall k : nat, k < n -> N.testbit_nat 1 k = false intros.a:N
p, p0:positive
H:forall n0 : nat,
Nplength (N.pos p0) = ni n0 ->
forall k0 : nat,
k0 < n0 -> N.testbit_nat (N.pos p0) k0 = false
n:nat
H0:Nplength (N.pos p0~1) = ni 0
k:nat
H1:k < 0
N.testbit_nat (N.pos p0~1) k = false
a:N
p, p0:positive
H:forall n0 : nat,
Nplength (N.pos p0) = ni n0 ->
forall k : nat,
k < n0 -> N.testbit_nat (N.pos p0) k = false
n:nat
forall n0 : nat,
(Nplength (N.pos p0~1) = ni n0 ->
 forall k : nat,
 k < n0 -> N.testbit_nat (N.pos p0~1) k = false) ->
Nplength (N.pos p0~1) = ni (S n0) ->
forall k : nat,
k < S n0 -> N.testbit_nat (N.pos p0~1) k = false
a:N
p:positive
forall p0 : positive,
(forall n : nat,
 Nplength (N.pos p0) = ni n ->
 forall k : nat,
 k < n -> N.testbit_nat (N.pos p0) k = false) ->
forall n : nat,
Nplength (N.pos p0~0) = ni n ->
forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
a:N
p:positive
forall n : nat,
Nplength 1 = ni n ->
forall k : nat, k < n -> N.testbit_nat 1 k = false inversion H1.a:N
p, p0:positive
H:forall n0 : nat,
Nplength (N.pos p0) = ni n0 ->
forall k : nat,
k < n0 -> N.testbit_nat (N.pos p0) k = false
n:nat
forall n0 : nat,
(Nplength (N.pos p0~1) = ni n0 ->
 forall k : nat,
 k < n0 -> N.testbit_nat (N.pos p0~1) k = false) ->
Nplength (N.pos p0~1) = ni (S n0) ->
forall k : nat,
k < S n0 -> N.testbit_nat (N.pos p0~1) k = false
a:N
p:positive
forall p0 : positive,
(forall n : nat,
 Nplength (N.pos p0) = ni n ->
 forall k : nat,
 k < n -> N.testbit_nat (N.pos p0) k = false) ->
forall n : nat,
Nplength (N.pos p0~0) = ni n ->
forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
a:N
p:positive
forall n : nat,
Nplength 1 = ni n ->
forall k : nat, k < n -> N.testbit_nat 1 k = false
  simple induction k.a:N
p, p0:positive
H:forall n1 : nat,
Nplength (N.pos p0) = ni n1 ->
forall k0 : nat,
k0 < n1 -> N.testbit_nat (N.pos p0) k0 = false
n, n0:nat
H0:Nplength (N.pos p0~1) = ni n0 ->
forall k0 : nat,
k0 < n0 -> N.testbit_nat (N.pos p0~1) k0 = false
H1:Nplength (N.pos p0~1) = ni (S n0)
k:nat
0 < S n0 -> N.testbit_nat (N.pos p0~1) 0 = false
a:N
p, p0:positive
H:forall n1 : nat,
Nplength (N.pos p0) = ni n1 ->
forall k0 : nat,
k0 < n1 -> N.testbit_nat (N.pos p0) k0 = false
n, n0:nat
H0:Nplength (N.pos p0~1) = ni n0 ->
forall k0 : nat,
k0 < n0 -> N.testbit_nat (N.pos p0~1) k0 = false
H1:Nplength (N.pos p0~1) = ni (S n0)
k:nat
forall n1 : nat,
(n1 < S n0 -> N.testbit_nat (N.pos p0~1) n1 = false) ->
S n1 < S n0 ->
N.testbit_nat (N.pos p0~1) (S n1) = false
a:N
p:positive
forall p0 : positive,
(forall n : nat,
 Nplength (N.pos p0) = ni n ->
 forall k : nat,
 k < n -> N.testbit_nat (N.pos p0) k = false) ->
forall n : nat,
Nplength (N.pos p0~0) = ni n ->
forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
a:N
p:positive
forall n : nat,
Nplength 1 = ni n ->
forall k : nat, k < n -> N.testbit_nat 1 k = false simpl in H1.a:N
p, p0:positive
H:forall n1 : nat,
Nplength (N.pos p0) = ni n1 ->
forall k0 : nat,
k0 < n1 -> N.testbit_nat (N.pos p0) k0 = false
n, n0:nat
H0:Nplength (N.pos p0~1) = ni n0 ->
forall k0 : nat,
k0 < n0 -> N.testbit_nat (N.pos p0~1) k0 = false
H1:ni 0 = ni (S n0)
k:nat
0 < S n0 -> N.testbit_nat (N.pos p0~1) 0 = false
a:N
p, p0:positive
H:forall n1 : nat,
Nplength (N.pos p0) = ni n1 ->
forall k0 : nat,
k0 < n1 -> N.testbit_nat (N.pos p0) k0 = false
n, n0:nat
H0:Nplength (N.pos p0~1) = ni n0 ->
forall k0 : nat,
k0 < n0 -> N.testbit_nat (N.pos p0~1) k0 = false
H1:Nplength (N.pos p0~1) = ni (S n0)
k:nat
forall n1 : nat,
(n1 < S n0 -> N.testbit_nat (N.pos p0~1) n1 = false) ->
S n1 < S n0 ->
N.testbit_nat (N.pos p0~1) (S n1) = false
a:N
p:positive
forall p0 : positive,
(forall n : nat,
 Nplength (N.pos p0) = ni n ->
 forall k : nat,
 k < n -> N.testbit_nat (N.pos p0) k = false) ->
forall n : nat,
Nplength (N.pos p0~0) = ni n ->
forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
a:N
p:positive
forall n : nat,
Nplength 1 = ni n ->
forall k : nat, k < n -> N.testbit_nat 1 k = false discriminate H1.a:N
p, p0:positive
H:forall n1 : nat,
Nplength (N.pos p0) = ni n1 ->
forall k0 : nat,
k0 < n1 -> N.testbit_nat (N.pos p0) k0 = false
n, n0:nat
H0:Nplength (N.pos p0~1) = ni n0 ->
forall k0 : nat,
k0 < n0 -> N.testbit_nat (N.pos p0~1) k0 = false
H1:Nplength (N.pos p0~1) = ni (S n0)
k:nat
forall n1 : nat,
(n1 < S n0 -> N.testbit_nat (N.pos p0~1) n1 = false) ->
S n1 < S n0 ->
N.testbit_nat (N.pos p0~1) (S n1) = false
a:N
p:positive
forall p0 : positive,
(forall n : nat,
 Nplength (N.pos p0) = ni n ->
 forall k : nat,
 k < n -> N.testbit_nat (N.pos p0) k = false) ->
forall n : nat,
Nplength (N.pos p0~0) = ni n ->
forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
a:N
p:positive
forall n : nat,
Nplength 1 = ni n ->
forall k : nat, k < n -> N.testbit_nat 1 k = false
  intros.a:N
p, p0:positive
H:forall n2 : nat,
Nplength (N.pos p0) = ni n2 ->
forall k0 : nat,
k0 < n2 -> N.testbit_nat (N.pos p0) k0 = false
n, n0:nat
H0:Nplength (N.pos p0~1) = ni n0 ->
forall k0 : nat,
k0 < n0 -> N.testbit_nat (N.pos p0~1) k0 = false
H1:Nplength (N.pos p0~1) = ni (S n0)
k, n1:nat
H2:n1 < S n0 ->
N.testbit_nat (N.pos p0~1) n1 = false
H3:S n1 < S n0
N.testbit_nat (N.pos p0~1) (S n1) = false
a:N
p:positive
forall p0 : positive,
(forall n : nat,
 Nplength (N.pos p0) = ni n ->
 forall k : nat,
 k < n -> N.testbit_nat (N.pos p0) k = false) ->
forall n : nat,
Nplength (N.pos p0~0) = ni n ->
forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
a:N
p:positive
forall n : nat,
Nplength 1 = ni n ->
forall k : nat, k < n -> N.testbit_nat 1 k = false simpl in H1.a:N
p, p0:positive
H:forall n2 : nat,
Nplength (N.pos p0) = ni n2 ->
forall k0 : nat,
k0 < n2 -> N.testbit_nat (N.pos p0) k0 = false
n, n0:nat
H0:Nplength (N.pos p0~1) = ni n0 ->
forall k0 : nat,
k0 < n0 -> N.testbit_nat (N.pos p0~1) k0 = false
H1:ni 0 = ni (S n0)
k, n1:nat
H2:n1 < S n0 ->
N.testbit_nat (N.pos p0~1) n1 = false
H3:S n1 < S n0
N.testbit_nat (N.pos p0~1) (S n1) = false
a:N
p:positive
forall p0 : positive,
(forall n : nat,
 Nplength (N.pos p0) = ni n ->
 forall k : nat,
 k < n -> N.testbit_nat (N.pos p0) k = false) ->
forall n : nat,
Nplength (N.pos p0~0) = ni n ->
forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
a:N
p:positive
forall n : nat,
Nplength 1 = ni n ->
forall k : nat, k < n -> N.testbit_nat 1 k = false discriminate H1.a:N
p:positive
forall p0 : positive,
(forall n : nat,
 Nplength (N.pos p0) = ni n ->
 forall k : nat,
 k < n -> N.testbit_nat (N.pos p0) k = false) ->
forall n : nat,
Nplength (N.pos p0~0) = ni n ->
forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
a:N
p:positive
forall n : nat,
Nplength 1 = ni n ->
forall k : nat, k < n -> N.testbit_nat 1 k = false
  simple induction k.a:N
p, p0:positive
H:forall n0 : nat,
Nplength (N.pos p0) = ni n0 ->
forall k0 : nat,
k0 < n0 -> N.testbit_nat (N.pos p0) k0 = false
n:nat
H0:Nplength (N.pos p0~0) = ni n
k:nat
0 < n -> N.testbit_nat (N.pos p0~0) 0 = false
a:N
p, p0:positive
H:forall n0 : nat,
Nplength (N.pos p0) = ni n0 ->
forall k0 : nat,
k0 < n0 -> N.testbit_nat (N.pos p0) k0 = false
n:nat
H0:Nplength (N.pos p0~0) = ni n
k:nat
forall n0 : nat,
(n0 < n -> N.testbit_nat (N.pos p0~0) n0 = false) ->
S n0 < n -> N.testbit_nat (N.pos p0~0) (S n0) = false
a:N
p:positive
forall n : nat,
Nplength 1 = ni n ->
forall k : nat, k < n -> N.testbit_nat 1 k = false trivial.a:N
p, p0:positive
H:forall n0 : nat,
Nplength (N.pos p0) = ni n0 ->
forall k0 : nat,
k0 < n0 -> N.testbit_nat (N.pos p0) k0 = false
n:nat
H0:Nplength (N.pos p0~0) = ni n
k:nat
forall n0 : nat,
(n0 < n -> N.testbit_nat (N.pos p0~0) n0 = false) ->
S n0 < n -> N.testbit_nat (N.pos p0~0) (S n0) = false
a:N
p:positive
forall n : nat,
Nplength 1 = ni n ->
forall k : nat, k < n -> N.testbit_nat 1 k = false
  generalize H0.a:N
p, p0:positive
H:forall n0 : nat,
Nplength (N.pos p0) = ni n0 ->
forall k0 : nat,
k0 < n0 -> N.testbit_nat (N.pos p0) k0 = false
n:nat
H0:Nplength (N.pos p0~0) = ni n
k:nat
Nplength (N.pos p0~0) = ni n ->
forall n0 : nat,
(n0 < n -> N.testbit_nat (N.pos p0~0) n0 = false) ->
S n0 < n -> N.testbit_nat (N.pos p0~0) (S n0) = false
a:N
p:positive
forall n : nat,
Nplength 1 = ni n ->
forall k : nat, k < n -> N.testbit_nat 1 k = false case n.a:N
p, p0:positive
H:forall n0 : nat,
Nplength (N.pos p0) = ni n0 ->
forall k0 : nat,
k0 < n0 -> N.testbit_nat (N.pos p0) k0 = false
n:nat
H0:Nplength (N.pos p0~0) = ni n
k:nat
Nplength (N.pos p0~0) = ni 0 ->
forall n0 : nat,
(n0 < 0 -> N.testbit_nat (N.pos p0~0) n0 = false) ->
S n0 < 0 -> N.testbit_nat (N.pos p0~0) (S n0) = false
a:N
p, p0:positive
H:forall n0 : nat,
Nplength (N.pos p0) = ni n0 ->
forall k0 : nat,
k0 < n0 -> N.testbit_nat (N.pos p0) k0 = false
n:nat
H0:Nplength (N.pos p0~0) = ni n
k:nat
forall n0 : nat,
Nplength (N.pos p0~0) = ni (S n0) ->
forall n1 : nat,
(n1 < S n0 -> N.testbit_nat (N.pos p0~0) n1 = false) ->
S n1 < S n0 ->
N.testbit_nat (N.pos p0~0) (S n1) = false
a:N
p:positive
forall n : nat,
Nplength 1 = ni n ->
forall k : nat, k < n -> N.testbit_nat 1 k = false intros.a:N
p, p0:positive
H:forall n1 : nat,
Nplength (N.pos p0) = ni n1 ->
forall k0 : nat,
k0 < n1 -> N.testbit_nat (N.pos p0) k0 = false
n:nat
H0:Nplength (N.pos p0~0) = ni n
k:nat
H1:Nplength (N.pos p0~0) = ni 0
n0:nat
H2:n0 < 0 -> N.testbit_nat (N.pos p0~0) n0 = false
H3:S n0 < 0
N.testbit_nat (N.pos p0~0) (S n0) = false
a:N
p, p0:positive
H:forall n0 : nat,
Nplength (N.pos p0) = ni n0 ->
forall k0 : nat,
k0 < n0 -> N.testbit_nat (N.pos p0) k0 = false
n:nat
H0:Nplength (N.pos p0~0) = ni n
k:nat
forall n0 : nat,
Nplength (N.pos p0~0) = ni (S n0) ->
forall n1 : nat,
(n1 < S n0 -> N.testbit_nat (N.pos p0~0) n1 = false) ->
S n1 < S n0 ->
N.testbit_nat (N.pos p0~0) (S n1) = false
a:N
p:positive
forall n : nat,
Nplength 1 = ni n ->
forall k : nat, k < n -> N.testbit_nat 1 k = false inversion H3.a:N
p, p0:positive
H:forall n0 : nat,
Nplength (N.pos p0) = ni n0 ->
forall k0 : nat,
k0 < n0 -> N.testbit_nat (N.pos p0) k0 = false
n:nat
H0:Nplength (N.pos p0~0) = ni n
k:nat
forall n0 : nat,
Nplength (N.pos p0~0) = ni (S n0) ->
forall n1 : nat,
(n1 < S n0 -> N.testbit_nat (N.pos p0~0) n1 = false) ->
S n1 < S n0 ->
N.testbit_nat (N.pos p0~0) (S n1) = false
a:N
p:positive
forall n : nat,
Nplength 1 = ni n ->
forall k : nat, k < n -> N.testbit_nat 1 k = false
  intros.a:N
p, p0:positive
H:forall n2 : nat,
Nplength (N.pos p0) = ni n2 ->
forall k0 : nat,
k0 < n2 -> N.testbit_nat (N.pos p0) k0 = false
n:nat
H0:Nplength (N.pos p0~0) = ni n
k, n0:nat
H1:Nplength (N.pos p0~0) = ni (S n0)
n1:nat
H2:n1 < S n0 ->
N.testbit_nat (N.pos p0~0) n1 = false
H3:S n1 < S n0
N.testbit_nat (N.pos p0~0) (S n1) = false
a:N
p:positive
forall n : nat,
Nplength 1 = ni n ->
forall k : nat, k < n -> N.testbit_nat 1 k = false simpl.a:N
p, p0:positive
H:forall n2 : nat,
Nplength (N.pos p0) = ni n2 ->
forall k0 : nat,
k0 < n2 -> N.testbit_nat (N.pos p0) k0 = false
n:nat
H0:Nplength (N.pos p0~0) = ni n
k, n0:nat
H1:Nplength (N.pos p0~0) = ni (S n0)
n1:nat
H2:n1 < S n0 ->
N.testbit_nat (N.pos p0~0) n1 = false
H3:S n1 < S n0
Pos.testbit_nat p0 n1 = false
a:N
p:positive
forall n : nat,
Nplength 1 = ni n ->
forall k : nat, k < n -> N.testbit_nat 1 k = false unfold N.testbit_nat in H.a:N
p, p0:positive
H:forall n2 : nat,
Nplength (N.pos p0) = ni n2 ->
forall k0 : nat,
k0 < n2 -> Pos.testbit_nat p0 k0 = false
n:nat
H0:Nplength (N.pos p0~0) = ni n
k, n0:nat
H1:Nplength (N.pos p0~0) = ni (S n0)
n1:nat
H2:n1 < S n0 ->
N.testbit_nat (N.pos p0~0) n1 = false
H3:S n1 < S n0
Pos.testbit_nat p0 n1 = false
a:N
p:positive
forall n : nat,
Nplength 1 = ni n ->
forall k : nat, k < n -> N.testbit_nat 1 k = false apply (H n0).a:N
p, p0:positive
H:forall n2 : nat,
Nplength (N.pos p0) = ni n2 ->
forall k0 : nat,
k0 < n2 -> Pos.testbit_nat p0 k0 = false
n:nat
H0:Nplength (N.pos p0~0) = ni n
k, n0:nat
H1:Nplength (N.pos p0~0) = ni (S n0)
n1:nat
H2:n1 < S n0 ->
N.testbit_nat (N.pos p0~0) n1 = false
H3:S n1 < S n0
Nplength (N.pos p0) = ni n0
a:N
p, p0:positive
H:forall n2 : nat,
Nplength (N.pos p0) = ni n2 ->
forall k0 : nat,
k0 < n2 -> Pos.testbit_nat p0 k0 = false
n:nat
H0:Nplength (N.pos p0~0) = ni n
k, n0:nat
H1:Nplength (N.pos p0~0) = ni (S n0)
n1:nat
H2:n1 < S n0 ->
N.testbit_nat (N.pos p0~0) n1 = false
H3:S n1 < S n0
n1 < n0
a:N
p:positive
forall n : nat,
Nplength 1 = ni n ->
forall k : nat, k < n -> N.testbit_nat 1 k = false simpl in H1.a:N
p, p0:positive
H:forall n2 : nat,
Nplength (N.pos p0) = ni n2 ->
forall k0 : nat,
k0 < n2 -> Pos.testbit_nat p0 k0 = false
n:nat
H0:Nplength (N.pos p0~0) = ni n
k, n0:nat
H1:ni (S (Pplength p0)) = ni (S n0)
n1:nat
H2:n1 < S n0 ->
N.testbit_nat (N.pos p0~0) n1 = false
H3:S n1 < S n0
Nplength (N.pos p0) = ni n0
a:N
p, p0:positive
H:forall n2 : nat,
Nplength (N.pos p0) = ni n2 ->
forall k0 : nat,
k0 < n2 -> Pos.testbit_nat p0 k0 = false
n:nat
H0:Nplength (N.pos p0~0) = ni n
k, n0:nat
H1:Nplength (N.pos p0~0) = ni (S n0)
n1:nat
H2:n1 < S n0 ->
N.testbit_nat (N.pos p0~0) n1 = false
H3:S n1 < S n0
n1 < n0
a:N
p:positive
forall n : nat,
Nplength 1 = ni n ->
forall k : nat, k < n -> N.testbit_nat 1 k = false inversion H1.a:N
p, p0:positive
H:forall n2 : nat,
Nplength (N.pos p0) = ni n2 ->
forall k0 : nat,
k0 < n2 -> Pos.testbit_nat p0 k0 = false
n:nat
H0:Nplength (N.pos p0~0) = ni n
k, n0:nat
H1:ni (S (Pplength p0)) = ni (S n0)
n1:nat
H2:n1 < S n0 ->
N.testbit_nat (N.pos p0~0) n1 = false
H3:S n1 < S n0
H5:Pplength p0 = n0
Nplength (N.pos p0) = ni (Pplength p0)
a:N
p, p0:positive
H:forall n2 : nat,
Nplength (N.pos p0) = ni n2 ->
forall k0 : nat,
k0 < n2 -> Pos.testbit_nat p0 k0 = false
n:nat
H0:Nplength (N.pos p0~0) = ni n
k, n0:nat
H1:Nplength (N.pos p0~0) = ni (S n0)
n1:nat
H2:n1 < S n0 ->
N.testbit_nat (N.pos p0~0) n1 = false
H3:S n1 < S n0
n1 < n0
a:N
p:positive
forall n : nat,
Nplength 1 = ni n ->
forall k : nat, k < n -> N.testbit_nat 1 k = false reflexivity.a:N
p, p0:positive
H:forall n2 : nat,
Nplength (N.pos p0) = ni n2 ->
forall k0 : nat,
k0 < n2 -> Pos.testbit_nat p0 k0 = false
n:nat
H0:Nplength (N.pos p0~0) = ni n
k, n0:nat
H1:Nplength (N.pos p0~0) = ni (S n0)
n1:nat
H2:n1 < S n0 ->
N.testbit_nat (N.pos p0~0) n1 = false
H3:S n1 < S n0
n1 < n0
a:N
p:positive
forall n : nat,
Nplength 1 = ni n ->
forall k : nat, k < n -> N.testbit_nat 1 k = false
  exact (lt_S_n n1 n0 H3).a:N
p:positive
forall n : nat,
Nplength 1 = ni n ->
forall k : nat, k < n -> N.testbit_nat 1 k = false
  simpl.a:N
p:positive
forall n : nat,
ni 0 = ni n ->
forall k : nat,
k < n ->
match k with
| 0 => true
| S _ => false
end = false intros n H.a:N
p:positive
n:nat
H:ni 0 = ni n
forall k : nat,
k < n ->
match k with
| 0 => true
| S _ => false
end = false inversion H.a:N
p:positive
n:nat
H:ni 0 = ni n
H1:0 = n
forall k : nat,
k < 0 ->
match k with
| 0 => true
| S _ => false
end = false intros.a:N
p:positive
n:nat
H:ni 0 = ni n
H1:0 = n
k:nat
H0:k < 0
match k with
| 0 => true
| S _ => false
end = false inversion H0.
Qed.

Lemma Nplength_one :
 forall (a:N) (n:nat), Nplength a = ni n -> N.testbit_nat a n = true.forall (a : N) (n : nat),
Nplength a = ni n -> N.testbit_nat a n = true
Proof.forall (a : N) (n : nat),
Nplength a = ni n -> N.testbit_nat a n = true
  simple induction a.a:N
forall n : nat,
Nplength 0 = ni n -> N.testbit_nat 0 n = true
a:N
forall (p : positive) (n : nat),
Nplength (N.pos p) = ni n ->
N.testbit_nat (N.pos p) n = true intros.a:N
n:nat
H:Nplength 0 = ni n
N.testbit_nat 0 n = true
a:N
forall (p : positive) (n : nat),
Nplength (N.pos p) = ni n ->
N.testbit_nat (N.pos p) n = true inversion H.a:N
forall (p : positive) (n : nat),
Nplength (N.pos p) = ni n ->
N.testbit_nat (N.pos p) n = true
  simple induction p.a:N
p:positive
forall p0 : positive,
(forall n : nat,
 Nplength (N.pos p0) = ni n ->
 N.testbit_nat (N.pos p0) n = true) ->
forall n : nat,
Nplength (N.pos p0~1) = ni n ->
N.testbit_nat (N.pos p0~1) n = true
a:N
p:positive
forall p0 : positive,
(forall n : nat,
 Nplength (N.pos p0) = ni n ->
 N.testbit_nat (N.pos p0) n = true) ->
forall n : nat,
Nplength (N.pos p0~0) = ni n ->
N.testbit_nat (N.pos p0~0) n = true
a:N
p:positive
forall n : nat,
Nplength 1 = ni n -> N.testbit_nat 1 n = true intros.a:N
p, p0:positive
H:forall n0 : nat,
Nplength (N.pos p0) = ni n0 ->
N.testbit_nat (N.pos p0) n0 = true
n:nat
H0:Nplength (N.pos p0~1) = ni n
N.testbit_nat (N.pos p0~1) n = true
a:N
p:positive
forall p0 : positive,
(forall n : nat,
 Nplength (N.pos p0) = ni n ->
 N.testbit_nat (N.pos p0) n = true) ->
forall n : nat,
Nplength (N.pos p0~0) = ni n ->
N.testbit_nat (N.pos p0~0) n = true
a:N
p:positive
forall n : nat,
Nplength 1 = ni n -> N.testbit_nat 1 n = true simpl in H0.a:N
p, p0:positive
H:forall n0 : nat,
Nplength (N.pos p0) = ni n0 ->
N.testbit_nat (N.pos p0) n0 = true
n:nat
H0:ni 0 = ni n
N.testbit_nat (N.pos p0~1) n = true
a:N
p:positive
forall p0 : positive,
(forall n : nat,
 Nplength (N.pos p0) = ni n ->
 N.testbit_nat (N.pos p0) n = true) ->
forall n : nat,
Nplength (N.pos p0~0) = ni n ->
N.testbit_nat (N.pos p0~0) n = true
a:N
p:positive
forall n : nat,
Nplength 1 = ni n -> N.testbit_nat 1 n = true inversion H0.a:N
p, p0:positive
H:forall n0 : nat,
Nplength (N.pos p0) = ni n0 ->
N.testbit_nat (N.pos p0) n0 = true
n:nat
H0:ni 0 = ni n
H2:0 = n
N.testbit_nat (N.pos p0~1) 0 = true
a:N
p:positive
forall p0 : positive,
(forall n : nat,
 Nplength (N.pos p0) = ni n ->
 N.testbit_nat (N.pos p0) n = true) ->
forall n : nat,
Nplength (N.pos p0~0) = ni n ->
N.testbit_nat (N.pos p0~0) n = true
a:N
p:positive
forall n : nat,
Nplength 1 = ni n -> N.testbit_nat 1 n = true reflexivity.a:N
p:positive
forall p0 : positive,
(forall n : nat,
 Nplength (N.pos p0) = ni n ->
 N.testbit_nat (N.pos p0) n = true) ->
forall n : nat,
Nplength (N.pos p0~0) = ni n ->
N.testbit_nat (N.pos p0~0) n = true
a:N
p:positive
forall n : nat,
Nplength 1 = ni n -> N.testbit_nat 1 n = true
  intros.a:N
p, p0:positive
H:forall n0 : nat,
Nplength (N.pos p0) = ni n0 ->
N.testbit_nat (N.pos p0) n0 = true
n:nat
H0:Nplength (N.pos p0~0) = ni n
N.testbit_nat (N.pos p0~0) n = true
a:N
p:positive
forall n : nat,
Nplength 1 = ni n -> N.testbit_nat 1 n = true simpl in H0.a:N
p, p0:positive
H:forall n0 : nat,
Nplength (N.pos p0) = ni n0 ->
N.testbit_nat (N.pos p0) n0 = true
n:nat
H0:ni (S (Pplength p0)) = ni n
N.testbit_nat (N.pos p0~0) n = true
a:N
p:positive
forall n : nat,
Nplength 1 = ni n -> N.testbit_nat 1 n = true inversion H0.a:N
p, p0:positive
H:forall n0 : nat,
Nplength (N.pos p0) = ni n0 ->
N.testbit_nat (N.pos p0) n0 = true
n:nat
H0:ni (S (Pplength p0)) = ni n
H2:S (Pplength p0) = n
N.testbit_nat (N.pos p0~0) (S (Pplength p0)) = true
a:N
p:positive
forall n : nat,
Nplength 1 = ni n -> N.testbit_nat 1 n = true simpl.a:N
p, p0:positive
H:forall n0 : nat,
Nplength (N.pos p0) = ni n0 ->
N.testbit_nat (N.pos p0) n0 = true
n:nat
H0:ni (S (Pplength p0)) = ni n
H2:S (Pplength p0) = n
Pos.testbit_nat p0 (Pplength p0) = true
a:N
p:positive
forall n : nat,
Nplength 1 = ni n -> N.testbit_nat 1 n = true unfold N.testbit_nat in H.a:N
p, p0:positive
H:forall n0 : nat,
Nplength (N.pos p0) = ni n0 ->
Pos.testbit_nat p0 n0 = true
n:nat
H0:ni (S (Pplength p0)) = ni n
H2:S (Pplength p0) = n
Pos.testbit_nat p0 (Pplength p0) = true
a:N
p:positive
forall n : nat,
Nplength 1 = ni n -> N.testbit_nat 1 n = true apply H.a:N
p, p0:positive
H:forall n0 : nat,
Nplength (N.pos p0) = ni n0 ->
Pos.testbit_nat p0 n0 = true
n:nat
H0:ni (S (Pplength p0)) = ni n
H2:S (Pplength p0) = n
Nplength (N.pos p0) = ni (Pplength p0)
a:N
p:positive
forall n : nat,
Nplength 1 = ni n -> N.testbit_nat 1 n = true reflexivity.a:N
p:positive
forall n : nat,
Nplength 1 = ni n -> N.testbit_nat 1 n = true
  intros.a:N
p:positive
n:nat
H:Nplength 1 = ni n
N.testbit_nat 1 n = true simpl in H.a:N
p:positive
n:nat
H:ni 0 = ni n
N.testbit_nat 1 n = true inversion H.a:N
p:positive
n:nat
H:ni 0 = ni n
H1:0 = n
N.testbit_nat 1 0 = true reflexivity.
Qed.

Lemma Nplength_first_one :
 forall (a:N) (n:nat),
   (forall k:nat, k < n -> N.testbit_nat a k = false) ->
   N.testbit_nat a n = true -> Nplength a = ni n.forall (a : N) (n : nat),
(forall k : nat, k < n -> N.testbit_nat a k = false) ->
N.testbit_nat a n = true -> Nplength a = ni n
Proof.forall (a : N) (n : nat),
(forall k : nat, k < n -> N.testbit_nat a k = false) ->
N.testbit_nat a n = true -> Nplength a = ni n
  simple induction a.a:N
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 0 k = false) ->
N.testbit_nat 0 n = true -> Nplength 0 = ni n
a:N
forall (p : positive) (n : nat),
(forall k : nat,
 k < n -> N.testbit_nat (N.pos p) k = false) ->
N.testbit_nat (N.pos p) n = true ->
Nplength (N.pos p) = ni n intros.a:N
n:nat
H:forall k : nat, k < n -> N.testbit_nat 0 k = false
H0:N.testbit_nat 0 n = true
Nplength 0 = ni n
a:N
forall (p : positive) (n : nat),
(forall k : nat,
 k < n -> N.testbit_nat (N.pos p) k = false) ->
N.testbit_nat (N.pos p) n = true ->
Nplength (N.pos p) = ni n simpl in H0.a:N
n:nat
H:forall k : nat, k < n -> N.testbit_nat 0 k = false
H0:false = true
Nplength 0 = ni n
a:N
forall (p : positive) (n : nat),
(forall k : nat,
 k < n -> N.testbit_nat (N.pos p) k = false) ->
N.testbit_nat (N.pos p) n = true ->
Nplength (N.pos p) = ni n discriminate H0.a:N
forall (p : positive) (n : nat),
(forall k : nat,
 k < n -> N.testbit_nat (N.pos p) k = false) ->
N.testbit_nat (N.pos p) n = true ->
Nplength (N.pos p) = ni n
  simple induction p.a:N
p:positive
forall p0 : positive,
(forall n : nat,
 (forall k : nat,
  k < n -> N.testbit_nat (N.pos p0) k = false) ->
 N.testbit_nat (N.pos p0) n = true ->
 Nplength (N.pos p0) = ni n) ->
forall n : nat,
(forall k : nat,
 k < n -> N.testbit_nat (N.pos p0~1) k = false) ->
N.testbit_nat (N.pos p0~1) n = true ->
Nplength (N.pos p0~1) = ni n
a:N
p:positive
forall p0 : positive,
(forall n : nat,
 (forall k : nat,
  k < n -> N.testbit_nat (N.pos p0) k = false) ->
 N.testbit_nat (N.pos p0) n = true ->
 Nplength (N.pos p0) = ni n) ->
forall n : nat,
(forall k : nat,
 k < n -> N.testbit_nat (N.pos p0~0) k = false) ->
N.testbit_nat (N.pos p0~0) n = true ->
Nplength (N.pos p0~0) = ni n
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n intros.a:N
p, p0:positive
H:forall n0 : nat,
(forall k : nat,
 k < n0 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n0 = true ->
Nplength (N.pos p0) = ni n0
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~1) k = false
H1:N.testbit_nat (N.pos p0~1) n = true
Nplength (N.pos p0~1) = ni n
a:N
p:positive
forall p0 : positive,
(forall n : nat,
 (forall k : nat,
  k < n -> N.testbit_nat (N.pos p0) k = false) ->
 N.testbit_nat (N.pos p0) n = true ->
 Nplength (N.pos p0) = ni n) ->
forall n : nat,
(forall k : nat,
 k < n -> N.testbit_nat (N.pos p0~0) k = false) ->
N.testbit_nat (N.pos p0~0) n = true ->
Nplength (N.pos p0~0) = ni n
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n generalize H0.a:N
p, p0:positive
H:forall n0 : nat,
(forall k : nat,
 k < n0 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n0 = true ->
Nplength (N.pos p0) = ni n0
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~1) k = false
H1:N.testbit_nat (N.pos p0~1) n = true
(forall k : nat,
 k < n -> N.testbit_nat (N.pos p0~1) k = false) ->
Nplength (N.pos p0~1) = ni n
a:N
p:positive
forall p0 : positive,
(forall n : nat,
 (forall k : nat,
  k < n -> N.testbit_nat (N.pos p0) k = false) ->
 N.testbit_nat (N.pos p0) n = true ->
 Nplength (N.pos p0) = ni n) ->
forall n : nat,
(forall k : nat,
 k < n -> N.testbit_nat (N.pos p0~0) k = false) ->
N.testbit_nat (N.pos p0~0) n = true ->
Nplength (N.pos p0~0) = ni n
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n case n.a:N
p, p0:positive
H:forall n0 : nat,
(forall k : nat,
 k < n0 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n0 = true ->
Nplength (N.pos p0) = ni n0
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~1) k = false
H1:N.testbit_nat (N.pos p0~1) n = true
(forall k : nat,
 k < 0 -> N.testbit_nat (N.pos p0~1) k = false) ->
Nplength (N.pos p0~1) = ni 0
a:N
p, p0:positive
H:forall n0 : nat,
(forall k : nat,
 k < n0 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n0 = true ->
Nplength (N.pos p0) = ni n0
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~1) k = false
H1:N.testbit_nat (N.pos p0~1) n = true
forall n0 : nat,
(forall k : nat,
 k < S n0 -> N.testbit_nat (N.pos p0~1) k = false) ->
Nplength (N.pos p0~1) = ni (S n0)
a:N
p:positive
forall p0 : positive,
(forall n : nat,
 (forall k : nat,
  k < n -> N.testbit_nat (N.pos p0) k = false) ->
 N.testbit_nat (N.pos p0) n = true ->
 Nplength (N.pos p0) = ni n) ->
forall n : nat,
(forall k : nat,
 k < n -> N.testbit_nat (N.pos p0~0) k = false) ->
N.testbit_nat (N.pos p0~0) n = true ->
Nplength (N.pos p0~0) = ni n
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n intros.a:N
p, p0:positive
H:forall n0 : nat,
(forall k : nat,
 k < n0 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n0 = true ->
Nplength (N.pos p0) = ni n0
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~1) k = false
H1:N.testbit_nat (N.pos p0~1) n = true
H2:forall k : nat,
k < 0 -> N.testbit_nat (N.pos p0~1) k = false
Nplength (N.pos p0~1) = ni 0
a:N
p, p0:positive
H:forall n0 : nat,
(forall k : nat,
 k < n0 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n0 = true ->
Nplength (N.pos p0) = ni n0
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~1) k = false
H1:N.testbit_nat (N.pos p0~1) n = true
forall n0 : nat,
(forall k : nat,
 k < S n0 -> N.testbit_nat (N.pos p0~1) k = false) ->
Nplength (N.pos p0~1) = ni (S n0)
a:N
p:positive
forall p0 : positive,
(forall n : nat,
 (forall k : nat,
  k < n -> N.testbit_nat (N.pos p0) k = false) ->
 N.testbit_nat (N.pos p0) n = true ->
 Nplength (N.pos p0) = ni n) ->
forall n : nat,
(forall k : nat,
 k < n -> N.testbit_nat (N.pos p0~0) k = false) ->
N.testbit_nat (N.pos p0~0) n = true ->
Nplength (N.pos p0~0) = ni n
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n reflexivity.a:N
p, p0:positive
H:forall n0 : nat,
(forall k : nat,
 k < n0 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n0 = true ->
Nplength (N.pos p0) = ni n0
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~1) k = false
H1:N.testbit_nat (N.pos p0~1) n = true
forall n0 : nat,
(forall k : nat,
 k < S n0 -> N.testbit_nat (N.pos p0~1) k = false) ->
Nplength (N.pos p0~1) = ni (S n0)
a:N
p:positive
forall p0 : positive,
(forall n : nat,
 (forall k : nat,
  k < n -> N.testbit_nat (N.pos p0) k = false) ->
 N.testbit_nat (N.pos p0) n = true ->
 Nplength (N.pos p0) = ni n) ->
forall n : nat,
(forall k : nat,
 k < n -> N.testbit_nat (N.pos p0~0) k = false) ->
N.testbit_nat (N.pos p0~0) n = true ->
Nplength (N.pos p0~0) = ni n
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n
  intros.a:N
p, p0:positive
H:forall n1 : nat,
(forall k : nat,
 k < n1 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n1 = true ->
Nplength (N.pos p0) = ni n1
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~1) k = false
H1:N.testbit_nat (N.pos p0~1) n = true
n0:nat
H2:forall k : nat,
k < S n0 -> N.testbit_nat (N.pos p0~1) k = false
Nplength (N.pos p0~1) = ni (S n0)
a:N
p:positive
forall p0 : positive,
(forall n : nat,
 (forall k : nat,
  k < n -> N.testbit_nat (N.pos p0) k = false) ->
 N.testbit_nat (N.pos p0) n = true ->
 Nplength (N.pos p0) = ni n) ->
forall n : nat,
(forall k : nat,
 k < n -> N.testbit_nat (N.pos p0~0) k = false) ->
N.testbit_nat (N.pos p0~0) n = true ->
Nplength (N.pos p0~0) = ni n
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n absurd (N.testbit_nat (Npos (xI p0)) 0 = false).a:N
p, p0:positive
H:forall n1 : nat,
(forall k : nat,
 k < n1 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n1 = true ->
Nplength (N.pos p0) = ni n1
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~1) k = false
H1:N.testbit_nat (N.pos p0~1) n = true
n0:nat
H2:forall k : nat,
k < S n0 -> N.testbit_nat (N.pos p0~1) k = false
N.testbit_nat (N.pos p0~1) 0 <> false
a:N
p, p0:positive
H:forall n1 : nat,
(forall k : nat,
 k < n1 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n1 = true ->
Nplength (N.pos p0) = ni n1
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~1) k = false
H1:N.testbit_nat (N.pos p0~1) n = true
n0:nat
H2:forall k : nat,
k < S n0 -> N.testbit_nat (N.pos p0~1) k = false
N.testbit_nat (N.pos p0~1) 0 = false
a:N
p:positive
forall p0 : positive,
(forall n : nat,
 (forall k : nat,
  k < n -> N.testbit_nat (N.pos p0) k = false) ->
 N.testbit_nat (N.pos p0) n = true ->
 Nplength (N.pos p0) = ni n) ->
forall n : nat,
(forall k : nat,
 k < n -> N.testbit_nat (N.pos p0~0) k = false) ->
N.testbit_nat (N.pos p0~0) n = true ->
Nplength (N.pos p0~0) = ni n
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n trivial with bool.a:N
p, p0:positive
H:forall n1 : nat,
(forall k : nat,
 k < n1 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n1 = true ->
Nplength (N.pos p0) = ni n1
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~1) k = false
H1:N.testbit_nat (N.pos p0~1) n = true
n0:nat
H2:forall k : nat,
k < S n0 -> N.testbit_nat (N.pos p0~1) k = false
N.testbit_nat (N.pos p0~1) 0 = false
a:N
p:positive
forall p0 : positive,
(forall n : nat,
 (forall k : nat,
  k < n -> N.testbit_nat (N.pos p0) k = false) ->
 N.testbit_nat (N.pos p0) n = true ->
 Nplength (N.pos p0) = ni n) ->
forall n : nat,
(forall k : nat,
 k < n -> N.testbit_nat (N.pos p0~0) k = false) ->
N.testbit_nat (N.pos p0~0) n = true ->
Nplength (N.pos p0~0) = ni n
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n
  auto with bool arith.a:N
p:positive
forall p0 : positive,
(forall n : nat,
 (forall k : nat,
  k < n -> N.testbit_nat (N.pos p0) k = false) ->
 N.testbit_nat (N.pos p0) n = true ->
 Nplength (N.pos p0) = ni n) ->
forall n : nat,
(forall k : nat,
 k < n -> N.testbit_nat (N.pos p0~0) k = false) ->
N.testbit_nat (N.pos p0~0) n = true ->
Nplength (N.pos p0~0) = ni n
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n
  intros.a:N
p, p0:positive
H:forall n0 : nat,
(forall k : nat,
 k < n0 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n0 = true ->
Nplength (N.pos p0) = ni n0
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
H1:N.testbit_nat (N.pos p0~0) n = true
Nplength (N.pos p0~0) = ni n
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n generalize H0 H1.a:N
p, p0:positive
H:forall n0 : nat,
(forall k : nat,
 k < n0 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n0 = true ->
Nplength (N.pos p0) = ni n0
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
H1:N.testbit_nat (N.pos p0~0) n = true
(forall k : nat,
 k < n -> N.testbit_nat (N.pos p0~0) k = false) ->
N.testbit_nat (N.pos p0~0) n = true ->
Nplength (N.pos p0~0) = ni n
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n case n.a:N
p, p0:positive
H:forall n0 : nat,
(forall k : nat,
 k < n0 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n0 = true ->
Nplength (N.pos p0) = ni n0
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
H1:N.testbit_nat (N.pos p0~0) n = true
(forall k : nat,
 k < 0 -> N.testbit_nat (N.pos p0~0) k = false) ->
N.testbit_nat (N.pos p0~0) 0 = true ->
Nplength (N.pos p0~0) = ni 0
a:N
p, p0:positive
H:forall n0 : nat,
(forall k : nat,
 k < n0 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n0 = true ->
Nplength (N.pos p0) = ni n0
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
H1:N.testbit_nat (N.pos p0~0) n = true
forall n0 : nat,
(forall k : nat,
 k < S n0 -> N.testbit_nat (N.pos p0~0) k = false) ->
N.testbit_nat (N.pos p0~0) (S n0) = true ->
Nplength (N.pos p0~0) = ni (S n0)
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n intros.a:N
p, p0:positive
H:forall n0 : nat,
(forall k : nat,
 k < n0 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n0 = true ->
Nplength (N.pos p0) = ni n0
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
H1:N.testbit_nat (N.pos p0~0) n = true
H2:forall k : nat,
k < 0 -> N.testbit_nat (N.pos p0~0) k = false
H3:N.testbit_nat (N.pos p0~0) 0 = true
Nplength (N.pos p0~0) = ni 0
a:N
p, p0:positive
H:forall n0 : nat,
(forall k : nat,
 k < n0 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n0 = true ->
Nplength (N.pos p0) = ni n0
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
H1:N.testbit_nat (N.pos p0~0) n = true
forall n0 : nat,
(forall k : nat,
 k < S n0 -> N.testbit_nat (N.pos p0~0) k = false) ->
N.testbit_nat (N.pos p0~0) (S n0) = true ->
Nplength (N.pos p0~0) = ni (S n0)
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n simpl in H3.a:N
p, p0:positive
H:forall n0 : nat,
(forall k : nat,
 k < n0 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n0 = true ->
Nplength (N.pos p0) = ni n0
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
H1:N.testbit_nat (N.pos p0~0) n = true
H2:forall k : nat,
k < 0 -> N.testbit_nat (N.pos p0~0) k = false
H3:false = true
Nplength (N.pos p0~0) = ni 0
a:N
p, p0:positive
H:forall n0 : nat,
(forall k : nat,
 k < n0 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n0 = true ->
Nplength (N.pos p0) = ni n0
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
H1:N.testbit_nat (N.pos p0~0) n = true
forall n0 : nat,
(forall k : nat,
 k < S n0 -> N.testbit_nat (N.pos p0~0) k = false) ->
N.testbit_nat (N.pos p0~0) (S n0) = true ->
Nplength (N.pos p0~0) = ni (S n0)
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n discriminate H3.a:N
p, p0:positive
H:forall n0 : nat,
(forall k : nat,
 k < n0 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n0 = true ->
Nplength (N.pos p0) = ni n0
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
H1:N.testbit_nat (N.pos p0~0) n = true
forall n0 : nat,
(forall k : nat,
 k < S n0 -> N.testbit_nat (N.pos p0~0) k = false) ->
N.testbit_nat (N.pos p0~0) (S n0) = true ->
Nplength (N.pos p0~0) = ni (S n0)
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n
  intros.a:N
p, p0:positive
H:forall n1 : nat,
(forall k : nat,
 k < n1 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n1 = true ->
Nplength (N.pos p0) = ni n1
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
H1:N.testbit_nat (N.pos p0~0) n = true
n0:nat
H2:forall k : nat,
k < S n0 -> N.testbit_nat (N.pos p0~0) k = false
H3:N.testbit_nat (N.pos p0~0) (S n0) = true
Nplength (N.pos p0~0) = ni (S n0)
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n simpl.a:N
p, p0:positive
H:forall n1 : nat,
(forall k : nat,
 k < n1 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n1 = true ->
Nplength (N.pos p0) = ni n1
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
H1:N.testbit_nat (N.pos p0~0) n = true
n0:nat
H2:forall k : nat,
k < S n0 -> N.testbit_nat (N.pos p0~0) k = false
H3:N.testbit_nat (N.pos p0~0) (S n0) = true
ni (S (Pplength p0)) = ni (S n0)
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n unfold Nplength in H.a:N
p, p0:positive
H:forall n1 : nat,
(forall k : nat,
 k < n1 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n1 = true ->
ni (Pplength p0) = ni n1
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
H1:N.testbit_nat (N.pos p0~0) n = true
n0:nat
H2:forall k : nat,
k < S n0 -> N.testbit_nat (N.pos p0~0) k = false
H3:N.testbit_nat (N.pos p0~0) (S n0) = true
ni (S (Pplength p0)) = ni (S n0)
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n
  enough (ni (Pplength p0) = ni n0) by (inversion H4; reflexivity).a:N
p, p0:positive
H:forall n1 : nat,
(forall k : nat,
 k < n1 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n1 = true ->
ni (Pplength p0) = ni n1
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
H1:N.testbit_nat (N.pos p0~0) n = true
n0:nat
H2:forall k : nat,
k < S n0 -> N.testbit_nat (N.pos p0~0) k = false
H3:N.testbit_nat (N.pos p0~0) (S n0) = true
ni (Pplength p0) = ni n0
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n
  apply H.a:N
p, p0:positive
H:forall n1 : nat,
(forall k : nat,
 k < n1 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n1 = true ->
ni (Pplength p0) = ni n1
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
H1:N.testbit_nat (N.pos p0~0) n = true
n0:nat
H2:forall k : nat,
k < S n0 -> N.testbit_nat (N.pos p0~0) k = false
H3:N.testbit_nat (N.pos p0~0) (S n0) = true
forall k : nat,
k < n0 -> N.testbit_nat (N.pos p0) k = false
a:N
p, p0:positive
H:forall n1 : nat,
(forall k : nat,
 k < n1 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n1 = true ->
ni (Pplength p0) = ni n1
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
H1:N.testbit_nat (N.pos p0~0) n = true
n0:nat
H2:forall k : nat,
k < S n0 -> N.testbit_nat (N.pos p0~0) k = false
H3:N.testbit_nat (N.pos p0~0) (S n0) = true
N.testbit_nat (N.pos p0) n0 = true
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n intros.a:N
p, p0:positive
H:forall n1 : nat,
(forall k0 : nat,
 k0 < n1 -> N.testbit_nat (N.pos p0) k0 = false) ->
N.testbit_nat (N.pos p0) n1 = true ->
ni (Pplength p0) = ni n1
n:nat
H0:forall k0 : nat,
k0 < n -> N.testbit_nat (N.pos p0~0) k0 = false
H1:N.testbit_nat (N.pos p0~0) n = true
n0:nat
H2:forall k0 : nat,
k0 < S n0 ->
N.testbit_nat (N.pos p0~0) k0 = false
H3:N.testbit_nat (N.pos p0~0) (S n0) = true
k:nat
H4:k < n0
N.testbit_nat (N.pos p0) k = false
a:N
p, p0:positive
H:forall n1 : nat,
(forall k : nat,
 k < n1 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n1 = true ->
ni (Pplength p0) = ni n1
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
H1:N.testbit_nat (N.pos p0~0) n = true
n0:nat
H2:forall k : nat,
k < S n0 -> N.testbit_nat (N.pos p0~0) k = false
H3:N.testbit_nat (N.pos p0~0) (S n0) = true
N.testbit_nat (N.pos p0) n0 = true
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n change (N.testbit_nat (Npos (xO p0)) (S k) = false).a:N
p, p0:positive
H:forall n1 : nat,
(forall k0 : nat,
 k0 < n1 -> N.testbit_nat (N.pos p0) k0 = false) ->
N.testbit_nat (N.pos p0) n1 = true ->
ni (Pplength p0) = ni n1
n:nat
H0:forall k0 : nat,
k0 < n -> N.testbit_nat (N.pos p0~0) k0 = false
H1:N.testbit_nat (N.pos p0~0) n = true
n0:nat
H2:forall k0 : nat,
k0 < S n0 ->
N.testbit_nat (N.pos p0~0) k0 = false
H3:N.testbit_nat (N.pos p0~0) (S n0) = true
k:nat
H4:k < n0
N.testbit_nat (N.pos p0~0) (S k) = false
a:N
p, p0:positive
H:forall n1 : nat,
(forall k : nat,
 k < n1 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n1 = true ->
ni (Pplength p0) = ni n1
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
H1:N.testbit_nat (N.pos p0~0) n = true
n0:nat
H2:forall k : nat,
k < S n0 -> N.testbit_nat (N.pos p0~0) k = false
H3:N.testbit_nat (N.pos p0~0) (S n0) = true
N.testbit_nat (N.pos p0) n0 = true
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n apply H2.a:N
p, p0:positive
H:forall n1 : nat,
(forall k0 : nat,
 k0 < n1 -> N.testbit_nat (N.pos p0) k0 = false) ->
N.testbit_nat (N.pos p0) n1 = true ->
ni (Pplength p0) = ni n1
n:nat
H0:forall k0 : nat,
k0 < n -> N.testbit_nat (N.pos p0~0) k0 = false
H1:N.testbit_nat (N.pos p0~0) n = true
n0:nat
H2:forall k0 : nat,
k0 < S n0 ->
N.testbit_nat (N.pos p0~0) k0 = false
H3:N.testbit_nat (N.pos p0~0) (S n0) = true
k:nat
H4:k < n0
S k < S n0
a:N
p, p0:positive
H:forall n1 : nat,
(forall k : nat,
 k < n1 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n1 = true ->
ni (Pplength p0) = ni n1
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
H1:N.testbit_nat (N.pos p0~0) n = true
n0:nat
H2:forall k : nat,
k < S n0 -> N.testbit_nat (N.pos p0~0) k = false
H3:N.testbit_nat (N.pos p0~0) (S n0) = true
N.testbit_nat (N.pos p0) n0 = true
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n apply lt_n_S.a:N
p, p0:positive
H:forall n1 : nat,
(forall k0 : nat,
 k0 < n1 -> N.testbit_nat (N.pos p0) k0 = false) ->
N.testbit_nat (N.pos p0) n1 = true ->
ni (Pplength p0) = ni n1
n:nat
H0:forall k0 : nat,
k0 < n -> N.testbit_nat (N.pos p0~0) k0 = false
H1:N.testbit_nat (N.pos p0~0) n = true
n0:nat
H2:forall k0 : nat,
k0 < S n0 ->
N.testbit_nat (N.pos p0~0) k0 = false
H3:N.testbit_nat (N.pos p0~0) (S n0) = true
k:nat
H4:k < n0
k < n0
a:N
p, p0:positive
H:forall n1 : nat,
(forall k : nat,
 k < n1 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n1 = true ->
ni (Pplength p0) = ni n1
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
H1:N.testbit_nat (N.pos p0~0) n = true
n0:nat
H2:forall k : nat,
k < S n0 -> N.testbit_nat (N.pos p0~0) k = false
H3:N.testbit_nat (N.pos p0~0) (S n0) = true
N.testbit_nat (N.pos p0) n0 = true
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n exact H4.a:N
p, p0:positive
H:forall n1 : nat,
(forall k : nat,
 k < n1 -> N.testbit_nat (N.pos p0) k = false) ->
N.testbit_nat (N.pos p0) n1 = true ->
ni (Pplength p0) = ni n1
n:nat
H0:forall k : nat,
k < n -> N.testbit_nat (N.pos p0~0) k = false
H1:N.testbit_nat (N.pos p0~0) n = true
n0:nat
H2:forall k : nat,
k < S n0 -> N.testbit_nat (N.pos p0~0) k = false
H3:N.testbit_nat (N.pos p0~0) (S n0) = true
N.testbit_nat (N.pos p0) n0 = true
a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n
  exact H3.a:N
p:positive
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n
  intro.a:N
p:positive
n:nat
(forall k : nat, k < n -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 n = true -> Nplength 1 = ni n case n.a:N
p:positive
n:nat
(forall k : nat, k < 0 -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 0 = true -> Nplength 1 = ni 0
a:N
p:positive
n:nat
forall n0 : nat,
(forall k : nat, k < S n0 -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 (S n0) = true ->
Nplength 1 = ni (S n0) trivial.a:N
p:positive
n:nat
forall n0 : nat,
(forall k : nat, k < S n0 -> N.testbit_nat 1 k = false) ->
N.testbit_nat 1 (S n0) = true ->
Nplength 1 = ni (S n0)
  intros.a:N
p:positive
n, n0:nat
H:forall k : nat,
k < S n0 -> N.testbit_nat 1 k = false
H0:N.testbit_nat 1 (S n0) = true
Nplength 1 = ni (S n0) simpl in H0.a:N
p:positive
n, n0:nat
H:forall k : nat,
k < S n0 -> N.testbit_nat 1 k = false
H0:false = true
Nplength 1 = ni (S n0) discriminate H0.
Qed.

Definition ni_min (d d':natinf) :=
  match d with
  | infty => d'
  | ni n => match d' with
            | infty => d
            | ni n' => ni (min n n')
            end
  end.

Lemma ni_min_idemp : forall d:natinf, ni_min d d = d.forall d : natinf, ni_min d d = d
Proof.forall d : natinf, ni_min d d = d
  simple induction d; trivial.d:natinf
forall n : nat, ni_min (ni n) (ni n) = ni n
  unfold ni_min.d:natinf
forall n : nat, ni (Nat.min n n) = ni n
  simple induction n; trivial.d:natinf
n:nat
forall n0 : nat,
ni (Nat.min n0 n0) = ni n0 ->
ni (Nat.min (S n0) (S n0)) = ni (S n0)
  intros.d:natinf
n, n0:nat
H:ni (Nat.min n0 n0) = ni n0
ni (Nat.min (S n0) (S n0)) = ni (S n0)
  simpl.d:natinf
n, n0:nat
H:ni (Nat.min n0 n0) = ni n0
ni (S (Nat.min n0 n0)) = ni (S n0)
  inversion H.d:natinf
n, n0:nat
H:ni (Nat.min n0 n0) = ni n0
H1:Nat.min n0 n0 = n0
ni (S (Nat.min (Nat.min n0 n0) (Nat.min n0 n0))) =
ni (S (Nat.min n0 n0))
  rewrite H1.d:natinf
n, n0:nat
H:ni (Nat.min n0 n0) = ni n0
H1:Nat.min n0 n0 = n0
ni (S (Nat.min n0 n0)) = ni (S n0)
  rewrite H1.d:natinf
n, n0:nat
H:ni (Nat.min n0 n0) = ni n0
H1:Nat.min n0 n0 = n0
ni (S n0) = ni (S n0)
  reflexivity.
Qed.

Lemma ni_min_comm : forall d d':natinf, ni_min d d' = ni_min d' d.forall d d' : natinf, ni_min d d' = ni_min d' d
Proof.forall d d' : natinf, ni_min d d' = ni_min d' d
  simple induction d.d:natinf
forall d' : natinf, ni_min infty d' = ni_min d' infty
d:natinf
forall (n : nat) (d' : natinf),
ni_min (ni n) d' = ni_min d' (ni n) simple induction d'; trivial.d:natinf
forall (n : nat) (d' : natinf),
ni_min (ni n) d' = ni_min d' (ni n)
  simple induction d'; trivial.d:natinf
n:nat
d':natinf
forall n0 : nat,
ni_min (ni n) (ni n0) = ni_min (ni n0) (ni n) elim n.d:natinf
n:nat
d':natinf
forall n0 : nat,
ni_min (ni 0) (ni n0) = ni_min (ni n0) (ni 0)
d:natinf
n:nat
d':natinf
forall n0 : nat,
(forall n1 : nat,
 ni_min (ni n0) (ni n1) = ni_min (ni n1) (ni n0)) ->
forall n1 : nat,
ni_min (ni (S n0)) (ni n1) =
ni_min (ni n1) (ni (S n0)) simple induction n0; trivial.d:natinf
n:nat
d':natinf
forall n0 : nat,
(forall n1 : nat,
 ni_min (ni n0) (ni n1) = ni_min (ni n1) (ni n0)) ->
forall n1 : nat,
ni_min (ni (S n0)) (ni n1) =
ni_min (ni n1) (ni (S n0))
  intros.d:natinf
n:nat
d':natinf
n0:nat
H:forall n2 : nat,
ni_min (ni n0) (ni n2) = ni_min (ni n2) (ni n0)
n1:nat
ni_min (ni (S n0)) (ni n1) =
ni_min (ni n1) (ni (S n0)) elim n1; trivial.d:natinf
n:nat
d':natinf
n0:nat
H:forall n2 : nat,
ni_min (ni n0) (ni n2) = ni_min (ni n2) (ni n0)
n1:nat
forall n2 : nat,
ni_min (ni (S n0)) (ni n2) =
ni_min (ni n2) (ni (S n0)) ->
ni_min (ni (S n0)) (ni (S n2)) =
ni_min (ni (S n2)) (ni (S n0)) intros.d:natinf
n:nat
d':natinf
n0:nat
H:forall n3 : nat,
ni_min (ni n0) (ni n3) = ni_min (ni n3) (ni n0)
n1, n2:nat
H0:ni_min (ni (S n0)) (ni n2) =
ni_min (ni n2) (ni (S n0))
ni_min (ni (S n0)) (ni (S n2)) =
ni_min (ni (S n2)) (ni (S n0)) unfold ni_min in H.d:natinf
n:nat
d':natinf
n0:nat
H:forall n3 : nat,
ni (Nat.min n0 n3) = ni (Nat.min n3 n0)
n1, n2:nat
H0:ni_min (ni (S n0)) (ni n2) =
ni_min (ni n2) (ni (S n0))
ni_min (ni (S n0)) (ni (S n2)) =
ni_min (ni (S n2)) (ni (S n0))
  enough (min n0 n2 = min n2 n0) by (unfold ni_min; simpl; rewrite H1; reflexivity).d:natinf
n:nat
d':natinf
n0:nat
H:forall n3 : nat,
ni (Nat.min n0 n3) = ni (Nat.min n3 n0)
n1, n2:nat
H0:ni_min (ni (S n0)) (ni n2) =
ni_min (ni n2) (ni (S n0))
Nat.min n0 n2 = Nat.min n2 n0
  enough (ni (min n0 n2) = ni (min n2 n0)) by (inversion H1; trivial).d:natinf
n:nat
d':natinf
n0:nat
H:forall n3 : nat,
ni (Nat.min n0 n3) = ni (Nat.min n3 n0)
n1, n2:nat
H0:ni_min (ni (S n0)) (ni n2) =
ni_min (ni n2) (ni (S n0))
ni (Nat.min n0 n2) = ni (Nat.min n2 n0)
  exact (H n2).
Qed.

Lemma ni_min_assoc :
 forall d d' d'':natinf, ni_min (ni_min d d') d'' = ni_min d (ni_min d' d'').forall d d' d'' : natinf,
ni_min (ni_min d d') d'' = ni_min d (ni_min d' d'')
Proof.forall d d' d'' : natinf,
ni_min (ni_min d d') d'' = ni_min d (ni_min d' d'')
  simple induction d; trivial.d:natinf
forall (n : nat) (d' d'' : natinf),
ni_min (ni_min (ni n) d') d'' =
ni_min (ni n) (ni_min d' d'') simple induction d'; trivial.d:natinf
n:nat
d':natinf
forall (n0 : nat) (d'' : natinf),
ni_min (ni_min (ni n) (ni n0)) d'' =
ni_min (ni n) (ni_min (ni n0) d'')
  simple induction d''; trivial.d:natinf
n:nat
d':natinf
n0:nat
d'':natinf
forall n1 : nat,
ni_min (ni_min (ni n) (ni n0)) (ni n1) =
ni_min (ni n) (ni_min (ni n0) (ni n1))
  unfold ni_min.d:natinf
n:nat
d':natinf
n0:nat
d'':natinf
forall n1 : nat,
ni (Nat.min (Nat.min n n0) n1) =
ni (Nat.min n (Nat.min n0 n1)) intro.d:natinf
n:nat
d':natinf
n0:nat
d'':natinf
n1:nat
ni (Nat.min (Nat.min n n0) n1) =
ni (Nat.min n (Nat.min n0 n1)) 
  enough (min (min n n0) n1 = min n (min n0 n1)) by (rewrite H; reflexivity).d:natinf
n:nat
d':natinf
n0:nat
d'':natinf
n1:nat
Nat.min (Nat.min n n0) n1 = Nat.min n (Nat.min n0 n1)
  induction n in n0, n1 |- *; trivial.d:natinf
n:nat
d':natinf
n0:nat
d'':natinf
n1:nat
IHn:forall n2 n3 : nat, Nat.min (Nat.min n n2) n3 = Nat.min n (Nat.min n2 n3)
Nat.min (Nat.min (S n) n0) n1 =
Nat.min (S n) (Nat.min n0 n1)
  destruct n0; trivial.d:natinf
n:nat
d':natinf
n0:nat
d'':natinf
n1:nat
IHn:forall n2 n3 : nat, Nat.min (Nat.min n n2) n3 = Nat.min n (Nat.min n2 n3)
Nat.min (Nat.min (S n) (S n0)) n1 =
Nat.min (S n) (Nat.min (S n0) n1) destruct n1; trivial.d:natinf
n:nat
d':natinf
n0:nat
d'':natinf
n1:nat
IHn:forall n2 n3 : nat, Nat.min (Nat.min n n2) n3 = Nat.min n (Nat.min n2 n3)
Nat.min (Nat.min (S n) (S n0)) (S n1) =
Nat.min (S n) (Nat.min (S n0) (S n1))
  intros.d:natinf
n:nat
d':natinf
n0:nat
d'':natinf
n1:nat
IHn:forall n2 n3 : nat, Nat.min (Nat.min n n2) n3 = Nat.min n (Nat.min n2 n3)
Nat.min (Nat.min (S n) (S n0)) (S n1) =
Nat.min (S n) (Nat.min (S n0) (S n1)) simpl.d:natinf
n:nat
d':natinf
n0:nat
d'':natinf
n1:nat
IHn:forall n2 n3 : nat, Nat.min (Nat.min n n2) n3 = Nat.min n (Nat.min n2 n3)
S (Nat.min (Nat.min n n0) n1) =
S (Nat.min n (Nat.min n0 n1)) auto.
Qed.

Lemma ni_min_O_l : forall d:natinf, ni_min (ni 0) d = ni 0.forall d : natinf, ni_min (ni 0) d = ni 0
Proof.forall d : natinf, ni_min (ni 0) d = ni 0
  simple induction d; trivial.
Qed.

Lemma ni_min_O_r : forall d:natinf, ni_min d (ni 0) = ni 0.forall d : natinf, ni_min d (ni 0) = ni 0
Proof.forall d : natinf, ni_min d (ni 0) = ni 0
  intros.d:natinf
ni_min d (ni 0) = ni 0 rewrite ni_min_comm.d:natinf
ni_min (ni 0) d = ni 0 apply ni_min_O_l.
Qed.

Lemma ni_min_inf_l : forall d:natinf, ni_min infty d = d.forall d : natinf, ni_min infty d = d
Proof.forall d : natinf, ni_min infty d = d
  trivial.
Qed.

Lemma ni_min_inf_r : forall d:natinf, ni_min d infty = d.forall d : natinf, ni_min d infty = d
Proof.forall d : natinf, ni_min d infty = d
  simple induction d; trivial.
Qed.

Definition ni_le (d d':natinf) := ni_min d d' = d.

Lemma ni_le_refl : forall d:natinf, ni_le d d.forall d : natinf, ni_le d d
Proof.forall d : natinf, ni_le d d
  exact ni_min_idemp.
Qed.

Lemma ni_le_antisym : forall d d':natinf, ni_le d d' -> ni_le d' d -> d = d'.forall d d' : natinf,
ni_le d d' -> ni_le d' d -> d = d'
Proof.forall d d' : natinf,
ni_le d d' -> ni_le d' d -> d = d'
  unfold ni_le.forall d d' : natinf,
ni_min d d' = d -> ni_min d' d = d' -> d = d' intros d d'.d, d':natinf
ni_min d d' = d -> ni_min d' d = d' -> d = d' rewrite ni_min_comm.d, d':natinf
ni_min d' d = d -> ni_min d' d = d' -> d = d' intro H.d, d':natinf
H:ni_min d' d = d
ni_min d' d = d' -> d = d' rewrite H.d, d':natinf
H:ni_min d' d = d
d = d' -> d = d' trivial.
Qed.

Lemma ni_le_trans :
 forall d d' d'':natinf, ni_le d d' -> ni_le d' d'' -> ni_le d d''.forall d d' d'' : natinf,
ni_le d d' -> ni_le d' d'' -> ni_le d d''
Proof.forall d d' d'' : natinf,
ni_le d d' -> ni_le d' d'' -> ni_le d d''
  unfold ni_le.forall d d' d'' : natinf,
ni_min d d' = d ->
ni_min d' d'' = d' -> ni_min d d'' = d intros.d, d', d'':natinf
H:ni_min d d' = d
H0:ni_min d' d'' = d'
ni_min d d'' = d rewrite <- H.d, d', d'':natinf
H:ni_min d d' = d
H0:ni_min d' d'' = d'
ni_min (ni_min d d') d'' = ni_min d d' rewrite ni_min_assoc.d, d', d'':natinf
H:ni_min d d' = d
H0:ni_min d' d'' = d'
ni_min d (ni_min d' d'') = ni_min d d' rewrite H0.d, d', d'':natinf
H:ni_min d d' = d
H0:ni_min d' d'' = d'
ni_min d d' = ni_min d d' reflexivity.
Qed.

Lemma ni_le_min_1 : forall d d':natinf, ni_le (ni_min d d') d.forall d d' : natinf, ni_le (ni_min d d') d
Proof.forall d d' : natinf, ni_le (ni_min d d') d
  unfold ni_le.forall d d' : natinf,
ni_min (ni_min d d') d = ni_min d d' intros.d, d':natinf
ni_min (ni_min d d') d = ni_min d d' rewrite (ni_min_comm d d').d, d':natinf
ni_min (ni_min d' d) d = ni_min d' d rewrite ni_min_assoc.d, d':natinf
ni_min d' (ni_min d d) = ni_min d' d
  rewrite ni_min_idemp.d, d':natinf
ni_min d' d = ni_min d' d reflexivity.
Qed.

Lemma ni_le_min_2 : forall d d':natinf, ni_le (ni_min d d') d'.forall d d' : natinf, ni_le (ni_min d d') d'
Proof.forall d d' : natinf, ni_le (ni_min d d') d'
  unfold ni_le.forall d d' : natinf,
ni_min (ni_min d d') d' = ni_min d d' intros.d, d':natinf
ni_min (ni_min d d') d' = ni_min d d' rewrite ni_min_assoc.d, d':natinf
ni_min d (ni_min d' d') = ni_min d d' rewrite ni_min_idemp.d, d':natinf
ni_min d d' = ni_min d d' reflexivity.
Qed.

Lemma ni_min_case : forall d d':natinf, ni_min d d' = d \/ ni_min d d' = d'.forall d d' : natinf,
ni_min d d' = d \/ ni_min d d' = d'
Proof.forall d d' : natinf,
ni_min d d' = d \/ ni_min d d' = d'
  destruct d.forall d' : natinf,
ni_min infty d' = infty \/ ni_min infty d' = d'
n:nat
forall d' : natinf,
ni_min (ni n) d' = ni n \/ ni_min (ni n) d' = d' right.d':natinf
ni_min infty d' = d'
n:nat
forall d' : natinf,
ni_min (ni n) d' = ni n \/ ni_min (ni n) d' = d' exact (ni_min_inf_l d').n:nat
forall d' : natinf,
ni_min (ni n) d' = ni n \/ ni_min (ni n) d' = d'
  destruct d'.n:nat
ni_min (ni n) infty = ni n \/
ni_min (ni n) infty = infty
n, n0:nat
ni_min (ni n) (ni n0) = ni n \/
ni_min (ni n) (ni n0) = ni n0 left.n:nat
ni_min (ni n) infty = ni n
n, n0:nat
ni_min (ni n) (ni n0) = ni n \/
ni_min (ni n) (ni n0) = ni n0 exact (ni_min_inf_r (ni n)).n, n0:nat
ni_min (ni n) (ni n0) = ni n \/
ni_min (ni n) (ni n0) = ni n0
  unfold ni_min.n, n0:nat
ni (Nat.min n n0) = ni n \/ ni (Nat.min n n0) = ni n0
  enough (min n n0 = n \/ min n n0 = n0) as [-> | ->].n, n0:nat
ni n = ni n \/ ni n = ni n0
n, n0:nat
ni n0 = ni n \/ ni n0 = ni n0
n, n0:nat
Nat.min n n0 = n \/ Nat.min n n0 = n0
  left.n, n0:nat
ni n = ni n
n, n0:nat
ni n0 = ni n \/ ni n0 = ni n0
n, n0:nat
Nat.min n n0 = n \/ Nat.min n n0 = n0 reflexivity.n, n0:nat
ni n0 = ni n \/ ni n0 = ni n0
n, n0:nat
Nat.min n n0 = n \/ Nat.min n n0 = n0
  right.n, n0:nat
ni n0 = ni n0
n, n0:nat
Nat.min n n0 = n \/ Nat.min n n0 = n0 reflexivity.n, n0:nat
Nat.min n n0 = n \/ Nat.min n n0 = n0
  destruct (Nat.min_dec n n0); [left|right]; assumption.
Qed.

Lemma ni_le_total : forall d d':natinf, ni_le d d' \/ ni_le d' d.forall d d' : natinf, ni_le d d' \/ ni_le d' d
Proof.forall d d' : natinf, ni_le d d' \/ ni_le d' d
  unfold ni_le.forall d d' : natinf,
ni_min d d' = d \/ ni_min d' d = d' intros.d, d':natinf
ni_min d d' = d \/ ni_min d' d = d' rewrite (ni_min_comm d' d).d, d':natinf
ni_min d d' = d \/ ni_min d d' = d' apply ni_min_case.
Qed.

Lemma ni_le_min_induc :
 forall d d' dm:natinf,
   ni_le dm d ->
   ni_le dm d' ->
   (forall d'':natinf, ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm) ->
   ni_min d d' = dm.forall d d' dm : natinf,
ni_le dm d ->
ni_le dm d' ->
(forall d'' : natinf,
 ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm) ->
ni_min d d' = dm
Proof.forall d d' dm : natinf,
ni_le dm d ->
ni_le dm d' ->
(forall d'' : natinf,
 ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm) ->
ni_min d d' = dm
  intros.d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
ni_min d d' = dm case (ni_min_case d d').d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
ni_min d d' = d -> ni_min d d' = dm
d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
ni_min d d' = d' -> ni_min d d' = dm intro.d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d
ni_min d d' = dm
d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
ni_min d d' = d' -> ni_min d d' = dm rewrite H2.d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d
d = dm
d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
ni_min d d' = d' -> ni_min d d' = dm
  apply ni_le_antisym.d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d
ni_le d dm
d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d
ni_le dm d
d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
ni_min d d' = d' -> ni_min d d' = dm apply H1.d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d
ni_le d d
d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d
ni_le d d'
d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d
ni_le dm d
d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
ni_min d d' = d' -> ni_min d d' = dm apply ni_le_refl.d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d
ni_le d d'
d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d
ni_le dm d
d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
ni_min d d' = d' -> ni_min d d' = dm
  exact H2.d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d
ni_le dm d
d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
ni_min d d' = d' -> ni_min d d' = dm
  exact H.d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
ni_min d d' = d' -> ni_min d d' = dm
  intro.d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d'
ni_min d d' = dm rewrite H2.d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d'
d' = dm apply ni_le_antisym.d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d'
ni_le d' dm
d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d'
ni_le dm d' apply H1.d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d'
ni_le d' d
d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d'
ni_le d' d'
d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d'
ni_le dm d' unfold ni_le.d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d'
ni_min d' d = d'
d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d'
ni_le d' d'
d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d'
ni_le dm d' rewrite ni_min_comm.d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d'
ni_min d d' = d'
d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d'
ni_le d' d'
d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d'
ni_le dm d' exact H2.d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d'
ni_le d' d'
d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d'
ni_le dm d'
  apply ni_le_refl.d, d', dm:natinf
H:ni_le dm d
H0:ni_le dm d'
H1:forall d'' : natinf,
ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm
H2:ni_min d d' = d'
ni_le dm d'
  exact H0.
Qed.

Lemma le_ni_le : forall m n:nat, m <= n -> ni_le (ni m) (ni n).forall m n : nat, m <= n -> ni_le (ni m) (ni n)
Proof.forall m n : nat, m <= n -> ni_le (ni m) (ni n)
  intros * H.m, n:nat
H:m <= n
ni_le (ni m) (ni n) unfold ni_le, ni_min.m, n:nat
H:m <= n
ni (Nat.min m n) = ni m rewrite (Peano.min_l m n H).m, n:nat
H:m <= n
ni m = ni m reflexivity.
Qed.

Lemma ni_le_le : forall m n:nat, ni_le (ni m) (ni n) -> m <= n.forall m n : nat, ni_le (ni m) (ni n) -> m <= n
Proof.forall m n : nat, ni_le (ni m) (ni n) -> m <= n
  unfold ni_le.forall m n : nat,
ni_min (ni m) (ni n) = ni m -> m <= n unfold ni_min.forall m n : nat, ni (Nat.min m n) = ni m -> m <= n intros.m, n:nat
H:ni (Nat.min m n) = ni m
m <= n inversion H.m, n:nat
H:ni (Nat.min m n) = ni m
H1:Nat.min m n = m
Nat.min m n <= n apply le_min_r.
Qed.

Lemma Nplength_lb :
 forall (a:N) (n:nat),
   (forall k:nat, k < n -> N.testbit_nat a k = false) -> ni_le (ni n) (Nplength a).forall (a : N) (n : nat),
(forall k : nat, k < n -> N.testbit_nat a k = false) ->
ni_le (ni n) (Nplength a)
Proof.forall (a : N) (n : nat),
(forall k : nat, k < n -> N.testbit_nat a k = false) ->
ni_le (ni n) (Nplength a)
  simple induction a.a:N
forall n : nat,
(forall k : nat, k < n -> N.testbit_nat 0 k = false) ->
ni_le (ni n) (Nplength 0)
a:N
forall (p : positive) (n : nat),
(forall k : nat,
 k < n -> N.testbit_nat (N.pos p) k = false) ->
ni_le (ni n) (Nplength (N.pos p)) intros.a:N
n:nat
H:forall k : nat, k < n -> N.testbit_nat 0 k = false
ni_le (ni n) (Nplength 0)
a:N
forall (p : positive) (n : nat),
(forall k : nat,
 k < n -> N.testbit_nat (N.pos p) k = false) ->
ni_le (ni n) (Nplength (N.pos p)) exact (ni_min_inf_r (ni n)).a:N
forall (p : positive) (n : nat),
(forall k : nat,
 k < n -> N.testbit_nat (N.pos p) k = false) ->
ni_le (ni n) (Nplength (N.pos p))
  intros.a:N
p:positive
n:nat
H:forall k : nat,
k < n -> N.testbit_nat (N.pos p) k = false
ni_le (ni n) (Nplength (N.pos p)) unfold Nplength.a:N
p:positive
n:nat
H:forall k : nat,
k < n -> N.testbit_nat (N.pos p) k = false
ni_le (ni n) (ni (Pplength p)) apply le_ni_le.a:N
p:positive
n:nat
H:forall k : nat,
k < n -> N.testbit_nat (N.pos p) k = false
n <= Pplength p case (le_or_lt n (Pplength p)).a:N
p:positive
n:nat
H:forall k : nat,
k < n -> N.testbit_nat (N.pos p) k = false
n <= Pplength p -> n <= Pplength p
a:N
p:positive
n:nat
H:forall k : nat,
k < n -> N.testbit_nat (N.pos p) k = false
Pplength p < n -> n <= Pplength p trivial.a:N
p:positive
n:nat
H:forall k : nat,
k < n -> N.testbit_nat (N.pos p) k = false
Pplength p < n -> n <= Pplength p
  intro.a:N
p:positive
n:nat
H:forall k : nat,
k < n -> N.testbit_nat (N.pos p) k = false
H0:Pplength p < n
n <= Pplength p absurd (N.testbit_nat (Npos p) (Pplength p) = false).a:N
p:positive
n:nat
H:forall k : nat,
k < n -> N.testbit_nat (N.pos p) k = false
H0:Pplength p < n
N.testbit_nat (N.pos p) (Pplength p) <> false
a:N
p:positive
n:nat
H:forall k : nat,
k < n -> N.testbit_nat (N.pos p) k = false
H0:Pplength p < n
N.testbit_nat (N.pos p) (Pplength p) = false
  rewrite
   (Nplength_one (Npos p) (Pplength p)
      (eq_refl (Nplength (Npos p)))).a:N
p:positive
n:nat
H:forall k : nat,
k < n -> N.testbit_nat (N.pos p) k = false
H0:Pplength p < n
true <> false
a:N
p:positive
n:nat
H:forall k : nat,
k < n -> N.testbit_nat (N.pos p) k = false
H0:Pplength p < n
N.testbit_nat (N.pos p) (Pplength p) = false
  discriminate.a:N
p:positive
n:nat
H:forall k : nat,
k < n -> N.testbit_nat (N.pos p) k = false
H0:Pplength p < n
N.testbit_nat (N.pos p) (Pplength p) = false
  apply H.a:N
p:positive
n:nat
H:forall k : nat,
k < n -> N.testbit_nat (N.pos p) k = false
H0:Pplength p < n
Pplength p < n exact H0.
Qed.

Lemma Nplength_ub :
 forall (a:N) (n:nat), N.testbit_nat a n = true -> ni_le (Nplength a) (ni n).forall (a : N) (n : nat),
N.testbit_nat a n = true -> ni_le (Nplength a) (ni n)
Proof.forall (a : N) (n : nat),
N.testbit_nat a n = true -> ni_le (Nplength a) (ni n)
  simple induction a.a:N
forall n : nat,
N.testbit_nat 0 n = true -> ni_le (Nplength 0) (ni n)
a:N
forall (p : positive) (n : nat),
N.testbit_nat (N.pos p) n = true ->
ni_le (Nplength (N.pos p)) (ni n) intros.a:N
n:nat
H:N.testbit_nat 0 n = true
ni_le (Nplength 0) (ni n)
a:N
forall (p : positive) (n : nat),
N.testbit_nat (N.pos p) n = true ->
ni_le (Nplength (N.pos p)) (ni n) discriminate H.a:N
forall (p : positive) (n : nat),
N.testbit_nat (N.pos p) n = true ->
ni_le (Nplength (N.pos p)) (ni n)
  intros.a:N
p:positive
n:nat
H:N.testbit_nat (N.pos p) n = true
ni_le (Nplength (N.pos p)) (ni n) unfold Nplength.a:N
p:positive
n:nat
H:N.testbit_nat (N.pos p) n = true
ni_le (ni (Pplength p)) (ni n) apply le_ni_le.a:N
p:positive
n:nat
H:N.testbit_nat (N.pos p) n = true
Pplength p <= n case (le_or_lt (Pplength p) n).a:N
p:positive
n:nat
H:N.testbit_nat (N.pos p) n = true
Pplength p <= n -> Pplength p <= n
a:N
p:positive
n:nat
H:N.testbit_nat (N.pos p) n = true
n < Pplength p -> Pplength p <= n trivial.a:N
p:positive
n:nat
H:N.testbit_nat (N.pos p) n = true
n < Pplength p -> Pplength p <= n
  intro.a:N
p:positive
n:nat
H:N.testbit_nat (N.pos p) n = true
H0:n < Pplength p
Pplength p <= n absurd (N.testbit_nat (Npos p) n = true).a:N
p:positive
n:nat
H:N.testbit_nat (N.pos p) n = true
H0:n < Pplength p
N.testbit_nat (N.pos p) n <> true
a:N
p:positive
n:nat
H:N.testbit_nat (N.pos p) n = true
H0:n < Pplength p
N.testbit_nat (N.pos p) n = true
  rewrite
   (Nplength_zeros (Npos p) (Pplength p)
      (eq_refl (Nplength (Npos p))) n H0).a:N
p:positive
n:nat
H:N.testbit_nat (N.pos p) n = true
H0:n < Pplength p
false <> true
a:N
p:positive
n:nat
H:N.testbit_nat (N.pos p) n = true
H0:n < Pplength p
N.testbit_nat (N.pos p) n = true
  discriminate.a:N
p:positive
n:nat
H:N.testbit_nat (N.pos p) n = true
H0:n < Pplength p
N.testbit_nat (N.pos p) n = true
  exact H.
Qed.

We define an ultrametric distance between N numbers: , where is the number of identical bits at the beginning of and (infinity if ). Instead of working with , we work with , namely Npdist:

Definition Npdist (a a':N) := Nplength (N.lxor a a').

d is a distance, so iff ; this means that iff :

Lemma Npdist_eq_1 : forall a:N, Npdist a a = infty.forall a : N, Npdist a a = infty
Proof.forall a : N, Npdist a a = infty
  intros.a:N
Npdist a a = infty unfold Npdist.a:N
Nplength (N.lxor a a) = infty rewrite N.lxor_nilpotent.a:N
Nplength 0 = infty reflexivity.
Qed.

Lemma Npdist_eq_2 : forall a a':N, Npdist a a' = infty -> a = a'.forall a a' : N, Npdist a a' = infty -> a = a'
Proof.forall a a' : N, Npdist a a' = infty -> a = a'
  intros.a, a':N
H:Npdist a a' = infty
a = a' apply N.lxor_eq.a, a':N
H:Npdist a a' = infty
N.lxor a a' = 0%N apply Nplength_infty.a, a':N
H:Npdist a a' = infty
Nplength (N.lxor a a') = infty exact H.
Qed.

is a distance, so :

Lemma Npdist_comm : forall a a':N, Npdist a a' = Npdist a' a.forall a a' : N, Npdist a a' = Npdist a' a
Proof.forall a a' : N, Npdist a a' = Npdist a' a
  unfold Npdist.forall a a' : N,
Nplength (N.lxor a a') = Nplength (N.lxor a' a) intros.a, a':N
Nplength (N.lxor a a') = Nplength (N.lxor a' a) rewrite N.lxor_comm.a, a':N
Nplength (N.lxor a' a) = Nplength (N.lxor a' a) reflexivity.
Qed.

is an ultrametric distance, that is, not only , but in fact . This means that (lemma Npdist_ultra below). This follows from the fact that is an ultrametric norm, i.e. that , or equivalently that , i.e. that min (lemma Nplength_ultra).

Lemma Nplength_ultra_1 :
 forall a a':N,
   ni_le (Nplength a) (Nplength a') ->
   ni_le (Nplength a) (Nplength (N.lxor a a')).forall a a' : N,
ni_le (Nplength a) (Nplength a') ->
ni_le (Nplength a) (Nplength (N.lxor a a'))
Proof.forall a a' : N,
ni_le (Nplength a) (Nplength a') ->
ni_le (Nplength a) (Nplength (N.lxor a a'))
  simple induction a.a:N
forall a' : N,
ni_le (Nplength 0) (Nplength a') ->
ni_le (Nplength 0) (Nplength (N.lxor 0 a'))
a:N
forall (p : positive) (a' : N),
ni_le (Nplength (N.pos p)) (Nplength a') ->
ni_le (Nplength (N.pos p))
  (Nplength (N.lxor (N.pos p) a')) intros.a, a':N
H:ni_le (Nplength 0) (Nplength a')
ni_le (Nplength 0) (Nplength (N.lxor 0 a'))
a:N
forall (p : positive) (a' : N),
ni_le (Nplength (N.pos p)) (Nplength a') ->
ni_le (Nplength (N.pos p))
  (Nplength (N.lxor (N.pos p) a')) unfold ni_le in H.a, a':N
H:ni_min (Nplength 0) (Nplength a') = Nplength 0
ni_le (Nplength 0) (Nplength (N.lxor 0 a'))
a:N
forall (p : positive) (a' : N),
ni_le (Nplength (N.pos p)) (Nplength a') ->
ni_le (Nplength (N.pos p))
  (Nplength (N.lxor (N.pos p) a')) unfold Nplength at 1 3 in H.a, a':N
H:ni_min infty (Nplength a') = infty
ni_le (Nplength 0) (Nplength (N.lxor 0 a'))
a:N
forall (p : positive) (a' : N),
ni_le (Nplength (N.pos p)) (Nplength a') ->
ni_le (Nplength (N.pos p))
  (Nplength (N.lxor (N.pos p) a'))
  rewrite (ni_min_inf_l (Nplength a')) in H.a, a':N
H:Nplength a' = infty
ni_le (Nplength 0) (Nplength (N.lxor 0 a'))
a:N
forall (p : positive) (a' : N),
ni_le (Nplength (N.pos p)) (Nplength a') ->
ni_le (Nplength (N.pos p))
  (Nplength (N.lxor (N.pos p) a'))
  rewrite (Nplength_infty a' H).a, a':N
H:Nplength a' = infty
ni_le (Nplength 0) (Nplength (N.lxor 0 0))
a:N
forall (p : positive) (a' : N),
ni_le (Nplength (N.pos p)) (Nplength a') ->
ni_le (Nplength (N.pos p))
  (Nplength (N.lxor (N.pos p) a')) simpl.a, a':N
H:Nplength a' = infty
ni_le infty infty
a:N
forall (p : positive) (a' : N),
ni_le (Nplength (N.pos p)) (Nplength a') ->
ni_le (Nplength (N.pos p))
  (Nplength (N.lxor (N.pos p) a')) apply ni_le_refl.a:N
forall (p : positive) (a' : N),
ni_le (Nplength (N.pos p)) (Nplength a') ->
ni_le (Nplength (N.pos p))
  (Nplength (N.lxor (N.pos p) a'))
  intros.a:N
p:positive
a':N
H:ni_le (Nplength (N.pos p)) (Nplength a')
ni_le (Nplength (N.pos p))
  (Nplength (N.lxor (N.pos p) a')) unfold Nplength at 1.a:N
p:positive
a':N
H:ni_le (Nplength (N.pos p)) (Nplength a')
ni_le (ni (Pplength p))
  (Nplength (N.lxor (N.pos p) a')) apply Nplength_lb.a:N
p:positive
a':N
H:ni_le (Nplength (N.pos p)) (Nplength a')
forall k : nat,
k < Pplength p ->
N.testbit_nat (N.lxor (N.pos p) a') k = false intros.a:N
p:positive
a':N
H:ni_le (Nplength (N.pos p)) (Nplength a')
k:nat
H0:k < Pplength p
N.testbit_nat (N.lxor (N.pos p) a') k = false
  enough (forall a'':N, N.lxor (Npos p) a' = a'' -> N.testbit_nat a'' k = false).a:N
p:positive
a':N
H:ni_le (Nplength (N.pos p)) (Nplength a')
k:nat
H0:k < Pplength p
H1:forall a'' : N,
N.lxor (N.pos p) a' = a'' ->
N.testbit_nat a'' k = false
N.testbit_nat (N.lxor (N.pos p) a') k = false
a:N
p:positive
a':N
H:ni_le (Nplength (N.pos p)) (Nplength a')
k:nat
H0:k < Pplength p
forall a'' : N,
N.lxor (N.pos p) a' = a'' ->
N.testbit_nat a'' k = false
  {a:N
p:positive
a':N
H:ni_le (Nplength (N.pos p)) (Nplength a')
k:nat
H0:k < Pplength p
H1:forall a'' : N,
N.lxor (N.pos p) a' = a'' ->
N.testbit_nat a'' k = false
N.testbit_nat (N.lxor (N.pos p) a') k = false apply H1.a:N
p:positive
a':N
H:ni_le (Nplength (N.pos p)) (Nplength a')
k:nat
H0:k < Pplength p
H1:forall a'' : N,
N.lxor (N.pos p) a' = a'' ->
N.testbit_nat a'' k = false
N.lxor (N.pos p) a' = N.lxor (N.pos p) a' reflexivity. }a:N
p:positive
a':N
H:ni_le (Nplength (N.pos p)) (Nplength a')
k:nat
H0:k < Pplength p
forall a'' : N,
N.lxor (N.pos p) a' = a'' ->
N.testbit_nat a'' k = false
  intro a''.a:N
p:positive
a':N
H:ni_le (Nplength (N.pos p)) (Nplength a')
k:nat
H0:k < Pplength p
a'':N
N.lxor (N.pos p) a' = a'' ->
N.testbit_nat a'' k = false case a''.a:N
p:positive
a':N
H:ni_le (Nplength (N.pos p)) (Nplength a')
k:nat
H0:k < Pplength p
a'':N
N.lxor (N.pos p) a' = 0%N -> N.testbit_nat 0 k = false
a:N
p:positive
a':N
H:ni_le (Nplength (N.pos p)) (Nplength a')
k:nat
H0:k < Pplength p
a'':N
forall p0 : positive,
N.lxor (N.pos p) a' = N.pos p0 ->
N.testbit_nat (N.pos p0) k = false intro.a:N
p:positive
a':N
H:ni_le (Nplength (N.pos p)) (Nplength a')
k:nat
H0:k < Pplength p
a'':N
H1:N.lxor (N.pos p) a' = 0%N
N.testbit_nat 0 k = false
a:N
p:positive
a':N
H:ni_le (Nplength (N.pos p)) (Nplength a')
k:nat
H0:k < Pplength p
a'':N
forall p0 : positive,
N.lxor (N.pos p) a' = N.pos p0 ->
N.testbit_nat (N.pos p0) k = false reflexivity.a:N
p:positive
a':N
H:ni_le (Nplength (N.pos p)) (Nplength a')
k:nat
H0:k < Pplength p
a'':N
forall p0 : positive,
N.lxor (N.pos p) a' = N.pos p0 ->
N.testbit_nat (N.pos p0) k = false
  intros.a:N
p:positive
a':N
H:ni_le (Nplength (N.pos p)) (Nplength a')
k:nat
H0:k < Pplength p
a'':N
p0:positive
H1:N.lxor (N.pos p) a' = N.pos p0
N.testbit_nat (N.pos p0) k = false rewrite <- H1.a:N
p:positive
a':N
H:ni_le (Nplength (N.pos p)) (Nplength a')
k:nat
H0:k < Pplength p
a'':N
p0:positive
H1:N.lxor (N.pos p) a' = N.pos p0
N.testbit_nat (N.lxor (N.pos p) a') k = false rewrite (Nxor_semantics (Npos p) a' k).a:N
p:positive
a':N
H:ni_le (Nplength (N.pos p)) (Nplength a')
k:nat
H0:k < Pplength p
a'':N
p0:positive
H1:N.lxor (N.pos p) a' = N.pos p0
xorb (N.testbit_nat (N.pos p) k) (N.testbit_nat a' k) =
false
  rewrite
   (Nplength_zeros (Npos p) (Pplength p)
      (eq_refl (Nplength (Npos p))) k H0).a:N
p:positive
a':N
H:ni_le (Nplength (N.pos p)) (Nplength a')
k:nat
H0:k < Pplength p
a'':N
p0:positive
H1:N.lxor (N.pos p) a' = N.pos p0
xorb false (N.testbit_nat a' k) = false
  destruct a'.a:N
p:positive
H:ni_le (Nplength (N.pos p)) (Nplength 0)
k:nat
H0:k < Pplength p
a'':N
p0:positive
H1:N.lxor (N.pos p) 0 = N.pos p0
xorb false (N.testbit_nat 0 k) = false
a:N
p, p1:positive
H:ni_le (Nplength (N.pos p)) (Nplength (N.pos p1))
k:nat
H0:k < Pplength p
a'':N
p0:positive
H1:N.lxor (N.pos p) (N.pos p1) = N.pos p0
xorb false (N.testbit_nat (N.pos p1) k) = false trivial.a:N
p, p1:positive
H:ni_le (Nplength (N.pos p)) (Nplength (N.pos p1))
k:nat
H0:k < Pplength p
a'':N
p0:positive
H1:N.lxor (N.pos p) (N.pos p1) = N.pos p0
xorb false (N.testbit_nat (N.pos p1) k) = false
  enough (N.testbit_nat (Npos p1) k = false) as -> by reflexivity.a:N
p, p1:positive
H:ni_le (Nplength (N.pos p)) (Nplength (N.pos p1))
k:nat
H0:k < Pplength p
a'':N
p0:positive
H1:N.lxor (N.pos p) (N.pos p1) = N.pos p0
N.testbit_nat (N.pos p1) k = false
  apply Nplength_zeros with (n := Pplength p1).a:N
p, p1:positive
H:ni_le (Nplength (N.pos p)) (Nplength (N.pos p1))
k:nat
H0:k < Pplength p
a'':N
p0:positive
H1:N.lxor (N.pos p) (N.pos p1) = N.pos p0
Nplength (N.pos p1) = ni (Pplength p1)
a:N
p, p1:positive
H:ni_le (Nplength (N.pos p)) (Nplength (N.pos p1))
k:nat
H0:k < Pplength p
a'':N
p0:positive
H1:N.lxor (N.pos p) (N.pos p1) = N.pos p0
k < Pplength p1 reflexivity.a:N
p, p1:positive
H:ni_le (Nplength (N.pos p)) (Nplength (N.pos p1))
k:nat
H0:k < Pplength p
a'':N
p0:positive
H1:N.lxor (N.pos p) (N.pos p1) = N.pos p0
k < Pplength p1
  apply (lt_le_trans k (Pplength p) (Pplength p1)).a:N
p, p1:positive
H:ni_le (Nplength (N.pos p)) (Nplength (N.pos p1))
k:nat
H0:k < Pplength p
a'':N
p0:positive
H1:N.lxor (N.pos p) (N.pos p1) = N.pos p0
k < Pplength p
a:N
p, p1:positive
H:ni_le (Nplength (N.pos p)) (Nplength (N.pos p1))
k:nat
H0:k < Pplength p
a'':N
p0:positive
H1:N.lxor (N.pos p) (N.pos p1) = N.pos p0
Pplength p <= Pplength p1 exact H0.a:N
p, p1:positive
H:ni_le (Nplength (N.pos p)) (Nplength (N.pos p1))
k:nat
H0:k < Pplength p
a'':N
p0:positive
H1:N.lxor (N.pos p) (N.pos p1) = N.pos p0
Pplength p <= Pplength p1
  apply ni_le_le.a:N
p, p1:positive
H:ni_le (Nplength (N.pos p)) (Nplength (N.pos p1))
k:nat
H0:k < Pplength p
a'':N
p0:positive
H1:N.lxor (N.pos p) (N.pos p1) = N.pos p0
ni_le (ni (Pplength p)) (ni (Pplength p1)) exact H.
Qed.

Lemma Nplength_ultra :
 forall a a':N,
   ni_le (ni_min (Nplength a) (Nplength a')) (Nplength (N.lxor a a')).forall a a' : N,
ni_le (ni_min (Nplength a) (Nplength a'))
  (Nplength (N.lxor a a'))
Proof.forall a a' : N,
ni_le (ni_min (Nplength a) (Nplength a'))
  (Nplength (N.lxor a a'))
  intros.a, a':N
ni_le (ni_min (Nplength a) (Nplength a'))
  (Nplength (N.lxor a a')) destruct (ni_le_total (Nplength a) (Nplength a')).a, a':N
H:ni_le (Nplength a) (Nplength a')
ni_le (ni_min (Nplength a) (Nplength a'))
  (Nplength (N.lxor a a'))
a, a':N
H:ni_le (Nplength a') (Nplength a)
ni_le (ni_min (Nplength a) (Nplength a'))
  (Nplength (N.lxor a a'))
  enough (ni_min (Nplength a) (Nplength a') = Nplength a) as -> by (apply Nplength_ultra_1; exact H).a, a':N
H:ni_le (Nplength a) (Nplength a')
ni_min (Nplength a) (Nplength a') = Nplength a
a, a':N
H:ni_le (Nplength a') (Nplength a)
ni_le (ni_min (Nplength a) (Nplength a'))
  (Nplength (N.lxor a a'))
  exact H.a, a':N
H:ni_le (Nplength a') (Nplength a)
ni_le (ni_min (Nplength a) (Nplength a'))
  (Nplength (N.lxor a a'))
  enough (ni_min (Nplength a) (Nplength a') = Nplength a') as -> by (rewrite N.lxor_comm; apply Nplength_ultra_1; exact H).a, a':N
H:ni_le (Nplength a') (Nplength a)
ni_min (Nplength a) (Nplength a') = Nplength a'
  rewrite ni_min_comm.a, a':N
H:ni_le (Nplength a') (Nplength a)
ni_min (Nplength a') (Nplength a) = Nplength a' exact H.
Qed.

Lemma Npdist_ultra :
 forall a a' a'':N,
   ni_le (ni_min (Npdist a a'') (Npdist a'' a')) (Npdist a a').forall a a' a'' : N,
ni_le (ni_min (Npdist a a'') (Npdist a'' a'))
  (Npdist a a')
Proof.forall a a' a'' : N,
ni_le (ni_min (Npdist a a'') (Npdist a'' a'))
  (Npdist a a')
  intros.a, a', a'':N
ni_le (ni_min (Npdist a a'') (Npdist a'' a'))
  (Npdist a a') unfold Npdist.a, a', a'':N
ni_le
  (ni_min (Nplength (N.lxor a a''))
     (Nplength (N.lxor a'' a')))
  (Nplength (N.lxor a a')) cut (N.lxor (N.lxor a a'') (N.lxor a'' a') = N.lxor a a').a, a', a'':N
N.lxor (N.lxor a a'') (N.lxor a'' a') = N.lxor a a' ->
ni_le
  (ni_min (Nplength (N.lxor a a''))
     (Nplength (N.lxor a'' a')))
  (Nplength (N.lxor a a'))
a, a', a'':N
N.lxor (N.lxor a a'') (N.lxor a'' a') = N.lxor a a'
  intro.a, a', a'':N
H:N.lxor (N.lxor a a'') (N.lxor a'' a') =
N.lxor a a'
ni_le
  (ni_min (Nplength (N.lxor a a''))
     (Nplength (N.lxor a'' a')))
  (Nplength (N.lxor a a'))
a, a', a'':N
N.lxor (N.lxor a a'') (N.lxor a'' a') = N.lxor a a' rewrite <- H.a, a', a'':N
H:N.lxor (N.lxor a a'') (N.lxor a'' a') =
N.lxor a a'
ni_le
  (ni_min (Nplength (N.lxor a a''))
     (Nplength (N.lxor a'' a')))
  (Nplength (N.lxor (N.lxor a a'') (N.lxor a'' a')))
a, a', a'':N
N.lxor (N.lxor a a'') (N.lxor a'' a') = N.lxor a a' apply Nplength_ultra.a, a', a'':N
N.lxor (N.lxor a a'') (N.lxor a'' a') = N.lxor a a'
  rewrite N.lxor_assoc.a, a', a'':N
N.lxor a (N.lxor a'' (N.lxor a'' a')) = N.lxor a a' rewrite <- (N.lxor_assoc a'' a'' a').a, a', a'':N
N.lxor a (N.lxor (N.lxor a'' a'') a') = N.lxor a a' rewrite N.lxor_nilpotent.a, a', a'':N
N.lxor a (N.lxor 0 a') = N.lxor a a'
  rewrite N.lxor_0_l.a, a', a'':N
N.lxor a a' = N.lxor a a' reflexivity.
Qed.