proposition: Lemma compare_eq_iff (a b : ascii) : compare a b = Eq -> a = b.
proof: Proof. unfold compare. intros H. apply N.compare_eq_iff in H. rewrite <- ascii_N_embedding. rewrite <- H. rewrite ascii_N_embedding. reflexivity. Qed.
imports: Bool BinPos BinNat PeanoNat Nnat Coq.Strings.Byte