proposition: Lemma sinterval_outside x y u : u \notin sinterval x y -> forall (p : Path u x), irred p -> y \notin p -> [disjoint p & sinterval x y].
proof: Proof. Proof using. move=> uNIxy p Ip yNp. rewrite disjoint_subset; apply/subsetP => v. rewrite inE /= -[mem (in_nodes p)]/(mem p) => v_p. apply/negP => v_Ixy. case/(isplitP Ip) eq_p : {-}p / v_p => [p1 p2 _ _ D]. case: (sinterval_exit uNIxy v_Ixy) => /cpP/(_ p1); last first. + apply/negP; apply: contraNN yNp. by rewrite eq_p mem_pcat => ->. + move => A. by rewrite -(D x) ?sinterval_bounds ?path_end in v_Ixy. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)