proposition: Lemma iter_porbit s x : iter #|porbit s x| s x = x.
proof: Proof. case def_n: #|_| (uniq_traject_porbit s x) => [//|n] Ut. have: looping s x n.+1. by rewrite -def_n -[looping _ _ _]porbit_traject -permX mem_porbit. rewrite /looping => /trajectP[[|i] //= lt_i_n /perm_inj eq_i_n_sx]. move: lt_i_n; rewrite ltnS ltn_neqAle andbC => /andP[le_i_n /negP[]]. by rewrite -(nth_uniq x _ _ Ut) ?size_traject ?nth_traject // eq_i_n_sx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)