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%

2 files changed, 40 insertions, 285 deletions

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.