proposition: Lemma compatible_ext_to_prod r r': equivalence r -> equivalence r' -> compatible_with_equiv (ext_to_prod (canon_proj r) (canon_proj r')) (prod_of_relation r r').
proof: Proof. move=> er er'. have fc: function (canon_proj r) by fprops. have fc': function (canon_proj r') by fprops. split; first by apply: ext_to_prod_f. by rewrite substrate_prod_of_rel // /ext_to_prod; aw. move=> x x'. move /prod_of_rel_P=> [px px']. move/(related_equiv_P er) => [pxs qx cx] /(related_equiv_P er') [pys qy cy]. have q1: (J (P x)(Q x) = x) by aw. have q2: (J (P x')(Q x') = x') by aw. rewrite -q1 -q2 ! ext_to_prod_V //; aw; trivial. by rewrite ! canon_proj_V // cx cy. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)