proposition: Lemma val_quotient A : val @: (A / H) = rcosets H 'N_A(H).
proof: Proof. apply/setP=> B; apply/imsetP/rcosetsP=> [[xbar Axbar]|[x /setIP[Ax Nx]]] ->{B}. case/morphimP: Axbar => x Nx Ax ->{xbar}. by exists x; [rewrite inE Ax | rewrite /= val_coset]. by exists (coset H x); [apply/morphimP; exists x | rewrite /= val_coset]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)