proposition: Lemma pcore_faithful_irr_act G M : p.-group M -> M \subset R -> acts_irreducibly G M to -> [faithful G, on M | to] -> 'O_p(G) = 1.
proof: Proof. move=> pM sMR irrG ffulG; apply/trivgP; apply: subset_trans ffulG. exact: pcore_sub_astab_irr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype prime bigop finset fingroup morphism) mathcomp(automorphism quotient action cyclic gproduct) mathcomp(gfunctor commutator pgroup center nilpotent)