proposition: Lemma CP_path (U : {set G}) (x y : G) (p : Path G x y) : x \in CP U -> y \in CP U -> irred p -> exists q : Path link_graph x y, [/\ irred q, q \subset CP U & q \subset p].
proof: Proof. Proof using G_conn. move: {2}#|p|.+1 (ltnSn #|p|) => n. elim: n x y p => [//|n IHn] x y p. rewrite ltnS leq_eqVlt => /orP[/eqP size_p x_cp y_cp Ip|]; last exact: IHn. case: (x =P y) => [x_y | /eqP xNy]. { move: x_y p size_p Ip => {y y_cp}<- p _ _. exists (@idp link_graph x); split; first exact: irred_idp; apply/subsetP=> z; rewrite mem_idp => /eqP-> //=. by rewrite path_end. } pose C := CP U :\ x. have {xNy} : y \in C by rewrite in_setD1 eq_sym xNy y_cp. case/split_at_first/(_ (path_end p)) => [z][p1][p2] [eq_p z_C z_1st]. move: z_C Ip. rewrite in_setD1 eq_p irred_cat => /andP[zNx z_cp] /and3P[Ip1 Ip2]. move/eqP/setP/(_ x). rewrite inE in_set1 path_begin/= eq_sym (negbTE zNx) => /negbT xNp2. have /IHn /(_ z_cp y_cp Ip2) [q[] Iq q_cp qSp2] : #|p2| < n. { rewrite -size_p. apply: proper_card. apply/properP. split; last exists x => //; last exact: path_begin. by apply/subsetP => a; rewrite eq_p mem_pcat => ->. } have xz : @sedge link_graph x z. { rewrite /= eq_sym zNx. apply/subsetP => u u_cpxz. rewrite !in_set2 -implyNb. apply/implyP=> uNx. apply/eqP. have /cpP/(_ p1) := u_cpxz. apply: z_1st. rewrite in_setD1 {}uNx /=. move: u u_cpxz. apply/subsetP. exact: CP_closed. } exists (pcat (edgep xz) q); split. - rewrite irred_cat irred_edge Iq /=. apply/eqP/setP=> u. rewrite inE in_set1 (@mem_edgep link_graph). apply/andP/eqP; [ case; case/orP=>/eqP->// | move=>->; by rewrite eqxx (path_begin q) ]. move/(subsetP qSp2). by rewrite (negbTE xNp2). - apply/subsetP=> u. rewrite (@mem_pcat link_graph) mem_edgep -orbA. case/or3P=> [/eqP->|/eqP->|/(subsetP q_cp)->] //. - apply/subsetP=> u. rewrite (@mem_pcat link_graph) mem_pcat mem_edgep -orbA. case/or3P=> [/eqP->|/eqP->|/(subsetP qSp2)->//]; by [ rewrite path_begin | rewrite path_end ]. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)