proposition: Lemma compare_spec x y : CompareSpec (x==y) (x<y) (y<x) (x?=y).
proof: Proof. case_eq (compare x y); intros H; constructor. - now apply compare_eq_iff. - now apply compare_lt_iff. - rewrite compare_antisym, CompOpp_iff in H. now apply compare_lt_iff. Qed.
imports: Bool Basics OrdersTac Orders