proposition: Lemma related_prod_of_relP2 r r' x x' v: (related (prod_of_relation r r') (J x x') v <-> inc v ((im_of_singleton r x) \times (im_of_singleton r' x'))).
proof: Proof. split. move=> /related_prod_of_relP1 [y [y' [eq r1 r2]]]; rewrite eq. by apply/setXp_i; apply /dirim_set1_P. move /setX_P => [pv /dirim_set1_P j1r /dirim_set1_P j2r]. by apply/related_prod_of_relP1;exists (P v); exists (Q v);aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)