proposition: Lemma arc_disjoint2 x y : uniq s -> x \in s -> y \in s -> x != y -> [disjoint arc s x y & arc s y x].
proof: Proof. move => uniq_s x_s y_s xDy. have [n s1 s2 <- <- rot_s] := rot_to_arc uniq_s x_s y_s xDy. move: uniq_s; rewrite -(rot_uniq n) rot_s -cat_cons cat_uniq. by rewrite disjoint_sym disjoint_has => /and3P [_ -> _]. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)