proposition: Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
proof: Proof. intros (x1,x2) (y1,y2); unfold compare; simpl. destruct (O1.compare_spec x1 y1); try (constructor; compute; auto). destruct (O2.compare_spec x2 y2); constructor; compute; auto with relations. Qed.
imports: Orders BoolOrder PeanoNat POrderedType BinNat BinInt RelationPairs EqualitiesFacts Ascii String