proposition: Lemma inj_cycle : {in p &, injective f}.
proof: Proof. apply: can_in_inj (iter (size p).-1 f) _ => x /rot_to[i q rip]. have /fpathE qxE : fcycle f (x :: q) by rewrite -rip rot_cycle. have -> : size p = size (rcons q x) by rewrite size_rcons -(size_rot i) rip. by rewrite -iterSr -last_traject prednK -?qxE ?size_rcons// last_rcons. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)