proposition: Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
proof: Proof. intros x y; unfold eq, lt, compare. destruct (N_as_OT.compare_spec (N_of_ascii x) (N_of_ascii y)) as [H|H|H]; constructor; try assumption. now rewrite <- (ascii_N_embedding x), <- (ascii_N_embedding y), H. Qed.
imports: Orders BoolOrder PeanoNat POrderedType BinNat BinInt RelationPairs EqualitiesFacts Ascii String