proposition: Lemma min_comm (a b: A): min a b = min b a.
proof: Proof. unfold min. pose proof (comparable_comp_spec a b) as [Hab | Hab | Hab]; pose proof (comparable_comp_spec b a) as [Hba | Hba | Hba]. 5,9: now apply lt_not_gt in Hab. all: easy. Qed.
imports: Coq(Relations RelationClasses Setoid)