proposition: Lemma pcore_mod1 pi gT (G : {group gT}) : pcore_mod G pi 1 = 'O_pi(G).
proof: Proof. rewrite /pcore_mod; have inj1 := coset1_injm gT; rewrite -injmF ?norms1 //. by rewrite -(morphim_invmE inj1) morphim_invm ?norms1. 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)