proposition: Lemma looping_order x : looping f x (order x).
proof: Proof. apply: contraFT (ltnn (order x)); rewrite -looping_uniq => /card_uniqP. rewrite size_traject => <-; apply: subset_leq_card. by apply/subsetP=> _ /trajectP[i _ ->]; apply: fconnect_iter. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)