proposition: Lemma right_directedP r: right_directed r <-> (order r /\ right_directed_prop r).
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)