proposition: Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
proof: Proof. unfold eq, lt. induction x as [|x xs IHxs], y as [|y ys]; cbn [compare]; try constructor; cbn [compare]; try reflexivity. specialize (IHxs ys). destruct (Ascii_as_OT.compare x y) eqn:H; [ destruct IHxs; constructor | constructor | constructor ]; cbn [compare]. all: destruct (Ascii_as_OT.compare_spec y x), (Ascii_as_OT.compare_spec x y); cbv [Ascii_as_OT.eq] in *; try congruence; subst. all: exfalso; eapply irreflexivity; (idtac + etransitivity); eassumption. Qed.
imports: Orders BoolOrder PeanoNat POrderedType BinNat BinInt RelationPairs EqualitiesFacts Ascii String