proposition: Lemma remgrP K B x : (remgr K B x \in K :* x :&: B) = (x \in K * B).
proof: Proof. set y := _ x; apply/idP/mulsgP=> [|[g b Kg Bb x_gb]]. rewrite inE rcoset_sym mem_rcoset => /andP[Kxy' By]. by exists (x * y^-1) y; rewrite ?mulgKV. by apply: (mem_repr b); rewrite inE rcoset_sym mem_rcoset x_gb mulgK Kg. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)