proposition: Lemma byte_dec_bl x y (H : eqb x y = true) : x = y.
proof: 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.
imports: Coq.Arith.EqNat Coq.NArith.BinNat Coq.NArith.Nnat Coq.Init.Byte