Speed up Byte

We could move another ~ 1s from Init.Byte to Strings.Byte by moving
`of_bits_to_bits` and `to_bits_of_bits`, but I figured it's probably not
worth it.

After    | File Name                            | Before   || Change    | % Change
----------------------------------------------------------------------------------
1m16.75s | Total                                | 1m21.45s || -0m04.70s | -5.77%
----------------------------------------------------------------------------------
0m08.95s | Strings/Byte                         | 0m12.41s || -0m03.46s | -27.88%
0m07.24s | Byte                                 | 0m08.76s || -0m01.51s | -17.35%
0m06.37s | plugins/setoid_ring/Ring_polynom     | 0m06.24s || +0m00.12s | +2.08%
0m03.14s | Numbers/Integer/Abstract/ZBits       | 0m03.20s || -0m00.06s | -1.87%
0m02.44s | ZArith/BinInt                        | 0m02.44s || +0m00.00s | +0.00%
0m02.24s | Numbers/Natural/Abstract/NBits       | 0m02.20s || +0m00.04s | +1.81%
0m01.97s | Lists/List                           | 0m01.93s || +0m00.04s | +2.07%
0m01.85s | Numbers/NatInt/NZLog                 | 0m01.82s || +0m00.03s | +1.64%
0m01.78s | PArith/BinPos                        | 0m01.78s || +0m00.00s | +0.00%
0m01.74s | plugins/setoid_ring/InitialRing      | 0m01.63s || +0m00.11s | +6.74%
0m01.73s | Strings/Ascii                        | 0m01.58s || +0m00.14s | +9.49%
0m01.39s | NArith/BinNat                        | 0m01.34s || +0m00.04s | +3.73%
0m01.32s | Numbers/NatInt/NZPow                 | 0m01.24s || +0m00.08s | +6.45%
0m01.22s | Numbers/NatInt/NZSqrt                | 0m01.15s || +0m00.07s | +6.08%
0m01.11s | Arith/PeanoNat                       | 0m01.16s || -0m00.04s | -4.31%
0m01.10s | Numbers/Integer/Abstract/ZDivTrunc   | 0m01.11s || -0m00.01s | -0.90%
0m01.02s | Specif                               | 0m01.04s || -0m00.02s | -1.92%
0m00.96s | Numbers/NatInt/NZMulOrder            | 0m00.84s || +0m00.12s | +14.28%
0m00.95s | Numbers/Integer/Abstract/ZDivFloor   | 0m00.97s || -0m00.02s | -2.06%
0m00.85s | plugins/setoid_ring/Ring_theory      | 0m00.86s || -0m00.01s | -1.16%
0m00.82s | Structures/GenericMinMax             | 0m00.85s || -0m00.03s | -3.52%
0m00.72s | Numbers/Integer/Abstract/ZLcm        | 0m00.82s || -0m00.09s | -12.19%
0m00.69s | Numbers/NatInt/NZParity              | 0m00.69s || +0m00.00s | +0.00%
0m00.68s | Numbers/NatInt/NZDiv                 | 0m00.71s || -0m00.02s | -4.22%
0m00.68s | Strings/String                       | 0m00.65s || +0m00.03s | +4.61%
0m00.64s | Numbers/Integer/Abstract/ZSgnAbs     | 0m00.64s || +0m00.00s | +0.00%
0m00.64s | ZArith/Zeven                         | 0m00.48s || +0m00.16s | +33.33%
0m00.63s | ZArith/Zorder                        | 0m00.61s || +0m00.02s | +3.27%
0m00.57s | Numbers/Integer/Abstract/ZMulOrder   | 0m00.67s || -0m00.10s | -14.92%
0m00.56s | Classes/Morphisms                    | 0m00.58s || -0m00.01s | -3.44%
0m00.55s | Numbers/NatInt/NZOrder               | 0m00.51s || +0m00.04s | +7.84%
0m00.48s | ZArith/BinIntDef                     | 0m00.48s || +0m00.00s | +0.00%
0m00.46s | Classes/CMorphisms                   | 0m00.48s || -0m00.01s | -4.16%
0m00.46s | Numbers/Integer/Abstract/ZGcd        | 0m00.46s || +0m00.00s | +0.00%
0m00.46s | Numbers/Natural/Abstract/NSub        | 0m00.48s || -0m00.01s | -4.16%
0m00.45s | Logic                                | 0m00.44s || +0m00.01s | +2.27%
0m00.45s | Numbers/Natural/Abstract/NGcd        | 0m00.48s || -0m00.02s | -6.24%
0m00.42s | Numbers/Natural/Abstract/NLcm        | 0m00.40s || +0m00.01s | +4.99%
0m00.42s | Structures/OrdersFacts               | 0m00.48s || -0m00.06s | -12.50%
0m00.41s | ZArith/Zbool                         | 0m00.38s || +0m00.02s | +7.89%
0m00.38s | Numbers/Integer/Abstract/ZPow        | 0m00.34s || +0m00.03s | +11.76%
0m00.36s | Bool/Bool                            | 0m00.36s || +0m00.00s | +0.00%
0m00.36s | Numbers/NatInt/NZGcd                 | 0m00.35s || +0m00.01s | +2.85%
0m00.36s | ZArith/ZArith_dec                    | 0m00.38s || -0m00.02s | -5.26%
0m00.34s | Numbers/Integer/Abstract/ZAdd        | 0m00.33s || +0m00.01s | +3.03%
0m00.34s | PArith/Pnat                          | 0m00.31s || +0m00.03s | +9.67%
0m00.32s | Numbers/Natural/Abstract/NOrder      | 0m00.32s || +0m00.00s | +0.00%
0m00.32s | PArith/BinPosDef                     | 0m00.31s || +0m00.01s | +3.22%
0m00.32s | ZArith/Zcompare                      | 0m00.28s || +0m00.03s | +14.28%
0m00.30s | Classes/RelationClasses              | 0m00.29s || +0m00.01s | +3.44%
0m00.30s | NArith/Nnat                          | 0m00.30s || +0m00.00s | +0.00%
0m00.29s | Numbers/Natural/Abstract/NAxioms     | 0m00.26s || +0m00.02s | +11.53%
0m00.28s | Numbers/Integer/Abstract/ZAddOrder   | 0m00.28s || +0m00.00s | +0.00%
0m00.28s | Structures/Orders                    | 0m00.30s || -0m00.01s | -6.66%
0m00.27s | Numbers/Integer/Abstract/ZAxioms     | 0m00.23s || +0m00.04s | +17.39%
0m00.27s | Numbers/NatInt/NZAxioms              | 0m00.26s || +0m00.01s | +3.84%
0m00.26s | Numbers/Integer/Abstract/ZMaxMin     | 0m00.25s || +0m00.01s | +4.00%
0m00.26s | Numbers/NatInt/NZAdd                 | 0m00.28s || -0m00.02s | -7.14%
0m00.26s | Numbers/Natural/Abstract/NMaxMin     | 0m00.24s || +0m00.02s | +8.33%
0m00.26s | Numbers/Natural/Abstract/NParity     | 0m00.31s || -0m00.04s | -16.12%
0m00.26s | plugins/setoid_ring/ArithRing        | 0m00.22s || +0m00.04s | +18.18%
0m00.26s | plugins/setoid_ring/Ring_tac         | 0m00.24s || +0m00.02s | +8.33%
0m00.25s | Logic/Decidable                      | 0m00.26s || -0m00.01s | -3.84%
0m00.25s | Structures/OrdersTac                 | 0m00.25s || +0m00.00s | +0.00%
0m00.24s | Classes/Equivalence                  | 0m00.25s || -0m00.01s | -4.00%
0m00.24s | Datatypes                            | 0m00.27s || -0m00.03s | -11.11%
0m00.24s | Numbers/NatInt/NZMul                 | 0m00.25s || -0m00.01s | -4.00%
0m00.24s | plugins/setoid_ring/Ring             | 0m00.20s || +0m00.03s | +19.99%
0m00.23s | Numbers/NatInt/NZAddOrder            | 0m00.33s || -0m00.10s | -30.30%
0m00.23s | Numbers/Natural/Abstract/NAdd        | 0m00.17s || +0m00.06s | +35.29%
0m00.22s | Arith/Compare_dec                    | 0m00.22s || +0m00.00s | +0.00%
0m00.22s | Classes/CRelationClasses             | 0m00.25s || -0m00.03s | -12.00%
0m00.22s | Logic/EqdepFacts                     | 0m00.19s || +0m00.03s | +15.78%
0m00.22s | NArith/BinNatDef                     | 0m00.25s || -0m00.03s | -12.00%
0m00.22s | plugins/setoid_ring/Ring_base        | 0m00.23s || -0m00.01s | -4.34%
0m00.21s | Arith/Arith                          | 0m00.19s || +0m00.01s | +10.52%
0m00.21s | Numbers/Natural/Abstract/NDiv        | 0m00.19s || +0m00.01s | +10.52%
0m00.20s | Numbers/Integer/Abstract/ZProperties | 0m00.23s || -0m00.03s | -13.04%
0m00.20s | Relations/Relation_Operators         | 0m00.17s || +0m00.03s | +17.64%
0m00.19s | Arith/Between                        | 0m00.22s || -0m00.03s | -13.63%
0m00.18s | Arith/Wf_nat                         | 0m00.24s || -0m00.06s | -25.00%
0m00.17s | Arith/Plus                           | 0m00.16s || +0m00.01s | +6.25%
0m00.17s | Nat                                  | 0m00.18s || -0m00.00s | -5.55%
0m00.17s | Numbers/Natural/Abstract/NProperties | 0m00.22s || -0m00.04s | -22.72%
0m00.17s | Relations/Relation_Definitions       | 0m00.08s || +0m00.09s | +112.50%
0m00.16s | Numbers/Integer/Abstract/ZLt         | 0m00.16s || +0m00.00s | +0.00%
0m00.16s | Numbers/Natural/Abstract/NBase       | 0m00.19s || -0m00.03s | -15.78%
0m00.16s | Numbers/Natural/Abstract/NPow        | 0m00.15s || +0m00.01s | +6.66%
0m00.15s | Classes/Morphisms_Prop               | 0m00.18s || -0m00.03s | -16.66%
0m00.14s | Arith/Mult                           | 0m00.12s || +0m00.02s | +16.66%
0m00.14s | Arith/Peano_dec                      | 0m00.16s || -0m00.01s | -12.49%
0m00.14s | Numbers/NatInt/NZBase                | 0m00.13s || +0m00.01s | +7.69%
0m00.14s | Numbers/Natural/Abstract/NMulOrder   | 0m00.13s || +0m00.01s | +7.69%
0m00.14s | Relations/Operators_Properties       | 0m00.13s || +0m00.01s | +7.69%
0m00.14s | plugins/setoid_ring/BinList          | 0m00.16s || -0m00.01s | -12.49%
0m00.13s | Arith/EqNat                          | 0m00.18s || -0m00.04s | -27.77%
0m00.13s | Structures/Equalities                | 0m00.17s || -0m00.04s | -23.52%
0m00.12s | Arith/Lt                             | 0m00.11s || +0m00.00s | +9.09%
0m00.12s | Arith/Minus                          | 0m00.13s || -0m00.01s | -7.69%
0m00.12s | Decimal                              | 0m00.16s || -0m00.04s | -25.00%
0m00.12s | Numbers/Integer/Abstract/ZBase       | 0m00.09s || +0m00.03s | +33.33%
0m00.12s | Numbers/Integer/Abstract/ZMul        | 0m00.12s || +0m00.00s | +0.00%
0m00.12s | Numbers/Integer/Abstract/ZParity     | 0m00.11s || +0m00.00s | +9.09%
0m00.12s | Numbers/Natural/Abstract/NAddOrder   | 0m00.12s || +0m00.00s | +0.00%
0m00.11s | Arith/Factorial                      | 0m00.11s || +0m00.00s | +0.00%
0m00.11s | Lists/ListTactics                    | 0m00.13s || -0m00.02s | -15.38%
0m00.11s | Logic/Eqdep_dec                      | 0m00.12s || -0m00.00s | -8.33%
0m00.11s | Numbers/Natural/Abstract/NLog        | 0m00.10s || +0m00.00s | +9.99%
0m00.11s | Peano                                | 0m00.10s || +0m00.00s | +9.99%
0m00.11s | Program/Basics                       | 0m00.07s || +0m00.03s | +57.14%
0m00.10s | Arith/Gt                             | 0m00.13s || -0m00.03s | -23.07%
0m00.10s | Bool/Sumbool                         | 0m00.10s || +0m00.00s | +0.00%
0m00.10s | Numbers/Natural/Abstract/NSqrt       | 0m00.12s || -0m00.01s | -16.66%
0m00.10s | Wf                                   | 0m00.11s || -0m00.00s | -9.09%
0m00.09s | Arith/Arith_base                     | 0m00.09s || +0m00.00s | +0.00%
0m00.09s | Logic_Type                           | 0m00.08s || +0m00.00s | +12.49%
0m00.08s | Arith/Le                             | 0m00.11s || -0m00.03s | -27.27%
0m00.08s | Numbers/BinNums                      | 0m00.06s || +0m00.02s | +33.33%
0m00.08s | Numbers/NatInt/NZBits                | 0m00.12s || -0m00.03s | -33.33%
0m00.08s | Numbers/NatInt/NZProperties          | 0m00.09s || -0m00.00s | -11.11%
0m00.08s | Program/Tactics                      | 0m00.08s || +0m00.00s | +0.00%
0m00.07s | Tactics                              | 0m00.10s || -0m00.03s | -30.00%
0m00.06s | Classes/SetoidTactics                | 0m00.06s || +0m00.00s | +0.00%
0m00.06s | Numbers/NumPrelude                   | 0m00.06s || +0m00.00s | +0.00%
0m00.05s | Classes/Init                         | 0m00.04s || +0m00.01s | +25.00%
0m00.05s | Prelude                              | 0m00.09s || -0m00.03s | -44.44%
0m00.05s | Setoids/Setoid                       | 0m00.08s || -0m00.03s | -37.50%
0m00.04s | Relations/Relations                  | 0m00.04s || +0m00.00s | +0.00%
0m00.04s | Tauto                                | 0m00.09s || -0m00.05s | -55.55%
0m00.02s | Notations                            | 0m00.04s || -0m00.02s | -50.00%

