proposition: Lemma lattice_directed r: lattice r -> (right_directed r /\ left_directed r).
proof: Proof. move=> [or lr]; split; split =>// x y xs ys; move: (lr _ _ xs ys)=> [p1 p2]. have sd: sub (doubleton x y) (substrate r) by apply: sub_set2. by move: p1=> [s] /(lubP or sd)[ub _]; exists s. have sd: sub (doubleton x y) (substrate r) by apply: sub_set2. by move: p2=> [s] /(glbP or sd)[ub _] ; exists s. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)