fact: Definition byte_eq_dec (x y : byte) : {x = y} + {x <> y} := (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.
imports: Coq.Arith.EqNat Coq.NArith.BinNat Coq.NArith.Nnat Coq.Init.Byte