proposition: Lemma cycle_prev : cycle (fun x y => x == prev p y) p.
proof: Proof. apply: etrans cycle_next; symmetry; case def_p: p => [|x q] //. by apply: eq_path; rewrite -def_p; apply: (can2_eq prev_next next_prev). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)