proposition: Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
proof: Proof. unfold eq, lt. induction x; destruct y; try constructor; simpl; auto. - destruct (IHx y); subst; auto. - destruct (IHx y); subst; auto. Qed.
imports: Orders BoolOrder PeanoNat POrderedType BinNat BinInt RelationPairs EqualitiesFacts Ascii String