proposition: Lemma subcycle_get_arc' (T : eqType) x (p s : seq T) : 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. move=> x_s uniq_s sub_p_s le2p. have mem_s := mem_subcycle sub_p_s. have uniq_p : uniq p by apply: subcycle_uniq uniq_s. have /ex_minnP [n iter_n min_n] : exists n, iter n (prev s) x \in p. move/leqW : le2p; rewrite ltnS -has_predT => /hasP [z z_p _]. have [n /eqP it_n] := next_iter uniq_s (mem_s _ z_p) x_s. by exists n; rewrite -it_n iterK //; exact: prev_next. set z := iter n _ _ in iter_n *; exists z => //. have [z_s nz_s] : z \in s /\ next p z \in s by rewrite ?mem_s // ?mem_next. apply/arc_iterP; rewrite ?next_neq //. have /ex_minnP [m /eqP iter_m min_m] := next_iter uniq_s z_s nz_s. exists n => [|n'] ; first exact/iterK/next_prev. apply: contraTN => /min_m => le_m_n'. rewrite -ltnNge. apply: leq_trans le_m_n' => {n'}. apply: wlog_neg; rewrite -ltnNge => gt_m_n. have gt0m : 0 < m. { by rewrite lt0n; apply: contra_eq_neq iter_m => -> /=; apply: next_neq. } have gt0n : 0 < n by apply: leq_trans gt0m _. have/min_n : iter (n - m) (prev s) x \in p. { have En : n = m + (n - m) by rewrite subnKC. move: iter_n. rewrite -mem_next -iter_m /z {1}En iterD iterK //. exact: next_prev. } by rewrite leqNgt ltn_subrL gt0m gt0n. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)