proposition: Lemma related_prod_of_relP1 r r' x x' v: related (prod_of_relation r r') (J x x') v <-> (exists y y', [/\ v = J y y', related r x y & related r' x' y']).
proof: Proof. split. move /prod_of_rel_P; aw; move=> [_ pb pc pd]. by exists (P v); exists (Q v). move=> [y [y' [eq r1 r2]]]; rewrite eq; apply /prod_of_rel_P; aw; split; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)