proposition: Lemma cosetP xbar : {x | x \in 'N(A) & xbar = coset x}.
proof: Proof. pose x := repr 'N_xbar(A). have [xbar_x Nx]: x \in xbar /\ x \in 'N(A). apply/setIP; rewrite {}/x; case: xbar => /= _ /rcosetsP[y Ny ->]. by apply: (mem_repr y); rewrite inE rcoset_refl. by exists x; last rewrite (coset_mem xbar_x). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)