proposition: Lemma compare_refl (a: A): compare a a = Eq.
proof: Proof. pose proof (comparable_comp_spec a a) as [H | H | H]. 1: reflexivity. all: now apply StrictOrder_Irreflexive in H. Qed.
imports: Coq(Relations RelationClasses Setoid)