proposition: Lemma ascii_of_byte_of_ascii x : ascii_of_byte (byte_of_ascii x) = x.
proof: Proof. cbv [ascii_of_byte byte_of_ascii]. destruct x; rewrite to_bits_of_bits; reflexivity. Qed.
imports: Bool BinPos BinNat PeanoNat Nnat Coq.Strings.Byte