proposition: Lemma popc_V w: inc w ((productb (graph f)) \times (productb (graph f'))) -> Vf (prod_of_products_canon (graph f) (graph f')) w = prod_of_fgraph (P w) (Q w).
proof: Proof. by move=> h; rewrite LfV // /productf popc_target_aux; apply: popc_axioms. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)