proposition: Theorem right_directed_maximal r x: right_directed r -> maximal r x -> greatest r x.
proof: Proof. move=> rr [xsr ma]; split=>// t ts. move /right_directedP:rr => [or rr]. by move:(rr _ _ xsr ts) => [z [xz tz]]; rewrite - (ma _ xz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)