proposition: Lemma rcosets_cycle_transversal : H_g_rcosets @: X = HGg.
proof: Proof. have sHXgHGg x: x \in X -> H_g_rcosets x \in HGg. by move/sXG=> Gx; apply: imset_f; rewrite -rcosetE imset_f. apply/setP=> Hxg; apply/imsetP/idP=> [[x /sHXgHGg HGgHxg -> //] | HGgHxg]. have [_ /rcosetsP[z Gz ->] ->] := imsetP HGgHxg. pose Hzg := H :* z * <[g]>; pose x := transversal_repr 1 X Hzg. have HGgHzg: Hzg \in HG :* <[g]>. by rewrite mem_mulg ?set11 // -rcosetE imset_f. have Hzg_x: x \in Hzg by rewrite (repr_mem_pblock trX). exists x; first by rewrite (repr_mem_transversal trX). case/mulsgP: Hzg_x => y u /rcoset_eqP <- /(orbit_act 'Rs) <- -> /=. by rewrite rcosetE -rcosetM. 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)