proposition: Lemma transfer_indep X (rX := transversal_repr 1 X) : is_transversal X HG G -> {in G, transfer =1 V rX}.
proof: Proof. move=> trX g Gg; have mem_rX := repr_mem_pblock trX 1; rewrite -/rX in mem_rX. apply: (addrI (\sum_(Hx in HG) fmalpha (repr Hx * (rX Hx)^-1))). rewrite {1}(reindex_acts 'Rs _ Gg) ?actsRs_rcosets // -!big_split /=. apply: eq_bigr => _ /rcosetsP[x Gx ->]; rewrite !rcosetE -!rcosetM. case: repr_rcosetP => h1 Hh1; case: repr_rcosetP => h2 Hh2. have: H :* (x * g) \in rcosets H G by rewrite -rcosetE imset_f ?groupM. have: H :* x \in rcosets H G by rewrite -rcosetE imset_f. case/mem_rX/rcosetP=> h3 Hh3 -> /mem_rX/rcosetP[h4 Hh4 ->]. rewrite -!(mulgA h1) -!(mulgA h2) -!(mulgA h3) !(mulKVg, invMg). by rewrite addrC -!zmodMgE -!morphM ?groupM ?groupV // -!mulgA !mulKg. 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)