proposition: Lemma Frobenius_trivg_cent : 'C_K(H) = 1.
proof: Proof. by apply: (cent_semiregular Frobenius_reg_ker); case: Frobenius_context. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div) mathcomp(fintype bigop prime finset fingroup morphism) mathcomp(perm action quotient gproduct cyclic center) mathcomp(pgroup nilpotent sylow hall abelian)