proposition: Lemma cmp_lt_nat (a b : ascii): cmp a b = Lt <-> (nat_of_ascii a < nat_of_ascii b)%nat.
proof: Proof. unfold cmp. unfold nat_of_ascii, Ascii.compare. rewrite N2Nat.inj_compare. rewrite Nat.compare_lt_iff. reflexivity. Qed.
imports: OrderedType ZArith_base PeanoNat Peano_dec Compare_dec Ascii String NArith Ndec