proposition: Theorem N_ascii_embedding : forall n:N, (n < 256)%N -> N_of_ascii (ascii_of_N n) = n.
proof: Proof. intro n; destruct n as [|p]. - reflexivity. - do 8 (destruct p as [p|p|]; [ | | intros; vm_compute; reflexivity ]); intro H; vm_compute in H; destruct p; discriminate. Qed.
imports: Bool BinPos BinNat PeanoNat Nnat Coq.Strings.Byte