proposition: Lemma arc_next (T : eqType) (s : seq T) (x : T) : 1 < size s -> uniq s -> x \in s -> arc s x (next s x) = [:: x].
proof: Proof. move=> le2s uniq_s x_s. have xDnx : x != next s x by apply: next_neq. have nx_s : next s x \in s by rewrite mem_next. have [i s1 s2 A1 A2 rot_i] := rot_to_arc uniq_s x_s nx_s xDnx. suff s1nil : s1 = [::] by rewrite -A1 s1nil. move: (uniq_s); rewrite -(rot_uniq i) rot_i -(next_rot i) // rot_i (next_cons x). by case: s1 {A1 A2 rot_i} => //= y s1'; rewrite !(inE,mem_cat) eqxx orbT andbF. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)