proposition: Lemma pidl_directed: right_directed_prop r1 -> right_directed_prop r2 -> right_directed_prop (prod_of_relation r1 r2).
proof: Proof. move => dr1 dr2 x y; rewrite (order_product2_sr1 or1 or2). move => /setX_P [px Px Qx] /setX_P [py Py Qy]. move:(dr1 _ _ Px Py) (dr2 _ _ Qx Qy)=> [a [pa pb]] [b [pc pd]]. exists (J a b);split; apply/pidl_gleP;aw; split; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)