proposition: Lemma le_min_a (a b: A): le (min a b) a.
proof: Proof. unfold min. pose proof (comparable_comp_spec a b) as [Heq | Hlt | Hgt]; subst. 1,2: now apply le_refl. now apply lt_incl_le. Qed.
imports: Coq(Relations RelationClasses Setoid)