proposition: Theorem nat_ascii_bounded : forall a : ascii, nat_of_ascii a < 256.
proof: Proof. intro a; unfold nat_of_ascii. change 256 with (N.to_nat 256). rewrite <- Nat.compare_lt_iff, <- N2Nat.inj_compare, N.compare_lt_iff. apply N_ascii_bounded. Qed.
imports: Bool BinPos BinNat PeanoNat Nnat Coq.Strings.Byte