proposition: Lemma uniq_traject_porbit s x : uniq (traject s x #|porbit s x|).
proof: Proof. case def_n: #|_| => // [n]; rewrite looping_uniq. apply: contraL (card_size (traject s x n)) => /loopingP t_sx. rewrite -ltnNge size_traject -def_n ?subset_leq_card // porbit.unlock. by apply/subsetP=> _ /imsetP[_ /cycleP[i ->] ->]; rewrite /aperm permX t_sx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)