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