proposition: Lemma setX_right_directed g: order_fam g -> (allf g right_directed) -> right_directed (order_product g).
proof: Proof. move=> pa alri; move: (order_product_osr pa) => [pb pc]. apply/right_directedP; split =>//. move=> x y xs ys. set (z:= Lg (domain g)(fun i => choose (fun w => upper_bound (Vg g i) (doubleton (Vg x i) (Vg y i)) w))). have alu: (forall i, inc i (domain g) -> upper_bound (Vg g i) (doubleton (Vg x i) (Vg y i)) (Vg z i)). move=> i idg; rewrite LgV//. move: xs ys; rewrite pc. move/(prod_of_substratesP) => [_ _ p1] /(prod_of_substratesP)[_ _ p2]. move:(p1 _ idg)(p2 _ idg)=> p3 p4. move: (alri _ idg)=> [t h]; move: (h _ _ p3 p4)=> [b bii]. by apply:choose_pr; exists b. have zs:inc z (substrate (order_product g)). rewrite pc;apply/prod_of_substratesP. split; first by rewrite/z; fprops. by rewrite/z; aw. by move => i idg; move: (alu _ idg); move=> [us ub]; apply: us. move: xs ys zs; rewrite pc => xs ys zs. exists z; split => //;apply /(order_product_gleP); split => //i idg; move: (alu _ idg); move=> [_ h]; apply: h; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)