proposition: Lemma lcoset_eqP {x y} : reflect (x *: G = y *: G) (x \in y *: G).
proof: Proof. suffices <-: (x *: G == y *: G) = (x \in y *: G) by apply: eqP. by rewrite eqEsubset !mulSG !sub1set lcoset_sym andbb. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)