proposition: Lemma cpo_cp x y : x \in cp i o -> y \in cp i o -> cpo x y -> forall z, z \in cp x y = [&& (z \in cp i o), cpo x z & cpo z y].
proof: Proof. Proof using. move=> x_cpio y_cpio. have [x_path y_path] : x \in the_uPath /\ y \in the_uPath. { by split; move: the_uPath; apply/cpP. } rewrite {1}/cpo leq_eqVlt =>/orP[/eqP/(idx_inj x_path)<- z | x_lt_y]. { rewrite cpxx inE eq_sym. apply/eqP/andP; last by case; exact: cpo_antisym. by move=><-; split; last rewrite /cpo. } case: (three_way_split the_connect_irredP x_path y_path x_lt_y) => [p1] [p2] [p3] [eq_path xNp3 yNp1]. move: the_connect_irredP. rewrite eq_path. case/irred_catE => Ip1 /irred_catE [Ip2 Ip3 D23] D123. move=> z; apply/idP/andP. + move=> z_cpxy. have z_cpio := cp_widen x_cpio y_cpio z_cpxy. split=>//. move: z_cpio => /cpP/(_ the_uPath) z_path. move: z_cpxy => /cpP/(_ p2) z_p2. rewrite /cpo. case: (altP (z =P x)) => [->|zNx]; first by rewrite leqnn (ltnW x_lt_y). apply/andP; split; last first. - rewrite eq_path idx_catR ?idx_catL ?path_end ?idx_end ?idx_mem //. apply: contraNN zNx => ?. by rewrite [z]D123 // mem_pcat z_p2. - rewrite eq_path leq_eqVlt. apply/orP; right. rewrite -idxR -?eq_path ?the_connect_irredP //. apply: in_tail zNx _. by rewrite mem_pcat z_p2. + case=> z_cpio /andP[x_le_z z_le_y]. apply/cpP => p. have /cpP/(_ (pcat p1 (pcat p p3))) := z_cpio. case (altP (z =P x)) => [-> _ | zNx]; first exact: path_begin. case (altP (z =P y)) => [-> _ | zNy]; first exact: path_end. have zNp1 : z \notin p1. { apply: contraNN zNx => z_p1. apply/eqP; apply: cpo_antisym => //. rewrite x_le_z andbT /cpo eq_path idx_catL ?path_end // idx_end //. exact: idx_mem. } rewrite mem_pcat -implyNb => /implyP/(_ zNp1). rewrite mem_pcat => /orP[// | /(in_tail zNy) z_p3]. exfalso; have := zNy; apply/negP; rewrite negbK. apply/eqP; apply: cpo_antisym => //. rewrite z_le_y /=/cpo eq_path idx_catR // leq_eqVlt. rewrite -idxR ?z_p3 // ?irred_cat ?mem_pcat ?(tailW z_p3) ?Ip2 ?Ip3//=. apply/eqP/setP => k. rewrite !inE. apply/andP/eqP => [[]|-> //]. exact: D23. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)