proposition: Lemma cycle_next : fcycle (next p) p.
proof: Proof. case def_p: p Up => [|x q] Uq //; rewrite -[in next _]def_p. apply/(pathP x)=> i; rewrite size_rcons => le_i_q. rewrite -cats1 -cat_cons nth_cat le_i_q /= next_nth {}def_p mem_nth //. rewrite index_uniq // nth_cat /= ltn_neqAle andbC -ltnS le_i_q. by case: (i =P _) => //= ->; rewrite subnn nth_default. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)