proposition: Lemma compatible_ext_to_prod_inv r r' x x': equivalence r -> equivalence r' -> pairp x -> inc (P x) (substrate r) -> inc (Q x) (substrate r') -> pairp x' -> inc (P x') (substrate r) -> inc (Q x') (substrate r') -> Vf (ext_to_prod (canon_proj r) (canon_proj r')) x = Vf (ext_to_prod (canon_proj r) (canon_proj r')) x' -> related (prod_of_relation r r') x x'.
proof: Proof. move=> er er' px Px Qx px' Px' Qx'. have p1: (J (P x) (Q x) = x) by aw. have p2: (J (P x') (Q x') = x') by aw. rewrite -p1 -p2 ext_to_prod_rel_V // ext_to_prod_rel_V // => Jeq. move: (pr1_def Jeq) (pr2_def Jeq)=> eq1 eq2. by apply/prod_of_rel_P; aw; split; fprops; apply/related_equiv_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)