proposition: Lemma next_mem_arc (T : eqType) (s : seq T) (x y : T) : uniq s -> x \in s -> y \in s -> x != y -> next s x \in rcons (arc s x y) y.
proof: Proof. move=> uniq_s x_s y_s xDy. have [i s1 s2 arc1 arc2 rot_r] := rot_to_arc uniq_s x_s y_s xDy. rewrite -arc1 -(next_rot i) // rot_r (next_cons x). by case: s1 {arc1 rot_r} => [|z s1']; rewrite /= !inE eqxx orbT. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)