proposition: Lemma mem_rcosets A x : (G :* x \in rcosets G A) = (x \in G * A).
proof: Proof. apply/rcosetsP/mulsgP=> [[a Aa /rcoset_eqP/rcosetP[g]] | ]; first by exists g a. by case=> g a Gg Aa ->{x}; exists a; rewrite // rcosetM rcoset_id. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)