proposition: Lemma remgr1 K H x : x \in K -> remgr K H x = 1.
proof: Proof. by move=> Kx; rewrite /remgr rcoset_id ?repr_group. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)