proposition: Lemma ex4_no_greater x: inc x I -> exists y, glt r x y.
proof: Proof. move => xI. move: ex4H => [neI or sr rdr noge]. move/right_directedP: rdr => [_];rewrite / right_directed_prop sr => h. case: (p_or_not_p (exists2 y, inc y I & ~(gle r y x))). move => [y yI nxy]; move:(h _ _ xI yI) =>[z [ qa qb]]. by exists z; split => // exz; case: nxy; rewrite exz. move => dy;case (noge _ xI); rewrite /greatest sr; split => // y yI. by ex_middle bad; case dy; exists y. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)