proposition: Lemma arc_iterP (T : eqType) (x y z : T) (s : seq T) (xDy : x != y) : uniq s -> x \in s -> y \in s -> reflect (exists2 n, iter n (next s) x = z & forall m, m <= n -> iter m (next s) x != y) (z \in arc s x y).
proof: Proof. move=> uniq_s x_s y_s. have [i s1 s2 arc1 arc2 rot_i] := rot_to_arc uniq_s x_s y_s xDy. have I k (lt_k_s : k < size (rot i s)) : iter k (next s) x = nth x (rot i s) k. { have -> : x = head z (rot i s) by rewrite rot_i. under eq_iter => u do rewrite -(next_rot i) //. by rewrite iter_next_nth // ?rot_uniq // (set_nth_default z). } have yNarc1 : y \notin arc s x y. { apply: contraTN uniq_s; rewrite -(rot_uniq i) rot_i -cat_cons arc1 cat_uniq. move=> y_arc1; rewrite [has _ _](_ : _ = true) ?andbF //. by apply/hasP; exists y => //=; apply: mem_head. } apply: (iffP idP) => [z_arc1|[n iter_n min_n]]. - have z_s := mem_arc z_arc1; exists (index z (rot i s)) => [|m lt_m_z]. rewrite I ?nth_index // ?mem_rot // index_mem. by rewrite rot_i -cat_cons arc1 mem_cat z_arc1. have lt_m_a1 : m < size (arc s x y). { apply: leq_ltn_trans lt_m_z _. by rewrite rot_i -cat_cons arc1 index_cat z_arc1 index_mem. } have m_lt_s : m < size (rot i s). by apply: leq_trans lt_m_a1 _; rewrite rot_i -cat_cons arc1 size_cat leq_addr. apply: contraNneq yNarc1; rewrite I // => {1}<-. by rewrite rot_i -cat_cons arc1 nth_cat lt_m_a1 mem_nth. - pose k := index y (rot i s); have lt_k_s : k < size (rot i s). by rewrite index_mem rot_i !(inE,mem_cat) eqxx !orbT. have lt_n_k : n < k. rewrite ltnNge; apply/negP=> /min_n. by rewrite I // nth_index ?eqxx // rot_i !(inE,mem_cat) eqxx !orbT. rewrite -iter_n I ?(ltn_trans lt_n_k lt_k_s) // rot_i -cat_cons arc1 nth_cat. suff eq_k : k = size (arc s x y) by rewrite -eq_k lt_n_k mem_nth // -eq_k. by rewrite /k rot_i -cat_cons arc1 index_cat (negbTE yNarc1) /= ?eqxx ?addn0. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)