proposition: Lemma compare_sym : forall x y, (y?=x) = CompOpp (x?=y).
proof: Proof. intros x y; unfold compare. destruct (compare_spec x y) as [U|U|U]; destruct (compare_spec y x) as [V|V|V]; auto. - rewrite U in V. elim (StrictOrder_Irreflexive y); auto. - rewrite U in V. elim (StrictOrder_Irreflexive y); auto. - rewrite V in U. elim (StrictOrder_Irreflexive x); auto. - rewrite V in U. elim (StrictOrder_Irreflexive x); auto. - rewrite V in U. elim (StrictOrder_Irreflexive x); auto. - rewrite V in U. elim (StrictOrder_Irreflexive y); auto. Qed.
imports: OrderedType Orders