proposition: Lemma connected_interval (x y : G) : connected (interval x y).
proof: Proof. Proof using G_conn. apply: connected_center (intervalL x y) => z. rewrite {1}/interval [[set _;_]]setUC -setUA in_setU1 orbC. case/orP=> [/(sinterval_connectedL (setU11 _ _))|/eqP{z}->]. { apply: connect_mono => {z}. apply: restrict_mono => z /=. by rewrite /interval [[set _;_]]setUC -setUA (in_setU1 z y) => ->. } case/connect_irredP: (G_conn x y) => p Ip. apply: connectRI (p) _ => z z_p. rewrite inE -implyNb in_set2 negb_or inE. apply/implyP. wlog suff Hyp : x y p Ip z_p / z != x -> x \notin cp z y. { have Ip' : irred (prev p) by rewrite irred_rev. have z_p' : z \in prev p by rewrite mem_prev. case/andP=> zNx zNy. apply/andP; split. - exact: Hyp Ip z_p zNx. - exact: Hyp Ip' z_p' zNy. } case/(isplitP Ip) _ : _ / z_p => p1 p2 _ _ I zNx. apply: (cpNI (p := p2)). apply: contraNN zNx => H. by rewrite [x]I. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)