proposition: Lemma arc_next_disjoint x y : x \in p -> y \in p -> x != y -> [disjoint arc s x (next p x) & arc s y (next p y)].
proof: Proof. move=> x_p y_p xDy. have x_s : x \in s by apply p_in_s. have ? : 1 < size p. { apply: leq_trans (card_size _). by apply/card_gt1P; exists x,y. } apply: arc_disjoint; try apply: p_in_s; rewrite ?mem_next //. 1-2: exact: next_neq. all: by apply: findex_next_other; rewrite // eq_sym. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)