fact: Definition pcontinuous := forall gT hT (G D : {group gT}) (phi : {morphism D >-> hT}), phi @* F G \subset F (phi @* G).
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)