proposition: Lemma mem_arc_other x y z : x \in s -> y \in s -> z \in s -> x != y -> (z \in arc s x y) = (z \notin arc s y x).
proof: Proof. move=> x_s y_s z_s xDy; have/esym := arc_cover x_s y_s xDy z; rewrite z_s inE /=. have D := arc_disjoint2 uniq_s x_s y_s xDy. by case/orP => z_arc; rewrite z_arc ?(disjointFr D) // ?(disjointFl D). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)