proposition: Lemma quotient_sub1 A : A \subset 'N(H) -> (A / H \subset [1]) = (A \subset H).
proof: Proof. by move=> nHA /=; rewrite -[gval H in RHS]ker_coset ker_trivg_morphim nHA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)