proposition: Lemma arc_subcycle_disjoint (T : finType) (p s : seq T) (x y : T) : uniq s -> subcycle p s -> x \in p -> y \in p -> x != y -> [disjoint arc s x (next p x) & arc s y (next p y)].
proof: Proof. move=> uniq_s /subcycleP [m sub_p_s]. wlog: p {sub_p_s} / subseq p s => [W|?]; last exact: arc_next_disjoint. move: (W _ sub_p_s); rewrite !mem_rot !next_rot // -(rot_uniq m). all: exact: subseq_uniq uniq_s. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)