proposition: Theorem ascii_nat_embedding : forall a : ascii, ascii_of_nat (nat_of_ascii a) = a.
proof: Proof. intro a; destruct a as [[|][|][|][|][|][|][|][|]]; compute; reflexivity. Qed.
imports: Bool BinPos BinNat PeanoNat Nnat Coq.Strings.Byte