proposition: Lemma sinterval_connectL (x y z : G) : z \in sinterval x y -> exists2 u, x -- u & connect (restrict (sinterval x y) sedge) z u.
proof: Proof. Proof using. case: (altP (z =P x)) => [->|zNx]; first by rewrite sinterval_bounds. case/sintervalP2=> -[p']. case: (splitR p' zNx) => [u] [p] [ux] {p'}->. rewrite irred_cat => /and3P[? _] /eqP/setP/(_ x). rewrite in_set1 in_set mem_edgep eqxx orbT andbT eq_sym (sg_edgeNeq ux). move=> xNp yNp' [q'] Iq' xNq'. exists u; first by rewrite sgP. apply: connectRI (p) _ => v in_p. case/psplitP eq_p : _ / in_p => [p1 p2]. rewrite inE. apply/andP. split. - apply: (@cpNI v y (pcat (prev p1) q')). rewrite mem_pcat mem_prev negb_or xNq' andbT. apply: contraFN xNp. by rewrite eq_p mem_pcat => ->. - apply: (@cpNI v x (pcat p2 (edgep ux))). apply: contraNN yNp'. by rewrite eq_p !mem_pcat -orbA => ->. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)