proposition: Lemma f_finv_in : {in S, cancel finv f}.
proof: Proof. move=> x xS; move: (looping_order x) (orbit_uniq x). rewrite /looping /orbit -orderSpred looping_uniq /= /looping; set n := _.-1. case/predU1P=> // /trajectP[i lt_i_n]; rewrite -iterSr. by move=> /injf ->; rewrite ?(iter_in _ f_in) //; case/trajectP; exists i. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)