fact: Definition prod7PCMMixin := PCMMixin ujoinC7 ujoinA7 uunitL7 uvalidL7 uvalidU7.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)