proposition: Lemma coset_mem y xbar : y \in xbar -> coset y = xbar.
proof: Proof. case: xbar => /= Hx NHx Hxy; apply: val_inj=> /=. case/rcosetsP: NHx (NHx) Hxy => x Nx -> NHx Hxy. by rewrite val_insubd /= (rcoset_eqP Hxy) NHx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)