proposition: Lemma sub_lcoset x A B : (A \subset x *: B) = (x^-1 *: A \subset B).
proof: Proof. by rewrite -(lcosetS x^-1) lcosetK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)