proposition: Lemma arc_disjoint x1 x2 y1 y2 : uniq s -> x1 \in s -> x2 \in s -> y1 \in s -> y2 \in s -> x1 != x2 -> y1 != y2 -> findex (next s) x1 x2 <= findex (next s) x1 y1 -> findex (next s) y1 y2 <= findex (next s) y1 x1 -> [disjoint arc s x1 x2 & arc s y1 y2].
proof: Proof. move=> uniq_s x1_s x2_s y1_s y2_s x1Dx2 y1Dy2 index_x index_y. have x1Dy1 : x1 != y1. { apply: contraNneq x1Dx2 => ?; subst y1. by move: index_x; rewrite findex0 leqn0 findex_eq0. } apply/pred0Pn => -[x] /=; rewrite !arc_findex // => /andP [A1 A2]. have {A1 index_x} := leq_trans A1 index_x. have {A2 index_y} := leq_trans A2 index_y. rewrite -!arc_findex //= 1?eq_sym // => x_arc. by apply/negP; rewrite (disjointFl (@arc_disjoint2 x1 y1 _ _ _ _)). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)