proposition: Lemma popc_target_aux: productb(Lg (domain (graph f)) (fun i => (Vg (graph f) i) \times (Vg (graph f') i))) = productb (graph (prod_of_products f f')).
proof: Proof. congr (productb _). move: (prod_of_products_f f f') => fp. apply: fgraph_exten; fprops; aw; rewrite !domain_fg //. by rewrite lf_source. move=> x xd; rewrite LgV //. symmetry; exact: (prod_of_products_V f' xd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)