proposition: Lemma compare_Eq : forall x y, compare x y = Eq <-> eq x y.
proof: Proof. unfold compare. intros x y; destruct (compare_spec x y); intuition; try discriminate. - rewrite H0 in H. elim (StrictOrder_Irreflexive y); auto. - rewrite H0 in H. elim (StrictOrder_Irreflexive y); auto. Qed.
imports: OrderedType Orders