proposition: Lemma remgr_id x : x \in H -> remgr K H x = x.
proof: Proof. move=> Hx; apply/eqP; rewrite eq_mulgV1 (sameP eqP set1gP) -tiKH inE. rewrite -mem_rcoset groupMr ?groupV // -in_setI remgrP. by apply: subsetP Hx; apply: mulG_subr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)