proposition: Lemma cent_joinEr G H : H \subset 'C(G) -> G <*> H = G * H.
proof: Proof. by move=> cGH; apply: norm_joinEr (cents_norm cGH). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)