proposition: Lemma mulg_exp_card_rcosets x : x * (g ^+ n_ x) \in H :* x.
proof: Proof. rewrite /n_ /indexg -orbitRs -porbit_actperm ?inE //. rewrite -{2}(iter_porbit (actperm 'Rs g) (H :* x)) -permX -morphX ?inE //. by rewrite actpermE //= rcosetE -rcosetM rcoset_refl. 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)