proposition: Lemma looping_uniq x n : uniq (traject f x n.+1) = ~~ looping x n.
proof: Proof. rewrite /looping; elim: n x => [|n IHn] x //. rewrite [n.+1 in LHS]lock [iter]lock /= -!lock {}IHn -iterSr -negb_or inE. congr (~~ _); apply: orb_id2r => /trajectP no_loop. apply/idP/eqP => [/trajectP[m le_m_n def_x] | {1}<-]; last first. by rewrite iterSr -last_traject mem_last. have loop_m: looping x m.+1 by rewrite /looping iterSr -def_x mem_head. have/trajectP[[|i] // le_i_m def_fn1x] := loopingP _ _ loop_m n.+1. by case: no_loop; exists i; rewrite -?iterSr // -ltnS (leq_trans le_i_m). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)