proposition: Lemma related_ext_to_prod_rel r r': equivalence r -> equivalence r' -> equivalence_associated (ext_to_prod(canon_proj r)(canon_proj r')) = prod_of_relation r r'.
proof: Proof. move=> er er'. move:(compatible_ext_to_prod er er')=> [fe se re]. have eq: equivalence (prod_of_relation r r') by apply: equivalence_prod_of_rel. have eq' := proj1(graph_ea_equivalence fe). apply: sgraph_exten; fprops. have f1: function (canon_proj r) by fprops. have f2: function (canon_proj r') by fprops. move=> u v; split. move /(ea_relatedP fe) => []. rewrite {1 2} /ext_to_prod lf_source. move /setX_P => [up Pu Qu] /setX_P [vp Pv Qv]. have r1: (J (P u)(Q u) = u) by aw. have r2: (J (P v)(Q v) = v) by aw. rewrite -r1 -r2 ext_to_prod_V // ext_to_prod_V //. move: Pu Qu Pv Qv; rewrite 2! canon_proj_s => Pu Qu Pv Qv. rewrite !canon_proj_V // => neq. move: (pr1_def neq) (pr2_def neq)=> eq1 eq2. by apply /prod_of_rel_P;split; fprops; aw; apply/related_equiv_P. move /prod_of_rel_P => [pu pv] /(related_equiv_P er)[Pu Pv c1] /(related_equiv_P er') [Qu Qv c2]. apply /(ea_relatedP fe); split. by rewrite /ext_to_prod lf_source; aw;apply/setX_P. by rewrite /ext_to_prod lf_source; aw;apply/setX_P. by apply: re; apply/prod_of_rel_P; split => //; apply /(related_equiv_P). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)