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