proposition: Lemma Exercise4_7c1: exists a, greatest r a.
proof: Proof. move: (finite_set_maximal1 (@sub_refl (substrate r)) nes). move=> [x xsr xp]; exists x;split => //. move=> u usr; move: (lattice_sup_pr lr usr xsr); move=> [p1 p2 p3]. move: lr => [or _]. have isr:inc (sup r u x) (substrate r) by order_tac. by move: (xp _ isr p2) => aux; rewrite - aux in p1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)