proposition: Lemma compare_eq_iff (a b: A): compare a b = Eq <-> a = b.
proof: Proof. pose proof (comparable_comp_spec a b) as [Heq | H | H]; split; intro; subst; try easy; now apply StrictOrder_Irreflexive in H. Qed.
imports: Coq(Relations RelationClasses Setoid)