fact: Definition fin_prodPCMMixin := PCMMixin ujoinC_fin ujoinA_fin uunitL_fin uvalidL_fin uvalidU_fin.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)