proposition: Lemma norm_conj_norm x A B : x \in 'N(A) -> (A \subset 'N(B :^ x)) = (A \subset 'N(B)).
proof: Proof. by move=> Nx; rewrite normJ -sub_conjgV (normP _) ?groupV. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)