proposition: Lemma ker_coset_prim : 'ker coset = 'N_H(A).
proof: Proof. apply/setP=> z; rewrite !in_setI andbC 2!inE -val_eqE /=. case Nz: (z \in 'N(A)); rewrite ?andbF ?val_coset_prim // !andbT. by apply/eqP/idP=> [<-| Az]; rewrite (rcoset_refl, rcoset_id). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)