proposition: Lemma class_prod_of_relP2 r r': equivalence r -> equivalence r' -> forall x, (classp (prod_of_relation r r') x <-> exists u v, [/\ classp r u, classp r' v & x = u \times v]).
proof: Proof. move=> er er'. move:(equivalence_prod_of_rel er er')=> er''. split. move => cx; move: (cx) => [ca cb]. move: (ca); rewrite (substrate_prod_of_rel er er') => /setX_P [pa pb pc]. exists (class r (P (rep x))); exists (class r' (Q (rep x))); split => //. by apply: (class_class er). by apply: (class_class er'). set_extens v. rewrite {1} cb; move /(class_P er'') => /prod_of_rel_P [qa qb qc qd]. apply /setX_P => //; split => //; apply /class_P => //. move /setX_P => [qa qb qc]; rewrite cb; apply /(class_P er''). by apply /prod_of_rel_P;split => //; apply /class_P. move=> [u [v [pa pb pe]]]. move: (pa)(pb) => [pc _] [pd _]. suff : x = class (prod_of_relation r r') (J (rep u) (rep v)). move => ->; apply: (class_class er''). by rewrite (substrate_prod_of_rel er er'); apply:setXp_i. set_extens t. rewrite pe; move => /setX_P [qa qb qc]. apply /(class_P er''); apply /prod_of_rel_P; aw. split; fprops; by apply :rel_in_class. move /(class_P er'') => /prod_of_rel_P; aw; move => [_ qa qb qc]. rewrite pe; apply /setX_P;split => //. apply: (rel_in_class2 er pa qb). apply: (rel_in_class2 er' pb qc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)