proposition: Lemma left_directedP r: left_directed r <-> (order r /\ forall x y, inc x (substrate r) -> inc y (substrate r) -> exists z, gle r z x /\ gle r z y).
proof: Proof. split; move=> [or h]; split=>//. move=> x y xs ys; move: (h _ _ xs ys)=> [t [ts tb]]; exists t; split; fprops. move=> x y xs ys; move: (h _ _ xs ys) => [z [xz yz]]. have zs: inc z (substrate r) by order_tac. by exists z; split =>//; move=> t td; case /set2_P: td => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)