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