proposition: Lemma nat_of_ascii_inverse a b : nat_of_ascii a = nat_of_ascii b -> a = b.
proof: Proof. intro H. rewrite <- (ascii_nat_embedding a). rewrite <- (ascii_nat_embedding b). apply f_equal; auto. Qed.
imports: OrderedType ZArith_base PeanoNat Peano_dec Compare_dec Ascii String NArith Ndec