proposition: Lemma remgrMl K B x y : y \in K -> remgr K B (y * x) = remgr K B x.
proof: Proof. by move=> Ky; rewrite {1}/remgr rcosetM rcoset_id. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)