proposition: Lemma prod_of_rel_P r r' a b: related (prod_of_relation r r') a b <-> [/\ pairp a, pairp b, related r (P a) (P b) & related r' (Q a) (Q b)].
proof: Proof. rewrite /related /prod_of_relation; split. by move /graph_on_P0 => [] /setX_P [pa _ _] /setX_P [pb _ _] [pc pd]. move => [pa pb pc pd]; apply /graph_on_P0;split => //; apply/setX_P; split => //; substr_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)