proposition: Lemma morphim_pgroup pi G : pi.-group G -> pi.-group (f @* G).
proof: Proof. by apply: pnat_dvd; apply: dvdn_morphim. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup morphism) mathcomp(gfunctor automorphism quotient action gproduct) mathcomp(cyclic)