proposition: Lemma class_sub_norm G A x : G \subset 'N(A) -> (x ^: G \subset A) = (x \in A).
proof: Proof. move=> nAG; apply/subsetP/idP=> [-> // | Ax xy]; first exact: class_refl. by case/imsetP=> y Gy ->; rewrite memJ_norm ?(subsetP nAG). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)