proposition: Lemma porbit_traject s x : porbit s x =i traject s x #|porbit s x|.
proof: Proof. apply: fsym; apply/subset_cardP. by rewrite (card_uniqP _) ?size_traject ?uniq_traject_porbit. by apply/subsetP=> _ /trajectP[i _ ->]; rewrite -permX mem_porbit. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)