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