proposition: Lemma cycle_traject x : <[x]> =i traject (mulg x) 1 #[x].
proof: Proof. set t := _ 1; apply: fsym; apply/subset_cardP; last first. by apply/subsetP=> _ /trajectP[i _ ->]; rewrite -iteropE mem_cycle. rewrite (card_uniqP _) ?size_traject //; case def_n: #[_] => // [n]. rewrite looping_uniq; apply: contraL (card_size (t n)) => /loopingP t_xi. rewrite -ltnNge size_traject -def_n ?subset_leq_card //. rewrite -(eq_subset_r (in_set _)) {}/t; set G := finset _. rewrite -[x]mulg1 -[G]gen_set_id ?genS ?sub1set ?inE ?(t_xi 1%N)//. apply/group_setP; split=> [|y z]; rewrite !inE ?(t_xi 0) //. by do 2!case/trajectP=> ? _ ->; rewrite -!iteropE -expgD [x ^+ _]iteropE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)