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