proposition: Lemma subcent_char G H K : H \char G -> K \char G -> 'C_H(K) \char G.
proof: Proof. case/charP=> sHG chHG /charP[sKG chKG]; apply/charP. split=> [|f injf Gf]; first by rewrite subIset ?sHG. by rewrite injm_subcent ?chHG ?chKG. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient action gproduct gfunctor) mathcomp(cyclic)