proposition: Lemma pidl_directed_bis: nonempty I1 -> nonempty I2 -> right_directed_prop (prod_of_relation r1 r2) -> right_directed_prop r1 /\ right_directed_prop r2.
proof: Proof. move:pidl_or => [orp srp]. move => [a aiI] [b bI2] h; split => x y xsr ysr. have jxbs : inc (J x b) (substrate ((prod_of_relation r1 r2))). rewrite srp - sr1; fprops. have jybs : inc (J y b) (substrate ((prod_of_relation r1 r2))). rewrite srp - sr1; fprops. move:(h _ _ jxbs jybs) => [z [/pidl_gleP [_ _ za _] /pidl_gleP [_ _ zb _]]]. by move: za zb; aw => za zb; exists (P z). have jxbs : inc (J a x) (substrate ((prod_of_relation r1 r2))). rewrite srp - sr2; fprops. have jybs : inc (J a y) (substrate ((prod_of_relation r1 r2))). rewrite srp - sr2; fprops. move:(h _ _ jxbs jybs) => [z [/pidl_gleP [_ _ _ za] /pidl_gleP [_ _ _ zb]]]. by move: za zb; aw => za zb; exists (Q z). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)