proposition: Lemma orbit_uniq x : uniq (orbit x).
proof: Proof. rewrite /orbit -orderSpred looping_uniq; set n := (order x).-1. apply: contraFN (ltnn n) => /trajectP[i lt_i_n eq_fnx_fix]. rewrite orderSpred -(size_traject f x n). apply: (leq_trans (subset_leq_card _) (card_size _)); apply/subsetP=> z. rewrite inE fconnect_orbit => /trajectP[j le_jn ->{z}]. rewrite -orderSpred -/n ltnS leq_eqVlt in le_jn. by apply/trajectP; case/predU1P: le_jn => [->|]; [exists i | exists j]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)