proposition: Lemma sinterval_cp_cover x y z : z \in cp x y :\: [set x; y] -> sinterval x y = sinterval x z :|: bag [set x; y] z :|: sinterval z y.
proof: Proof. Proof using G_conn. rewrite 4!inE negb_or => /andP[]/andP[zNx zNy] z_cpxy. apply/eqP. have [x_CP y_CP] : x \in CP [set x; y] /\ y \in CP [set x; y]. { by split; apply: CP_extensive; rewrite !inE eqxx. } rewrite eqEsubset !subUset sinterval_sub //=. rewrite {3}(sinterval_sym x y) {2}(sinterval_sym z y) sinterval_sub 1?cp_sym //. rewrite bag_sub_sinterval /= ?andbT //; last by rewrite in_setD in_set2 negb_or zNx zNy. apply/subsetP=> u u_sIxy. rewrite !in_setU. have [uNx uNy] : u != x /\ u != y. { by split; apply: contraTneq u_sIxy => ->; rewrite sinterval_bounds. } move: u_sIxy; rewrite inE. case/andP=> xNcpuy yNcpux. case: (boolP (z \in cp u x)) => Hx; case: (boolP (z \in cp u y)) => Hy. + suff -> : u \in bag [set x; y] z by []. apply/bagP=> c. rewrite CP_set2 => /(subsetP (cp_triangle z)). rewrite in_setU cp_sym. case/orP=> c_cp; exact: cp_tightenR c_cp _. + suff -> : u \in sinterval z y by []. rewrite inE Hy /=. apply: cpN_trans yNcpux _. apply: contraNN zNy => y_cpxz. suff : z \in cp y y by rewrite cpxx in_set1 eq_sym. move: y_cpxz z_cpxy. rewrite [cp x z]cp_sym [cp x y]cp_sym. exact: cp_tightenR. + suff -> : u \in sinterval x z by []. rewrite inE Hx andbT. apply: cpN_trans xNcpuy _. apply: contraNN zNx => x_cpyz. suff : z \in cp x x by rewrite cpxx in_set1 eq_sym. move: x_cpyz z_cpxy. rewrite [cp y z]cp_sym. exact: cp_tightenR. + rewrite cp_sym in Hx. have : z \notin cp x y := cpN_trans Hx Hy. by rewrite z_cpxy. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)