6 files changed, 592 insertions, 305 deletions

diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 1d0485ecd4..20b154b5d0 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -25,34 +25,40 @@ xorb: bool -> bool -> bool
 Nat.even: nat -> bool
 Nat.odd: nat -> bool
 BoolSpec: Prop -> Prop -> bool -> Prop
-Byte.byte_beq: Byte.byte -> Byte.byte -> bool
-Nat.testbit: nat -> nat -> bool
 Nat.eqb: nat -> nat -> bool
-Nat.leb: nat -> nat -> bool
+Nat.testbit: nat -> nat -> bool
 Nat.ltb: nat -> nat -> bool
+Nat.leb: nat -> nat -> bool
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
-eq_true_rect:
-  forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b
 bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
 bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
-eq_true_rect_r:
-  forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true
-eq_true_ind:
-  forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b
 eq_true_rec:
   forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b
+bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
+eq_true_rect_r:
+  forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true
 eq_true_rec_r:
   forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true
+eq_true_rect:
+  forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b
+eq_true_ind:
+  forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b
 eq_true_ind_r:
   forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true
-bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
-andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
+Byte.to_bits:
+  Byte.byte -> bool * bool * bool * bool * bool * bool * bool * bool
+Byte.of_bits:
+  bool * bool * bool * bool * bool * bool * bool * bool -> Byte.byte
 andb_true_intro:
   forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 BoolSpec_ind:
   forall (P Q : Prop) (P0 : bool -> Prop),
   (P -> P0 true) ->
   (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b
+Byte.to_bits_of_bits:
+  forall b : bool * bool * bool * bool * bool * bool * bool * bool,
+  Byte.to_bits (Byte.of_bits b) = b
 bool_choice:
   forall (S : Set) (R1 R2 : S -> Prop),
   (forall x : S, {R1 x} + {R2 x}) ->
diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out
index 04cd7c6c91..7038eac22c 100644
--- a/test-suite/output/SearchHead.out
+++ b/test-suite/output/SearchHead.out
@@ -17,7 +17,6 @@ Nat.leb: nat -> nat -> bool
 Nat.ltb: nat -> nat -> bool
 Nat.testbit: nat -> nat -> bool
 Nat.eqb: nat -> nat -> bool
-Byte.byte_beq: Byte.byte -> Byte.byte -> bool
 mult_n_O: forall n : nat, 0 = n * 0
 plus_O_n: forall n : nat, 0 + n = n
 plus_n_O: forall n : nat, n = n + 0
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index 5f63b3343d..b0ac9ea29f 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -11,7 +11,6 @@ Nat.leb: nat -> nat -> bool
 Nat.ltb: nat -> nat -> bool
 Nat.testbit: nat -> nat -> bool
 Nat.eqb: nat -> nat -> bool
-Byte.byte_beq: Byte.byte -> Byte.byte -> bool
 Nat.two: nat
 Nat.one: nat
 Nat.zero: nat
diff --git a/theories/Init/Byte.v b/theories/Init/Byte.v
index 2d8ee30a43..59b5f5ebe3 100644
--- a/theories/Init/Byte.v
+++ b/theories/Init/Byte.v
@@ -21,7 +21,6 @@ Declare ML Module "string_notation_plugin".
     which contains all ascii characters.  We use 256 constructors for
     efficiency and ease of conversion. *)
 
