proposition: Lemma arc_findex x y z (xDy : x != y) : uniq s -> x \in s -> y \in s -> (z \in arc s x y) = (findex (next s) x z < findex (next s) x y).
proof: Proof. move=> uniq_s x_s y_s; have [i s1 s2 A1 A2 R] := rot_to_arc uniq_s x_s y_s xDy. under eq_findex => u do rewrite -(next_rot i) //. under (@eq_findex _ (next s)) => u do rewrite -(next_rot i) //. have uniq_xy : uniq (x :: s1 ++ y :: s2) by rewrite -R rot_uniq. rewrite R !findex_head // -cat_cons !index_cat index_head. rewrite -A1 [X in _ < X]ifN. by case: ifP => [Hz|_]; rewrite ?ltn_add2l // addn0 index_mem Hz. by apply: contraTN uniq_xy => C; rewrite -cat_cons cat_uniq /= C /= andbF. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)