proposition: Lemma lcosetsP A B C : reflect (exists2 x, x \in B & C = x *: A) (C \in lcosets A B).
proof: Proof. by apply: (iffP imsetP) => [] [x Bx ->]; exists x; rewrite ?lcosetE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)