proposition: Lemma mem_lcosets A x : (x *: G \in lcosets G A) = (x \in A * G).
proof: Proof. rewrite -[LHS]memV_invg invg_lcoset invg_lcosets. by rewrite -[RHS]memV_invg invMg invGid mem_rcosets. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)