-Local Set Boolean Equality Schemes.
 Declare Scope byte_scope.
 Delimit Scope byte_scope with byte.
 
@@ -288,15 +287,544 @@ Bind Scope byte_scope with byte.
 
 Register byte as core.byte.type.
 
-Notation eqb := byte_beq.
+Local Notation "0" := false.
+Local Notation "1" := true.
+
+(** We pick a definition that matches with [Ascii.ascii] *)
+Definition of_bits (b : bool * bool * bool * bool * bool * bool * bool * bool) : byte
+  := match b with
+     | (0,0,0,0,0,0,0,0) => x00
+     | (1,0,0,0,0,0,0,0) => x01
+     | (0,1,0,0,0,0,0,0) => x02
+     | (1,1,0,0,0,0,0,0) => x03
+     | (0,0,1,0,0,0,0,0) => x04
+     | (1,0,1,0,0,0,0,0) => x05
+     | (0,1,1,0,0,0,0,0) => x06
+     | (1,1,1,0,0,0,0,0) => x07
+     | (0,0,0,1,0,0,0,0) => x08
+     | (1,0,0,1,0,0,0,0) => x09
+     | (0,1,0,1,0,0,0,0) => x0a
+     | (1,1,0,1,0,0,0,0) => x0b
+     | (0,0,1,1,0,0,0,0) => x0c
+     | (1,0,1,1,0,0,0,0) => x0d
+     | (0,1,1,1,0,0,0,0) => x0e
+     | (1,1,1,1,0,0,0,0) => x0f
+     | (0,0,0,0,1,0,0,0) => x10
+     | (1,0,0,0,1,0,0,0) => x11
+     | (0,1,0,0,1,0,0,0) => x12
+     | (1,1,0,0,1,0,0,0) => x13
+     | (0,0,1,0,1,0,0,0) => x14
+     | (1,0,1,0,1,0,0,0) => x15
+     | (0,1,1,0,1,0,0,0) => x16
+     | (1,1,1,0,1,0,0,0) => x17
+     | (0,0,0,1,1,0,0,0) => x18
+     | (1,0,0,1,1,0,0,0) => x19
+     | (0,1,0,1,1,0,0,0) => x1a
+     | (1,1,0,1,1,0,0,0) => x1b
+     | (0,0,1,1,1,0,0,0) => x1c
+     | (1,0,1,1,1,0,0,0) => x1d
+     | (0,1,1,1,1,0,0,0) => x1e
+     | (1,1,1,1,1,0,0,0) => x1f
+     | (0,0,0,0,0,1,0,0) => x20
+     | (1,0,0,0,0,1,0,0) => x21
+     | (0,1,0,0,0,1,0,0) => x22
+     | (1,1,0,0,0,1,0,0) => x23
+     | (0,0,1,0,0,1,0,0) => x24
+     | (1,0,1,0,0,1,0,0) => x25
+     | (0,1,1,0,0,1,0,0) => x26
+     | (1,1,1,0,0,1,0,0) => x27
+     | (0,0,0,1,0,1,0,0) => x28
+     | (1,0,0,1,0,1,0,0) => x29
+     | (0,1,0,1,0,1,0,0) => x2a
+     | (1,1,0,1,0,1,0,0) => x2b
+     | (0,0,1,1,0,1,0,0) => x2c
+     | (1,0,1,1,0,1,0,0) => x2d
+     | (0,1,1,1,0,1,0,0) => x2e
+     | (1,1,1,1,0,1,0,0) => x2f
+     | (0,0,0,0,1,1,0,0) => x30
+     | (1,0,0,0,1,1,0,0) => x31
+     | (0,1,0,0,1,1,0,0) => x32
+     | (1,1,0,0,1,1,0,0) => x33
+     | (0,0,1,0,1,1,0,0) => x34
+     | (1,0,1,0,1,1,0,0) => x35
+     | (0,1,1,0,1,1,0,0) => x36
+     | (1,1,1,0,1,1,0,0) => x37
+     | (0,0,0,1,1,1,0,0) => x38
+     | (1,0,0,1,1,1,0,0) => x39
+     | (0,1,0,1,1,1,0,0) => x3a
+     | (1,1,0,1,1,1,0,0) => x3b
+     | (0,0,1,1,1,1,0,0) => x3c
+     | (1,0,1,1,1,1,0,0) => x3d
+     | (0,1,1,1,1,1,0,0) => x3e
+     | (1,1,1,1,1,1,0,0) => x3f
+     | (0,0,0,0,0,0,1,0) => x40
+     | (1,0,0,0,0,0,1,0) => x41
+     | (0,1,0,0,0,0,1,0) => x42
+     | (1,1,0,0,0,0,1,0) => x43
+     | (0,0,1,0,0,0,1,0) => x44
+     | (1,0,1,0,0,0,1,0) => x45
+     | (0,1,1,0,0,0,1,0) => x46
+     | (1,1,1,0,0,0,1,0) => x47
+     | (0,0,0,1,0,0,1,0) => x48
+     | (1,0,0,1,0,0,1,0) => x49
+     | (0,1,0,1,0,0,1,0) => x4a
+     | (1,1,0,1,0,0,1,0) => x4b
+     | (0,0,1,1,0,0,1,0) => x4c
+     | (1,0,1,1,0,0,1,0) => x4d
+     | (0,1,1,1,0,0,1,0) => x4e
+     | (1,1,1,1,0,0,1,0) => x4f
+     | (0,0,0,0,1,0,1,0) => x50
+     | (1,0,0,0,1,0,1,0) => x51
+     | (0,1,0,0,1,0,1,0) => x52
+     | (1,1,0,0,1,0,1,0) => x53
+     | (0,0,1,0,1,0,1,0) => x54
+     | (1,0,1,0,1,0,1,0) => x55
+     | (0,1,1,0,1,0,1,0) => x56
+     | (1,1,1,0,1,0,1,0) => x57
+     | (0,0,0,1,1,0,1,0) => x58
+     | (1,0,0,1,1,0,1,0) => x59
+     | (0,1,0,1,1,0,1,0) => x5a
+     | (1,1,0,1,1,0,1,0) => x5b
+     | (0,0,1,1,1,0,1,0) => x5c
+     | (1,0,1,1,1,0,1,0) => x5d
+     | (0,1,1,1,1,0,1,0) => x5e
+     | (1,1,1,1,1,0,1,0) => x5f
+     | (0,0,0,0,0,1,1,0) => x60
+     | (1,0,0,0,0,1,1,0) => x61
+     | (0,1,0,0,0,1,1,0) => x62
+     | (1,1,0,0,0,1,1,0) => x63
+     | (0,0,1,0,0,1,1,0) => x64
+     | (1,0,1,0,0,1,1,0) => x65
+     | (0,1,1,0,0,1,1,0) => x66
+     | (1,1,1,0,0,1,1,0) => x67
+     | (0,0,0,1,0,1,1,0) => x68
+     | (1,0,0,1,0,1,1,0) => x69
+     | (0,1,0,1,0,1,1,0) => x6a
+     | (1,1,0,1,0,1,1,0) => x6b
+     | (0,0,1,1,0,1,1,0) => x6c
+     | (1,0,1,1,0,1,1,0) => x6d
+     | (0,1,1,1,0,1,1,0) => x6e
+     | (1,1,1,1,0,1,1,0) => x6f
+     | (0,0,0,0,1,1,1,0) => x70
+     | (1,0,0,0,1,1,1,0) => x71
+     | (0,1,0,0,1,1,1,0) => x72
+     | (1,1,0,0,1,1,1,0) => x73
+     | (0,0,1,0,1,1,1,0) => x74
+     | (1,0,1,0,1,1,1,0) => x75
+     | (0,1,1,0,1,1,1,0) => x76
+     | (1,1,1,0,1,1,1,0) => x77
+     | (0,0,0,1,1,1,1,0) => x78
+     | (1,0,0,1,1,1,1,0) => x79
+     | (0,1,0,1,1,1,1,0) => x7a
+     | (1,1,0,1,1,1,1,0) => x7b
+     | (0,0,1,1,1,1,1,0) => x7c
+     | (1,0,1,1,1,1,1,0) => x7d
+     | (0,1,1,1,1,1,1,0) => x7e
+     | (1,1,1,1,1,1,1,0) => x7f
+     | (0,0,0,0,0,0,0,1) => x80
+     | (1,0,0,0,0,0,0,1) => x81
+     | (0,1,0,0,0,0,0,1) => x82
+     | (1,1,0,0,0,0,0,1) => x83
+     | (0,0,1,0,0,0,0,1) => x84
+     | (1,0,1,0,0,0,0,1) => x85
+     | (0,1,1,0,0,0,0,1) => x86
+     | (1,1,1,0,0,0,0,1) => x87
+     | (0,0,0,1,0,0,0,1) => x88
+     | (1,0,0,1,0,0,0,1) => x89
+     | (0,1,0,1,0,0,0,1) => x8a
+     | (1,1,0,1,0,0,0,1) => x8b
+     | (0,0,1,1,0,0,0,1) => x8c
+     | (1,0,1,1,0,0,0,1) => x8d
+     | (0,1,1,1,0,0,0,1) => x8e
+     | (1,1,1,1,0,0,0,1) => x8f
+     | (0,0,0,0,1,0,0,1) => x90
+     | (1,0,0,0,1,0,0,1) => x91
+     | (0,1,0,0,1,0,0,1) => x92
+     | (1,1,0,0,1,0,0,1) => x93
+     | (0,0,1,0,1,0,0,1) => x94
+     | (1,0,1,0,1,0,0,1) => x95
+     | (0,1,1,0,1,0,0,1) => x96
+     | (1,1,1,0,1,0,0,1) => x97
+     | (0,0,0,1,1,0,0,1) => x98
+     | (1,0,0,1,1,0,0,1) => x99
+     | (0,1,0,1,1,0,0,1) => x9a
+     | (1,1,0,1,1,0,0,1) => x9b
+     | (0,0,1,1,1,0,0,1) => x9c
+     | (1,0,1,1,1,0,0,1) => x9d
+     | (0,1,1,1,1,0,0,1) => x9e
+     | (1,1,1,1,1,0,0,1) => x9f
+     | (0,0,0,0,0,1,0,1) => xa0
+     | (1,0,0,0,0,1,0,1) => xa1
+     | (0,1,0,0,0,1,0,1) => xa2
+     | (1,1,0,0,0,1,0,1) => xa3
+     | (0,0,1,0,0,1,0,1) => xa4
+     | (1,0,1,0,0,1,0,1) => xa5
+     | (0,1,1,0,0,1,0,1) => xa6
+     | (1,1,1,0,0,1,0,1) => xa7
+     | (0,0,0,1,0,1,0,1) => xa8
+     | (1,0,0,1,0,1,0,1) => xa9
+     | (0,1,0,1,0,1,0,1) => xaa
+     | (1,1,0,1,0,1,0,1) => xab
+     | (0,0,1,1,0,1,0,1) => xac
+     | (1,0,1,1,0,1,0,1) => xad
+     | (0,1,1,1,0,1,0,1) => xae
+     | (1,1,1,1,0,1,0,1) => xaf
+     | (0,0,0,0,1,1,0,1) => xb0
+     | (1,0,0,0,1,1,0,1) => xb1
+     | (0,1,0,0,1,1,0,1) => xb2
+     | (1,1,0,0,1,1,0,1) => xb3
+     | (0,0,1,0,1,1,0,1) => xb4
+     | (1,0,1,0,1,1,0,1) => xb5
+     | (0,1,1,0,1,1,0,1) => xb6
+     | (1,1,1,0,1,1,0,1) => xb7
+     | (0,0,0,1,1,1,0,1) => xb8
+     | (1,0,0,1,1,1,0,1) => xb9
+     | (0,1,0,1,1,1,0,1) => xba
+     | (1,1,0,1,1,1,0,1) => xbb
+     | (0,0,1,1,1,1,0,1) => xbc
+     | (1,0,1,1,1,1,0,1) => xbd
+     | (0,1,1,1,1,1,0,1) => xbe
+     | (1,1,1,1,1,1,0,1) => xbf
+     | (0,0,0,0,0,0,1,1) => xc0
+     | (1,0,0,0,0,0,1,1) => xc1
+     | (0,1,0,0,0,0,1,1) => xc2
+     | (1,1,0,0,0,0,1,1) => xc3
+     | (0,0,1,0,0,0,1,1) => xc4
+     | (1,0,1,0,0,0,1,1) => xc5
+     | (0,1,1,0,0,0,1,1) => xc6
+     | (1,1,1,0,0,0,1,1) => xc7
+     | (0,0,0,1,0,0,1,1) => xc8
+     | (1,0,0,1,0,0,1,1) => xc9
+     | (0,1,0,1,0,0,1,1) => xca
+     | (1,1,0,1,0,0,1,1) => xcb
+     | (0,0,1,1,0,0,1,1) => xcc
+     | (1,0,1,1,0,0,1,1) => xcd
+     | (0,1,1,1,0,0,1,1) => xce
+     | (1,1,1,1,0,0,1,1) => xcf
+     | (0,0,0,0,1,0,1,1) => xd0
+     | (1,0,0,0,1,0,1,1) => xd1
+     | (0,1,0,0,1,0,1,1) => xd2
+     | (1,1,0,0,1,0,1,1) => xd3
+     | (0,0,1,0,1,0,1,1) => xd4
+     | (1,0,1,0,1,0,1,1) => xd5
+     | (0,1,1,0,1,0,1,1) => xd6
+     | (1,1,1,0,1,0,1,1) => xd7
+     | (0,0,0,1,1,0,1,1) => xd8
+     | (1,0,0,1,1,0,1,1) => xd9
+     | (0,1,0,1,1,0,1,1) => xda
+     | (1,1,0,1,1,0,1,1) => xdb
+     | (0,0,1,1,1,0,1,1) => xdc
+     | (1,0,1,1,1,0,1,1) => xdd
+     | (0,1,1,1,1,0,1,1) => xde
+     | (1,1,1,1,1,0,1,1) => xdf
+     | (0,0,0,0,0,1,1,1) => xe0
+     | (1,0,0,0,0,1,1,1) => xe1
+     | (0,1,0,0,0,1,1,1) => xe2
+     | (1,1,0,0,0,1,1,1) => xe3
+     | (0,0,1,0,0,1,1,1) => xe4
+     | (1,0,1,0,0,1,1,1) => xe5
+     | (0,1,1,0,0,1,1,1) => xe6
+     | (1,1,1,0,0,1,1,1) => xe7
+     | (0,0,0,1,0,1,1,1) => xe8
+     | (1,0,0,1,0,1,1,1) => xe9
+     | (0,1,0,1,0,1,1,1) => xea
+     | (1,1,0,1,0,1,1,1) => xeb
+     | (0,0,1,1,0,1,1,1) => xec
+     | (1,0,1,1,0,1,1,1) => xed
+     | (0,1,1,1,0,1,1,1) => xee
+     | (1,1,1,1,0,1,1,1) => xef
+     | (0,0,0,0,1,1,1,1) => xf0
+     | (1,0,0,0,1,1,1,1) => xf1
+     | (0,1,0,0,1,1,1,1) => xf2
+     | (1,1,0,0,1,1,1,1) => xf3
+     | (0,0,1,0,1,1,1,1) => xf4
+     | (1,0,1,0,1,1,1,1) => xf5
+     | (0,1,1,0,1,1,1,1) => xf6
+     | (1,1,1,0,1,1,1,1) => xf7
+     | (0,0,0,1,1,1,1,1) => xf8
+     | (1,0,0,1,1,1,1,1) => xf9
+     | (0,1,0,1,1,1,1,1) => xfa
+     | (1,1,0,1,1,1,1,1) => xfb
+     | (0,0,1,1,1,1,1,1) => xfc
+     | (1,0,1,1,1,1,1,1) => xfd
+     | (0,1,1,1,1,1,1,1) => xfe
+     | (1,1,1,1,1,1,1,1) => xff
+     end.
+
+Definition to_bits (b : byte) : bool * bool * bool * bool * bool * bool * bool * bool
+  := match b with
+     | x00 => (0,0,0,0,0,0,0,0)
+     | x01 => (1,0,0,0,0,0,0,0)
+     | x02 => (0,1,0,0,0,0,0,0)
+     | x03 => (1,1,0,0,0,0,0,0)
+     | x04 => (0,0,1,0,0,0,0,0)
+     | x05 => (1,0,1,0,0,0,0,0)
+     | x06 => (0,1,1,0,0,0,0,0)
+     | x07 => (1,1,1,0,0,0,0,0)
+     | x08 => (0,0,0,1,0,0,0,0)
+     | x09 => (1,0,0,1,0,0,0,0)
+     | x0a => (0,1,0,1,0,0,0,0)
+     | x0b => (1,1,0,1,0,0,0,0)
+     | x0c => (0,0,1,1,0,0,0,0)
+     | x0d => (1,0,1,1,0,0,0,0)
+     | x0e => (0,1,1,1,0,0,0,0)
+     | x0f => (1,1,1,1,0,0,0,0)
+     | x10 => (0,0,0,0,1,0,0,0)
+     | x11 => (1,0,0,0,1,0,0,0)
+     | x12 => (0,1,0,0,1,0,0,0)
+     | x13 => (1,1,0,0,1,0,0,0)
+     | x14 => (0,0,1,0,1,0,0,0)
+     | x15 => (1,0,1,0,1,0,0,0)
+     | x16 => (0,1,1,0,1,0,0,0)
+     | x17 => (1,1,1,0,1,0,0,0)
+     | x18 => (0,0,0,1,1,0,0,0)
+     | x19 => (1,0,0,1,1,0,0,0)
+     | x1a => (0,1,0,1,1,0,0,0)
+     | x1b => (1,1,0,1,1,0,0,0)
+     | x1c => (0,0,1,1,1,0,0,0)
+     | x1d => (1,0,1,1,1,0,0,0)
+     | x1e => (0,1,1,1,1,0,0,0)
+     | x1f => (1,1,1,1,1,0,0,0)
+     | x20 => (0,0,0,0,0,1,0,0)
+     | x21 => (1,0,0,0,0,1,0,0)
+     | x22 => (0,1,0,0,0,1,0,0)
+     | x23 => (1,1,0,0,0,1,0,0)
+     | x24 => (0,0,1,0,0,1,0,0)
+     | x25 => (1,0,1,0,0,1,0,0)
+     | x26 => (0,1,1,0,0,1,0,0)
+     | x27 => (1,1,1,0,0,1,0,0)
+     | x28 => (0,0,0,1,0,1,0,0)
+     | x29 => (1,0,0,1,0,1,0,0)
+     | x2a => (0,1,0,1,0,1,0,0)
+     | x2b => (1,1,0,1,0,1,0,0)
+     | x2c => (0,0,1,1,0,1,0,0)
+     | x2d => (1,0,1,1,0,1,0,0)
+     | x2e => (0,1,1,1,0,1,0,0)
+     | x2f => (1,1,1,1,0,1,0,0)
+     | x30 => (0,0,0,0,1,1,0,0)
+     | x31 => (1,0,0,0,1,1,0,0)
+     | x32 => (0,1,0,0,1,1,0,0)
+     | x33 => (1,1,0,0,1,1,0,0)
+     | x34 => (0,0,1,0,1,1,0,0)
+     | x35 => (1,0,1,0,1,1,0,0)
+     | x36 => (0,1,1,0,1,1,0,0)
+     | x37 => (1,1,1,0,1,1,0,0)
+     | x38 => (0,0,0,1,1,1,0,0)
+     | x39 => (1,0,0,1,1,1,0,0)
+     | x3a => (0,1,0,1,1,1,0,0)
+     | x3b => (1,1,0,1,1,1,0,0)
+     | x3c => (0,0,1,1,1,1,0,0)
+     | x3d => (1,0,1,1,1,1,0,0)
+     | x3e => (0,1,1,1,1,1,0,0)
+     | x3f => (1,1,1,1,1,1,0,0)
+     | x40 => (0,0,0,0,0,0,1,0)
+     | x41 => (1,0,0,0,0,0,1,0)
+     | x42 => (0,1,0,0,0,0,1,0)
+     | x43 => (1,1,0,0,0,0,1,0)
+     | x44 => (0,0,1,0,0,0,1,0)
+     | x45 => (1,0,1,0,0,0,1,0)
+     | x46 => (0,1,1,0,0,0,1,0)
+     | x47 => (1,1,1,0,0,0,1,0)
+     | x48 => (0,0,0,1,0,0,1,0)
+     | x49 => (1,0,0,1,0,0,1,0)
+     | x4a => (0,1,0,1,0,0,1,0)
+     | x4b => (1,1,0,1,0,0,1,0)
+     | x4c => (0,0,1,1,0,0,1,0)
+     | x4d => (1,0,1,1,0,0,1,0)
+     | x4e => (0,1,1,1,0,0,1,0)
+     | x4f => (1,1,1,1,0,0,1,0)
+     | x50 => (0,0,0,0,1,0,1,0)
+     | x51 => (1,0,0,0,1,0,1,0)
+     | x52 => (0,1,0,0,1,0,1,0)
+     | x53 => (1,1,0,0,1,0,1,0)
+     | x54 => (0,0,1,0,1,0,1,0)
+     | x55 => (1,0,1,0,1,0,1,0)
+     | x56 => (0,1,1,0,1,0,1,0)
+     | x57 => (1,1,1,0,1,0,1,0)
+     | x58 => (0,0,0,1,1,0,1,0)
+     | x59 => (1,0,0,1,1,0,1,0)
+     | x5a => (0,1,0,1,1,0,1,0)
+     | x5b => (1,1,0,1,1,0,1,0)
+     | x5c => (0,0,1,1,1,0,1,0)
+     | x5d => (1,0,1,1,1,0,1,0)
+     | x5e => (0,1,1,1,1,0,1,0)
+     | x5f => (1,1,1,1,1,0,1,0)
+     | x60 => (0,0,0,0,0,1,1,0)
+     | x61 => (1,0,0,0,0,1,1,0)
+     | x62 => (0,1,0,0,0,1,1,0)
+     | x63 => (1,1,0,0,0,1,1,0)
+     | x64 => (0,0,1,0,0,1,1,0)
+     | x65 => (1,0,1,0,0,1,1,0)
+     | x66 => (0,1,1,0,0,1,1,0)
+     | x67 => (1,1,1,0,0,1,1,0)
+     | x68 => (0,0,0,1,0,1,1,0)
+     | x69 => (1,0,0,1,0,1,1,0)
+     | x6a => (0,1,0,1,0,1,1,0)
+     | x6b => (1,1,0,1,0,1,1,0)
+     | x6c => (0,0,1,1,0,1,1,0)
+     | x6d => (1,0,1,1,0,1,1,0)
+     | x6e => (0,1,1,1,0,1,1,0)
+     | x6f => (1,1,1,1,0,1,1,0)
+     | x70 => (0,0,0,0,1,1,1,0)
+     | x71 => (1,0,0,0,1,1,1,0)
+     | x72 => (0,1,0,0,1,1,1,0)
+     | x73 => (1,1,0,0,1,1,1,0)
+     | x74 => (0,0,1,0,1,1,1,0)
+     | x75 => (1,0,1,0,1,1,1,0)
+     | x76 => (0,1,1,0,1,1,1,0)
+     | x77 => (1,1,1,0,1,1,1,0)
+     | x78 => (0,0,0,1,1,1,1,0)
+     | x79 => (1,0,0,1,1,1,1,0)
+     | x7a => (0,1,0,1,1,1,1,0)
+     | x7b => (1,1,0,1,1,1,1,0)
+     | x7c => (0,0,1,1,1,1,1,0)
+     | x7d => (1,0,1,1,1,1,1,0)
+     | x7e => (0,1,1,1,1,1,1,0)
+     | x7f => (1,1,1,1,1,1,1,0)
+     | x80 => (0,0,0,0,0,0,0,1)
+     | x81 => (1,0,0,0,0,0,0,1)
+     | x82 => (0,1,0,0,0,0,0,1)
+     | x83 => (1,1,0,0,0,0,0,1)
+     | x84 => (0,0,1,0,0,0,0,1)
+     | x85 => (1,0,1,0,0,0,0,1)
+     | x86 => (0,1,1,0,0,0,0,1)
+     | x87 => (1,1,1,0,0,0,0,1)
+     | x88 => (0,0,0,1,0,0,0,1)
+     | x89 => (1,0,0,1,0,0,0,1)
+     | x8a => (0,1,0,1,0,0,0,1)
+     | x8b => (1,1,0,1,0,0,0,1)
+     | x8c => (0,0,1,1,0,0,0,1)
+     | x8d => (1,0,1,1,0,0,0,1)
+     | x8e => (0,1,1,1,0,0,0,1)
+     | x8f => (1,1,1,1,0,0,0,1)
+     | x90 => (0,0,0,0,1,0,0,1)
+     | x91 => (1,0,0,0,1,0,0,1)
+     | x92 => (0,1,0,0,1,0,0,1)
+     | x93 => (1,1,0,0,1,0,0,1)
+     | x94 => (0,0,1,0,1,0,0,1)
+     | x95 => (1,0,1,0,1,0,0,1)
+     | x96 => (0,1,1,0,1,0,0,1)
+     | x97 => (1,1,1,0,1,0,0,1)
+     | x98 => (0,0,0,1,1,0,0,1)
+     | x99 => (1,0,0,1,1,0,0,1)
+     | x9a => (0,1,0,1,1,0,0,1)
+     | x9b => (1,1,0,1,1,0,0,1)
+     | x9c => (0,0,1,1,1,0,0,1)
+     | x9d => (1,0,1,1,1,0,0,1)
+     | x9e => (0,1,1,1,1,0,0,1)
+     | x9f => (1,1,1,1,1,0,0,1)
+     | xa0 => (0,0,0,0,0,1,0,1)
+     | xa1 => (1,0,0,0,0,1,0,1)
+     | xa2 => (0,1,0,0,0,1,0,1)
+     | xa3 => (1,1,0,0,0,1,0,1)
+     | xa4 => (0,0,1,0,0,1,0,1)
+     | xa5 => (1,0,1,0,0,1,0,1)
+     | xa6 => (0,1,1,0,0,1,0,1)
+     | xa7 => (1,1,1,0,0,1,0,1)
+     | xa8 => (0,0,0,1,0,1,0,1)
+     | xa9 => (1,0,0,1,0,1,0,1)
+     | xaa => (0,1,0,1,0,1,0,1)
+     | xab => (1,1,0,1,0,1,0,1)
+     | xac => (0,0,1,1,0,1,0,1)
+     | xad => (1,0,1,1,0,1,0,1)
+     | xae => (0,1,1,1,0,1,0,1)
+     | xaf => (1,1,1,1,0,1,0,1)
+     | xb0 => (0,0,0,0,1,1,0,1)
+     | xb1 => (1,0,0,0,1,1,0,1)
+     | xb2 => (0,1,0,0,1,1,0,1)
+     | xb3 => (1,1,0,0,1,1,0,1)
+     | xb4 => (0,0,1,0,1,1,0,1)
+     | xb5 => (1,0,1,0,1,1,0,1)
+     | xb6 => (0,1,1,0,1,1,0,1)
+     | xb7 => (1,1,1,0,1,1,0,1)
+     | xb8 => (0,0,0,1,1,1,0,1)
+     | xb9 => (1,0,0,1,1,1,0,1)
+     | xba => (0,1,0,1,1,1,0,1)
+     | xbb => (1,1,0,1,1,1,0,1)
+     | xbc => (0,0,1,1,1,1,0,1)
+     | xbd => (1,0,1,1,1,1,0,1)
+     | xbe => (0,1,1,1,1,1,0,1)
+     | xbf => (1,1,1,1,1,1,0,1)
+     | xc0 => (0,0,0,0,0,0,1,1)
+     | xc1 => (1,0,0,0,0,0,1,1)
+     | xc2 => (0,1,0,0,0,0,1,1)
+     | xc3 => (1,1,0,0,0,0,1,1)
+     | xc4 => (0,0,1,0,0,0,1,1)
+     | xc5 => (1,0,1,0,0,0,1,1)
+     | xc6 => (0,1,1,0,0,0,1,1)
+     | xc7 => (1,1,1,0,0,0,1,1)
+     | xc8 => (0,0,0,1,0,0,1,1)
+     | xc9 => (1,0,0,1,0,0,1,1)
+     | xca => (0,1,0,1,0,0,1,1)
+     | xcb => (1,1,0,1,0,0,1,1)
+     | xcc => (0,0,1,1,0,0,1,1)
+     | xcd => (1,0,1,1,0,0,1,1)
+     | xce => (0,1,1,1,0,0,1,1)
+     | xcf => (1,1,1,1,0,0,1,1)
+     | xd0 => (0,0,0,0,1,0,1,1)
+     | xd1 => (1,0,0,0,1,0,1,1)
+     | xd2 => (0,1,0,0,1,0,1,1)
+     | xd3 => (1,1,0,0,1,0,1,1)
+     | xd4 => (0,0,1,0,1,0,1,1)
+     | xd5 => (1,0,1,0,1,0,1,1)
+     | xd6 => (0,1,1,0,1,0,1,1)
+     | xd7 => (1,1,1,0,1,0,1,1)
+     | xd8 => (0,0,0,1,1,0,1,1)
+     | xd9 => (1,0,0,1,1,0,1,1)
+     | xda => (0,1,0,1,1,0,1,1)
+     | xdb => (1,1,0,1,1,0,1,1)
+     | xdc => (0,0,1,1,1,0,1,1)
+     | xdd => (1,0,1,1,1,0,1,1)
+     | xde => (0,1,1,1,1,0,1,1)
+     | xdf => (1,1,1,1,1,0,1,1)
+     | xe0 => (0,0,0,0,0,1,1,1)
+     | xe1 => (1,0,0,0,0,1,1,1)
+     | xe2 => (0,1,0,0,0,1,1,1)
+     | xe3 => (1,1,0,0,0,1,1,1)
+     | xe4 => (0,0,1,0,0,1,1,1)
+     | xe5 => (1,0,1,0,0,1,1,1)
+     | xe6 => (0,1,1,0,0,1,1,1)
+     | xe7 => (1,1,1,0,0,1,1,1)
+     | xe8 => (0,0,0,1,0,1,1,1)
+     | xe9 => (1,0,0,1,0,1,1,1)
+     | xea => (0,1,0,1,0,1,1,1)
+     | xeb => (1,1,0,1,0,1,1,1)
+     | xec => (0,0,1,1,0,1,1,1)
+     | xed => (1,0,1,1,0,1,1,1)
+     | xee => (0,1,1,1,0,1,1,1)
+     | xef => (1,1,1,1,0,1,1,1)
+     | xf0 => (0,0,0,0,1,1,1,1)
+     | xf1 => (1,0,0,0,1,1,1,1)
+     | xf2 => (0,1,0,0,1,1,1,1)
+     | xf3 => (1,1,0,0,1,1,1,1)
+     | xf4 => (0,0,1,0,1,1,1,1)
+     | xf5 => (1,0,1,0,1,1,1,1)
+     | xf6 => (0,1,1,0,1,1,1,1)
+     | xf7 => (1,1,1,0,1,1,1,1)
+     | xf8 => (0,0,0,1,1,1,1,1)
+     | xf9 => (1,0,0,1,1,1,1,1)
+     | xfa => (0,1,0,1,1,1,1,1)
+     | xfb => (1,1,0,1,1,1,1,1)
+     | xfc => (0,0,1,1,1,1,1,1)
+     | xfd => (1,0,1,1,1,1,1,1)
+     | xfe => (0,1,1,1,1,1,1,1)
+     | xff => (1,1,1,1,1,1,1,1)
+     end.
+
+Lemma of_bits_to_bits (b : byte) : of_bits (to_bits b) = b.
+Proof. destruct b; exact eq_refl. Qed.
+
+Lemma to_bits_of_bits (b : _) : to_bits (of_bits b) = b.
+Proof.
+  repeat match goal with
+         | p : prod _ _ |- _ => destruct p
+         | b : bool |- _ => destruct b
+         end;
+    exact eq_refl.
+Qed.
 
 Definition byte_of_byte (b : byte) : byte := b.
 
 Module Export ByteSyntaxNotations.
   String Notation byte byte_of_byte byte_of_byte : byte_scope.
 End ByteSyntaxNotations.
