proposition: Lemma Exercise1_11a r: complete_lattice r -> (has_greatest r /\ has_least r).
proof: Proof. move=> [or cl]. have es:(sub emptyset (substrate r)) by fprops. move: (cl _ es) => [[x xse] [y yie]]. move: xse; rewrite (lub_set0 or) => xse. move: yie; rewrite (glb_set0 or) => yie. by split; [ exists y | exists x]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)