proposition: Lemma findex_next_other (x y : T) : x \in p -> y \in p -> x != y -> findex (next s) x (next p x) <= findex (next s) x y.
proof: Proof. move=> x_p y_p xDy; have x_s : x \in s by apply: p_in_s. have [n s' rot_n] := rot_to x_s. under eq_findex => z do rewrite -(next_rot n) //. under [X in _ <= X]eq_findex => z do rewrite -(next_rot n) //. have uniq_xs : uniq (x :: s') by rewrite -rot_n rot_uniq. have [m _ sub] := subseq_rot n p_sub_s. rewrite rot_n !findex_head // -(next_rot m) //; rewrite rot_n in sub. have [p' P] : exists p', rot m p = x :: p'. { rewrite -(mem_rot m) in x_p; rewrite -(rot_uniq m) in (uniq_p). case: (splitPr x_p) sub => p1 p2. rewrite -[x::s']cat0s. rewrite uniq_subseq_pivot // => /andP. by rewrite subseq0 => -[/eqP -> _]; exists p2. } rewrite P next_nth mem_head index_head. case: p' P => [|y' p' P]; first by rewrite /= eqxx leq0n. rewrite [nth _ _ _]/= P in sub *; apply: index_subseq sub _ _ => //. by rewrite -P mem_rot. by rewrite /= eqxx (negbTE xDy); case: (x == y'). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)