proposition: Lemma norm_normalI G A : G \subset 'N(A) -> G :&: A <| G.
proof: Proof. by move=> nAG; rewrite /normal subsetIl normsI ?normG. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)