proposition: Theorem nat_ascii_embedding : forall n : nat, n < 256 -> nat_of_ascii (ascii_of_nat n) = n.
proof: Proof. intros. unfold nat_of_ascii, ascii_of_nat. rewrite N_ascii_embedding. - apply Nat2N.id. - unfold N.lt. change 256%N with (N.of_nat 256). rewrite <- Nat2N.inj_compare. now apply Nat.compare_lt_iff. Qed.
imports: Bool BinPos BinNat PeanoNat Nnat Coq.Strings.Byte