proposition: Lemma byte_of_ascii_of_byte x : byte_of_ascii (ascii_of_byte x) = x.
proof: Proof. cbv [ascii_of_byte byte_of_ascii]. 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.
imports: Bool BinPos BinNat PeanoNat Nnat Coq.Strings.Byte