proposition: Lemma sinterval_sub x y z : z \in cp x y -> sinterval x z \subset sinterval x y.
proof: Proof. Proof using G_conn. move=> z_cpxy. apply/subsetP=> u. rewrite !inE. case/andP=> xNcpuz zNcpux. apply/andP; split. - apply: contraNN xNcpuz => x_cpuy. exact: cp_tightenR z_cpxy x_cpuy. - apply: contraNN zNcpux => y_cpux. apply: cp_widen y_cpux z_cpxy. by rewrite cp_sym mem_cpl. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)