-
-Module Export ByteNotations.
-  Export ByteSyntaxNotations.
-  Infix "=?" := eqb (at level 70) : byte_scope.
-End ByteNotations.
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index 13757c6007..a7bb1732be 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -190,36 +190,29 @@ Qed.
  *)
 
 Definition ascii_of_byte (b : byte) : ascii
-  := ascii_of_N (Byte.to_N b).
+  := let '(b7, b6, b5, b4, b3, b2, b1, b0) := Byte.to_bits b in
+     Ascii b7 b6 b5 b4 b3 b2 b1 b0.
 
 Definition byte_of_ascii (a : ascii) : byte
-  := match Byte.of_N (N_of_ascii a) with
-     | Some v => v
-     | None => x00 (* can't happen *)
-     end.
+  := let (b7, b6, b5, b4, b3, b2, b1, b0) := a in
+     Byte.of_bits (b7, b6, b5, b4, b3, b2, b1, b0).
 
 Lemma ascii_of_byte_of_ascii x : ascii_of_byte (byte_of_ascii x) = x.
 Proof.
   cbv [ascii_of_byte byte_of_ascii].
-  pose proof (to_of_N (N_of_ascii x)).
-  destruct (of_N (N_of_ascii x)) as [x'|] eqn:H1.
-  { specialize (H x' eq_refl); rewrite H.
-    apply ascii_N_embedding. }
-  { exfalso.
-    rewrite of_N_None_iff in H1.
-    pose proof (N_ascii_bounded x) as H2.
-    rewrite N.lt_nge in H1, H2.
-    destruct (N.le_gt_cases (N_of_ascii x) 255) as [H3|H3].
-    { apply H1, H3. }
-    { rewrite <- N.le_succ_l in H3; apply H2, H3. } }
+  destruct x; rewrite to_bits_of_bits; reflexivity.
 Qed.
 
 Lemma byte_of_ascii_of_byte x : byte_of_ascii (ascii_of_byte x) = x.
 Proof.
   cbv [ascii_of_byte byte_of_ascii].
-  rewrite N_ascii_embedding, of_to_N; [ reflexivity | ].
-  pose proof (to_N_bounded x) as H.
-  rewrite <- N.lt_succ_r in H; exact H.
+  repeat match goal with
+         | [ |- context[match ?x with pair _ _ => _ end] ]
+           => rewrite (surjective_pairing x)
+         | [ |- context[(fst ?x, snd ?x)] ]
+           => rewrite <- (surjective_pairing x)
+         end.
+  rewrite of_bits_to_bits; reflexivity.
 Qed.
 
 Module Export AsciiSyntax.
diff --git a/theories/Strings/Byte.v b/theories/Strings/Byte.v
index 581094a8b5..d4c719bb4c 100644
--- a/theories/Strings/Byte.v
+++ b/theories/Strings/Byte.v
@@ -14,278 +14,40 @@ Require Export Coq.Init.Byte.
 
 Local Set Implicit Arguments.
 
-Lemma byte_dec_lb x y : x = y -> Byte.eqb x y = true.
+Definition eqb (a b : byte) : bool
+  := let '(a7, a6, a5, a4, a3, a2, a1, a0) := to_bits a in
+     let '(b7, b6, b5, b4, b3, b2, b1, b0) := to_bits b in
+     (Bool.eqb a0 b0 && Bool.eqb a1 b1 && Bool.eqb a2 b2 && Bool.eqb a3 b3 &&
+          Bool.eqb a4 b4 && Bool.eqb a5 b5 && Bool.eqb a6 b6 && Bool.eqb a7 b7)%bool.
+
+Module Export ByteNotations.
+  Export ByteSyntaxNotations.
+  Infix "=?" := eqb (at level 70) : byte_scope.
+End ByteNotations.
+
+Lemma byte_dec_lb x y : x = y -> eqb x y = true.
 Proof. intro; subst y; destruct x; reflexivity. Defined.
 
-Definition byte_dec_bl x y (H : Byte.eqb x y = true) : x = y
-  := match H in (_ = tr) return if tr then x = y else True with
-     | eq_refl
-       => match x, y return if Byte.eqb x y then x = y else True with
-          | x00, x00 => eq_refl
-          | x01, x01 => eq_refl
-          | x02, x02 => eq_refl
-          | x03, x03 => eq_refl
-          | x04, x04 => eq_refl
-          | x05, x05 => eq_refl
-          | x06, x06 => eq_refl
-          | x07, x07 => eq_refl
-          | x08, x08 => eq_refl
-          | x09, x09 => eq_refl
-          | x0a, x0a => eq_refl
-          | x0b, x0b => eq_refl
-          | x0c, x0c => eq_refl
-          | x0d, x0d => eq_refl
-          | x0e, x0e => eq_refl
-          | x0f, x0f => eq_refl
-          | x10, x10 => eq_refl
-          | x11, x11 => eq_refl
-          | x12, x12 => eq_refl
-          | x13, x13 => eq_refl
-          | x14, x14 => eq_refl
-          | x15, x15 => eq_refl
-          | x16, x16 => eq_refl
-          | x17, x17 => eq_refl
-          | x18, x18 => eq_refl
-          | x19, x19 => eq_refl
-          | x1a, x1a => eq_refl
-          | x1b, x1b => eq_refl
-          | x1c, x1c => eq_refl
-          | x1d, x1d => eq_refl
-          | x1e, x1e => eq_refl
-          | x1f, x1f => eq_refl
-          | x20, x20 => eq_refl
-          | x21, x21 => eq_refl
-          | x22, x22 => eq_refl
-          | x23, x23 => eq_refl
-          | x24, x24 => eq_refl
-          | x25, x25 => eq_refl
-          | x26, x26 => eq_refl
-          | x27, x27 => eq_refl
-          | x28, x28 => eq_refl
-          | x29, x29 => eq_refl
-          | x2a, x2a => eq_refl
-          | x2b, x2b => eq_refl
-          | x2c, x2c => eq_refl
-          | x2d, x2d => eq_refl
-          | x2e, x2e => eq_refl
-          | x2f, x2f => eq_refl
-          | x30, x30 => eq_refl
-          | x31, x31 => eq_refl
-          | x32, x32 => eq_refl
-          | x33, x33 => eq_refl
-          | x34, x34 => eq_refl
-          | x35, x35 => eq_refl
-          | x36, x36 => eq_refl
-          | x37, x37 => eq_refl
-          | x38, x38 => eq_refl
-          | x39, x39 => eq_refl
-          | x3a, x3a => eq_refl
-          | x3b, x3b => eq_refl
-          | x3c, x3c => eq_refl
-          | x3d, x3d => eq_refl
-          | x3e, x3e => eq_refl
-          | x3f, x3f => eq_refl
-          | x40, x40 => eq_refl
-          | x41, x41 => eq_refl
-          | x42, x42 => eq_refl
-          | x43, x43 => eq_refl
-          | x44, x44 => eq_refl
-          | x45, x45 => eq_refl
-          | x46, x46 => eq_refl
-          | x47, x47 => eq_refl
-          | x48, x48 => eq_refl
-          | x49, x49 => eq_refl
-          | x4a, x4a => eq_refl
-          | x4b, x4b => eq_refl
-          | x4c, x4c => eq_refl
-          | x4d, x4d => eq_refl
-          | x4e, x4e => eq_refl
-          | x4f, x4f => eq_refl
-          | x50, x50 => eq_refl
-          | x51, x51 => eq_refl
-          | x52, x52 => eq_refl
-          | x53, x53 => eq_refl
-          | x54, x54 => eq_refl
-          | x55, x55 => eq_refl
-          | x56, x56 => eq_refl
-          | x57, x57 => eq_refl
-          | x58, x58 => eq_refl
-          | x59, x59 => eq_refl
-          | x5a, x5a => eq_refl
-          | x5b, x5b => eq_refl
-          | x5c, x5c => eq_refl
-          | x5d, x5d => eq_refl
-          | x5e, x5e => eq_refl
-          | x5f, x5f => eq_refl
-          | x60, x60 => eq_refl
-          | x61, x61 => eq_refl
-          | x62, x62 => eq_refl
-          | x63, x63 => eq_refl
-          | x64, x64 => eq_refl
-          | x65, x65 => eq_refl
-          | x66, x66 => eq_refl
-          | x67, x67 => eq_refl
-          | x68, x68 => eq_refl
-          | x69, x69 => eq_refl
-          | x6a, x6a => eq_refl
-          | x6b, x6b => eq_refl
-          | x6c, x6c => eq_refl
-          | x6d, x6d => eq_refl
-          | x6e, x6e => eq_refl
-          | x6f, x6f => eq_refl
-          | x70, x70 => eq_refl
-          | x71, x71 => eq_refl
-          | x72, x72 => eq_refl
-          | x73, x73 => eq_refl
-          | x74, x74 => eq_refl
-          | x75, x75 => eq_refl
-          | x76, x76 => eq_refl
-          | x77, x77 => eq_refl
-          | x78, x78 => eq_refl
-          | x79, x79 => eq_refl
-          | x7a, x7a => eq_refl
-          | x7b, x7b => eq_refl
-          | x7c, x7c => eq_refl
-          | x7d, x7d => eq_refl
-          | x7e, x7e => eq_refl
-          | x7f, x7f => eq_refl
-          | x80, x80 => eq_refl
-          | x81, x81 => eq_refl
-          | x82, x82 => eq_refl
-          | x83, x83 => eq_refl
-          | x84, x84 => eq_refl
-          | x85, x85 => eq_refl
-          | x86, x86 => eq_refl
-          | x87, x87 => eq_refl
-          | x88, x88 => eq_refl
-          | x89, x89 => eq_refl
-          | x8a, x8a => eq_refl
-          | x8b, x8b => eq_refl
-          | x8c, x8c => eq_refl
-          | x8d, x8d => eq_refl
-          | x8e, x8e => eq_refl
-          | x8f, x8f => eq_refl
-          | x90, x90 => eq_refl
-          | x91, x91 => eq_refl
-          | x92, x92 => eq_refl
-          | x93, x93 => eq_refl
-          | x94, x94 => eq_refl
-          | x95, x95 => eq_refl
-          | x96, x96 => eq_refl
-          | x97, x97 => eq_refl
-          | x98, x98 => eq_refl
-          | x99, x99 => eq_refl
-          | x9a, x9a => eq_refl
-          | x9b, x9b => eq_refl
-          | x9c, x9c => eq_refl
-          | x9d, x9d => eq_refl
-          | x9e, x9e => eq_refl
-          | x9f, x9f => eq_refl
-          | xa0, xa0 => eq_refl
-          | xa1, xa1 => eq_refl
-          | xa2, xa2 => eq_refl
-          | xa3, xa3 => eq_refl
-          | xa4, xa4 => eq_refl
-          | xa5, xa5 => eq_refl
-          | xa6, xa6 => eq_refl
-          | xa7, xa7 => eq_refl
-          | xa8, xa8 => eq_refl
-          | xa9, xa9 => eq_refl
-          | xaa, xaa => eq_refl
-          | xab, xab => eq_refl
-          | xac, xac => eq_refl
-          | xad, xad => eq_refl
-          | xae, xae => eq_refl
-          | xaf, xaf => eq_refl
-          | xb0, xb0 => eq_refl
-          | xb1, xb1 => eq_refl
-          | xb2, xb2 => eq_refl
-          | xb3, xb3 => eq_refl
-          | xb4, xb4 => eq_refl
-          | xb5, xb5 => eq_refl
-          | xb6, xb6 => eq_refl
-          | xb7, xb7 => eq_refl
-          | xb8, xb8 => eq_refl
-          | xb9, xb9 => eq_refl
-          | xba, xba => eq_refl
-          | xbb, xbb => eq_refl
-          | xbc, xbc => eq_refl
-          | xbd, xbd => eq_refl
-          | xbe, xbe => eq_refl
-          | xbf, xbf => eq_refl
-          | xc0, xc0 => eq_refl
-          | xc1, xc1 => eq_refl
-          | xc2, xc2 => eq_refl
-          | xc3, xc3 => eq_refl
-          | xc4, xc4 => eq_refl
-          | xc5, xc5 => eq_refl
-          | xc6, xc6 => eq_refl
-          | xc7, xc7 => eq_refl
-          | xc8, xc8 => eq_refl
-          | xc9, xc9 => eq_refl
-          | xca, xca => eq_refl
-          | xcb, xcb => eq_refl
-          | xcc, xcc => eq_refl
-          | xcd, xcd => eq_refl
-          | xce, xce => eq_refl
-          | xcf, xcf => eq_refl
-          | xd0, xd0 => eq_refl
-          | xd1, xd1 => eq_refl
-          | xd2, xd2 => eq_refl
-          | xd3, xd3 => eq_refl
-          | xd4, xd4 => eq_refl
-          | xd5, xd5 => eq_refl
-          | xd6, xd6 => eq_refl
-          | xd7, xd7 => eq_refl
-          | xd8, xd8 => eq_refl
-          | xd9, xd9 => eq_refl
-          | xda, xda => eq_refl
-          | xdb, xdb => eq_refl
-          | xdc, xdc => eq_refl
-          | xdd, xdd => eq_refl
-          | xde, xde => eq_refl
-          | xdf, xdf => eq_refl
-          | xe0, xe0 => eq_refl
-          | xe1, xe1 => eq_refl
-          | xe2, xe2 => eq_refl
-          | xe3, xe3 => eq_refl
-          | xe4, xe4 => eq_refl
-          | xe5, xe5 => eq_refl
-          | xe6, xe6 => eq_refl
-          | xe7, xe7 => eq_refl
-          | xe8, xe8 => eq_refl
-          | xe9, xe9 => eq_refl
-          | xea, xea => eq_refl
-          | xeb, xeb => eq_refl
-          | xec, xec => eq_refl
-          | xed, xed => eq_refl
-          | xee, xee => eq_refl
-          | xef, xef => eq_refl
-          | xf0, xf0 => eq_refl
-          | xf1, xf1 => eq_refl
-          | xf2, xf2 => eq_refl
-          | xf3, xf3 => eq_refl
-          | xf4, xf4 => eq_refl
-          | xf5, xf5 => eq_refl
-          | xf6, xf6 => eq_refl
-          | xf7, xf7 => eq_refl
-          | xf8, xf8 => eq_refl
-          | xf9, xf9 => eq_refl
-          | xfa, xfa => eq_refl
-          | xfb, xfb => eq_refl
-          | xfc, xfc => eq_refl
-          | xfd, xfd => eq_refl
-          | xfe, xfe => eq_refl
-          | xff, xff => eq_refl
-          | _, _ => I
-          end
-     end.
+Lemma byte_dec_bl x y (H : eqb x y = true) : x = y.
+Proof.
+  rewrite <- (of_bits_to_bits x), <- (of_bits_to_bits y).
+  cbv [eqb] in H; revert H.
+  generalize (to_bits x) (to_bits y); clear x y; intros x y H.
+  repeat match goal with
+         | [ H : and _ _ |- _ ] => destruct H
+         | [ H : prod _ _ |- _ ] => destruct H
+         | [ H : context[andb _ _ = true] |- _ ] => rewrite Bool.andb_true_iff in H
+         | [ H : context[Bool.eqb _ _ = true] |- _ ] => rewrite Bool.eqb_true_iff in H
+         | _ => progress subst
+         | _ => reflexivity
+         end.
+Qed.
 
-Lemma eqb_false x y : Byte.eqb x y = false -> x <> y.
+Lemma eqb_false x y : eqb x y = false -> x <> y.
 Proof. intros H H'; pose proof (byte_dec_lb H'); congruence. Qed.
 
 Definition byte_eq_dec (x y : byte) : {x = y} + {x <> y}
-  := (if Byte.eqb x y as beq return Byte.eqb x y = beq -> _
+  := (if eqb x y as beq return eqb x y = beq -> _
       then fun pf => left (byte_dec_bl x y pf)
       else fun pf => right (eqb_false pf))
        eq_refl.