proposition: Lemma sinterval_connectedL (x y : G) : connected (x |: sinterval x y).
proof: Proof. Proof using. apply: connected_center (setU11 _ _) => z Hx. have := Hx. rewrite in_setU1. case/orP=> [/eqP->|/sinterval_connectL]; first exact: connect0. case=> u xu /connect_restrict_case[z_u|]. - rewrite z_u. apply: connectRI (edgep xu) _ => v. rewrite mem_edgep. case/orP=> /eqP->; by [exact: setU11 | rewrite -z_u]. - case=> zNu _ Hu /(connect_irredRP zNu)[p _ /subsetP p_sub]. apply: connectRI (pcat (edgep xu) (prev p)) _ => v. rewrite mem_pcat mem_edgep mem_prev in_setU1 -orbA. case/or3P=> [->|/eqP->|/p_sub->] //. by rewrite Hu. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)