proposition: Lemma decomposable_ext_to_prod_rel r r': equivalence r -> equivalence r' -> exists h, [/\ bijection h, source h = quotient (prod_of_relation r r'), target h = (quotient r) \times (quotient r') & h \co (canon_proj (prod_of_relation r r')) = ext_to_prod(canon_proj r)(canon_proj r')].
proof: Proof. move=> er er'. set (r'':=prod_of_relation r r'). set (f'':=ext_to_prod (canon_proj r) (canon_proj r')). set (h:=fun_on_quotient r'' f''). have er'': equivalence r'' by rewrite /r''; apply: equivalence_prod_of_rel. have co: compatible_with_equiv f'' r''. rewrite /f'' /r''; apply: compatible_ext_to_prod=>//. move :(compose_foq_proj er'' co); rewrite -/h => cop. have sh: source h = quotient r''. by rewrite /h /fun_on_quotient/section_canon_proj; aw. have th: target h = (quotient r) \times (quotient r'). by rewrite /h/fun_on_quotient/ f'' /ext_to_prod; aw. have fh: function h. rewrite /h /f''; apply: foqc_f =>//. apply: ext_to_prod_f; fprops. by rewrite /r'' substrate_prod_of_rel // /ext_to_prod; aw. have ff'': function f'' by rewrite /f''; apply: ext_to_prod_rel_f. have sf'': source f'' = substrate r''. by rewrite /f'' /r''/ext_to_prod substrate_prod_of_rel; aw. have ih: injection h. split=>//. move=> x y; rewrite sh /h => xs ys. rewrite foqc_V // foqc_V //. move: (rep_i_sr er'' xs)(rep_i_sr er'' ys). rewrite substrate_prod_of_rel //. move=> /setX_P [px Px Qx] /setX_P [py Py Qy] WW. move: (compatible_ext_to_prod_inv er er' px Px Qx py Py Qy WW). by move/(related_rr_P er'' xs ys). exists h;split => //;split =>//;split =>//. move=> y; rewrite th; move /setX_P=> [py Py Qy]. have p1: (inc (J (rep (P y)) (rep (Q y))) (substrate r'')). rewrite /r'' substrate_prod_of_rel //;apply:setXp_i; fprops. set (x:= class r'' (J (rep (P y)) (rep (Q y)))). have xq: inc x (quotient r'') by rewrite /x; fprops. have rxs: inc (rep x) (substrate r'') by fprops. move: (related_rep_class er'' p1). move: rxs; rewrite substrate_prod_of_rel //; move /setX_P => [ pr Pr Qr]. move: p1; rewrite substrate_prod_of_rel //; move /setXp_P=> [Py' Qy']. rewrite -/x; move /(related_prod_of_relP1)=> [u [v [e1 e2 e3]]]. exists x; rewrite ?sh // /h foqc_V //- pr - py /f'' ext_to_prod_rel_V //. have <-: (P y = class r (P (rep x))). apply: is_class_pr =>//; rewrite e1; aw. by move:Py => /(setQ_P er) [_ ->]; apply /(class_P er). have <- //: (Q y = class r' (Q (rep x))) . apply: is_class_pr =>//; rewrite e1; aw. by move:Qy => /(setQ_P er') [_ ->]; apply /(class_P er'). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)