proposition: Lemma mem_lcoset A x y : (y \in x *: A) = (x^-1 * y \in A).
proof: Proof. by rewrite -lcosetE [_ x](can_imset_pre _ (mulKg _)) inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)