proposition: Lemma popc_axioms: lf_axiom(fun w => prod_of_fgraph (P w) (Q w)) ((productb (graph f)) \times (productb (graph f'))) (productb (graph (prod_of_products f f'))).
proof: Proof. move=> x xd /=. by move/setX_P: xd => [pxd px qx]; apply: prod_of_function_f. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)