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