proposition: Lemma byte_of_ascii_via_nat x : Some (byte_of_ascii x) = Byte.of_nat (nat_of_ascii x).
proof: Proof. rewrite <- (ascii_of_byte_of_ascii x); destruct (byte_of_ascii x); reflexivity. Qed.
imports: Bool BinPos BinNat PeanoNat Nnat Coq.Strings.Byte