proposition: Lemma compare_reflect (a b: A): match compare a b with | Lt => lt a b | Eq => a = b | Gt => lt b a end.
proof: Proof. pose proof (comparable_comp_spec a b) as [Heq | Hlt | Hgt]; assumption. Qed.
imports: Coq(Relations RelationClasses Setoid)