proposition: Lemma transferM : {in G &, {morph transfer : x y / (x * y)%g >-> x + y}}.
proof: Proof. move=> s t Gs Gt /=. rewrite [transfer t](reindex_acts 'Rs _ Gs) ?actsRs_rcosets //= -big_split /=. apply: eq_bigr => _ /rcosetsP[x Gx ->]; rewrite !rcosetE -!rcosetM. rewrite -zmodMgE -morphM -?mem_rcoset; first by rewrite !mulgA mulgKV rcosetM. by rewrite rcoset_repr rcosetM mem_rcoset mulgK mem_repr_rcoset. by rewrite rcoset_repr (rcosetM _ _ t) mem_rcoset mulgK mem_repr_rcoset. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype bigop ssralg finset fingroup) mathcomp(morphism perm finalg action gproduct commutator) mathcomp(cyclic)