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