proposition: Theorem ascii_N_embedding : forall a : ascii, ascii_of_N (N_of_ascii a) = a.
proof: Proof. intro a; destruct a as [[|][|][|][|][|][|][|][|]]; vm_compute; reflexivity. Qed.
imports: Bool BinPos BinNat PeanoNat Nnat Coq.Strings.Byte