proposition: Lemma CP_closed U x y : x \in CP U -> y \in CP U -> cp x y \subset CP U.
proof: Proof. Proof using G_conn. case/bigcupP => [[x1 x2] /= /setXP [x1U x2U] x_cp]. case/bigcupP => [[y1 y2] /= /setXP [y1U y2U] y_cp]. apply/subsetP => t t_cp. case (boolP (t == y)) => [/eqP-> //|T2]. { apply/bigcupP. exists (y1,y2); by [exact/setXP|]. } case (boolP (t == x)) => [/eqP-> //|T1]. { apply/bigcupP. exists (x1,x2); by [exact/setXP|]. } move: (cp_mid T1 x_cp) => [p1] [p2] H. wlog P1 : x1 x2 p1 p2 x1U x2U x_cp H / t \notin p1 => [W|{H}]. { case: H => H. - by apply : (W _ _ p1 p2) => //; tauto. - rewrite cp_sym in x_cp. apply : (W _ _ p2 p1) => //; tauto. } move: (cp_mid T2 y_cp) => [q1] [q2] H. wlog P2 : y1 y2 q1 q2 y1U y2U y_cp H / t \notin q1 => [W|{H}]. { case: H => H. - by apply : (W _ _ q1 q2) => //; tauto. - rewrite cp_sym in y_cp. apply : (W _ _ q2 q1) => //; tauto. } apply/bigcupP; exists (x1,y1) => /= ; first exact/setXP. apply: contraTT t_cp => /cpPn [s _ Hs]. suff: t \notin (pcat p1 (pcat s (prev q1))) by apply: cpNI. by rewrite !mem_pcat !mem_prev (negbTE P1) (negbTE P2) (negbTE Hs). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)