proposition: Lemma popc_fb: bijection (prod_of_products_canon (graph f) (graph f')).
proof: Proof. move: (domain_fg ff) (domain_fg ff') => fa f'a. apply: lf_bijective. - by rewrite/productf popc_target_aux //; apply: popc_axioms. - move => x y xs ys sv. move: (xs)(ys) => /setX_P [xp px qx] /setX_P [yp py qy]. have sj: forall i, inc i (source f) -> J (Vg (P x) i) (Vg (Q x) i) = J (Vg (P y) i) (Vg (Q y) i). move => j js. by rewrite -(prod_of_function_V px qx js) -(prod_of_function_V py qy js) sv. apply: pair_exten => //. apply: (setXb_exten px py). move => i; rewrite fa => js; exact: (pr1_def (sj _ js)). apply: (setXb_exten qx qy). move => i; rewrite f'a - sfsf => js;exact: (pr2_def (sj _ js)). - rewrite /productf popc_target_aux => y. move: (prod_of_products_f f f') => fc. move /setXb_P=> [fy]; rewrite domain_fg //; rewrite lf_source => pa pb. set xa:= Lf (fun i => P (Vg y i)) (source f)(union (target f)). set xb:= Lf (fun i => Q (Vg y i)) (source f)(union (target f')). have ta: lf_axiom (fun i => P (Vg y i)) (source f) (union (target f)). move=> t tf /=; move:(pb _ tf); rewrite -/(Vf _ _) (prod_of_products_V f' tf). move/setX_P => [_ iP _]; apply: (@setU_i _ (Vf f t)) => //; Wtac. have tb: lf_axiom (fun i => Q (Vg y i)) (source f) (union (target f')). move=> t tf /=; move:(pb _ tf); rewrite -/(Vf _ _) (prod_of_products_V f' tf). move/setX_P => [_ _ iQ]; apply: (@setU_i _ (Vf f' t)) => //; Wtac. have fxa: function xa by apply: lf_function. have fxb: function xb by apply: lf_function. have sxa: source xa = source f by rewrite /xa; aw. have sxb: source xb = source f by rewrite /xb; aw. have ixa :inc (graph xa) (productb (graph f)). apply /setXb_P;rewrite fa (domain_fg fxa);split; fprops. move => i isf; rewrite /xa -/(Vf _ _) (LfV ta isf). move: (pb _ isf); rewrite -/(Vf _ _) (prod_of_products_V f' isf). by move/setX_P => [_ ]. have ixb :inc (graph xb) (productb (graph f')). apply /setXb_P;rewrite f'a (domain_fg fxb);split; fprops. by rewrite sxb - sxa - sfsf. rewrite - sfsf; move => i isf; rewrite /xb -/(Vf _ _) (LfV tb isf). move: (pb _ isf); rewrite -/(Vf _ _) (prod_of_products_V f' isf). by move/setX_P => [_ ]. exists (J (graph xa) (graph xb));fprops; aw. rewrite /prod_of_fgraph (domain_fg fxa) lf_source. symmetry;apply: fgraph_exten;fprops; aw; first by ue. move => i isf; rewrite LgV //. rewrite /xa -/(Vf _ _) (LfV ta isf) /xa -/(Vf _ _) (LfV tb isf). move: (pb _ isf); rewrite -/(Vf _ _) (prod_of_products_V f' isf). by move/setX_P => [-> _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)