proposition: Lemma sinterval_components (C : {set G}) x y : C \in components (sinterval x y) -> (exists2 u, u \in C & x -- u) /\ (exists2 v, v \in C & y -- v).
proof: Proof. Proof using. move=> C_comp. wlog suff Hyp : x y C_comp / exists2 u : G, u \in C & x -- u. { split; move: C_comp; last rewrite sinterval_sym; exact: Hyp. } case/and3P: (partition_components (sinterval x y)). move=> /eqP compU compI comp0. have /card_gt0P[a a_C] : 0 < #|C|. { rewrite card_gt0. by apply: contraTneq C_comp =>->. } have a_sI : a \in sinterval x y. { rewrite -compU. by apply/bigcupP; exists C. } rewrite -{C C_comp a_C}(def_pblock compI C_comp a_C). case: (sinterval_connectL a_sI) => u xu u_a. exists u => //. have u_sI : u \in sinterval x y by case/connect_restrict_case: u_a => [<-|[]]. rewrite pblock_equivalence_partition //. exact: sedge_equiv_in. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)