proposition: Lemma next_cycle p x : cycle e p -> x \in p -> e x (next p x).
proof: Proof. case: p => //= y0 p; elim: p {1 3 5}y0 => [|z p IHp] y /=; rewrite inE. by rewrite andbT; case: (x =P y) => // ->. by case/andP=> eyz /IHp; case: (x =P y) => // ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)