proposition: Lemma subcycle_get_arc x p s : x \in s -> uniq s -> subcycle p s -> 1 < size p -> exists2 z, z \in p & x \in arc s z (next p z).
proof: Proof. wlog [s' -> _ {s}] : s / exists s', s = x::s'. { move=> W x_s uniq_s sub_p_s size_p; have [i s' rot_i] := rot_to x_s. case: (W (rot i s)); rewrite ?mem_rot ?rot_uniq ?subcycle_rot_r //; first by exists s'. move=> z z_p; rewrite arc_rot ?(mem_subcycle sub_p_s) //; by exists z. } move=> uniq_s sub_p_s size_p. have uniq_p : uniq p by apply: subcycle_uniq uniq_s. have [x_p|xNp] := boolP (x \in p). - exists x; rewrite ?head_arc ?mem_head //; first exact: next_neq. apply: mem_subcycle sub_p_s _ _. by rewrite mem_next. - have has_p : has (mem p) s'. { case: p => [//|z p] in size_p sub_p_s uniq_p xNp *. apply/hasP; exists z; rewrite /= ?mem_head //. move:(mem_subcycle sub_p_s) => /(_ z (mem_head _ _)) /predU1P [zx|//]. by rewrite zx inE eqxx in xNp. } case def_s : _ _ _ _ / (split_find_nth x has_p) => [/= nz s1 s2 nz_p Ns2]. pose z := path.prev p nz. have z_s2 : z \in s2. { have z_p : z \in p by rewrite path.mem_prev. move:(mem_subcycle sub_p_s z_p); rewrite inE => /predU1P[zx|]. by subst; contrab. rewrite def_s. rewrite mem_cat mem_rcons inE eq_sym (negbTE (prev_neq _ _ _)) //=. by case/orP => [z_s1|//]; apply: contraNT Ns2 => _; apply/hasP; exists z. } exists z; rewrite ?path.mem_prev // next_prev // -cats1 -catA /=. case def_s2 : _ / (path.splitPr z_s2) => [p1 p2]. have U1 : uniq (x :: s1 ++ nz :: p1 ++ z :: p2). { by rewrite -def_s2 -[nz :: _]cat1s catA cats1 -def_s. } move: (U1). rewrite -cat_cons -(rot_uniq (size (x :: s1))) rot_size_cat => U2. rewrite -cat_cons -(arc_rot (size (x :: s1))) // ?rot_size_cat ?(inE,mem_cat,eqxx,orbT)//. have E : ((nz :: p1) ++ z :: p2) ++ x :: s1 = nz :: p1 ++ z :: (p2 ++ x :: s1). { by rewrite /= -!cat_cons -!catA. } by rewrite E right_arc -?E// !(inE,mem_cat) eqxx /= !orbT. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)