proposition: Lemma cmp_eq (a b : ascii): cmp a b = Eq <-> a = b.
proof: Proof. unfold cmp, Ascii.compare. rewrite N.compare_eq_iff. split. 2:{ intro. now subst. } intro H. rewrite<- (ascii_N_embedding a). rewrite<- (ascii_N_embedding b). now rewrite H. Qed.
imports: OrderedType ZArith_base PeanoNat Peano_dec Compare_dec Ascii String NArith Ndec