proposition: Lemma ncp_bag (U : {set G}) (p : G) x : x \in CP U -> (p \in bag U x) = (ncp U p == [set x]).
proof: Proof. Proof using G_conn. move => Ux. apply/bagP/eq_set1P. - move => A. split. + apply/ncpP; split => //. case/connect_irredP : (G_conn p x) => q irr_q. case: (boolP [exists y in CP U, y \in [predD1 q & x]]). * case/exists_inP => y /= B. rewrite inE eq_sym => /= /andP [C D]. case:notF. apply: contraTT (A _ B) => _. apply/cpPn. case/(isplitP irr_q) def_q : q / D => [q1 q2 irr_q1 irr_q2 D12]. exists q1 => //. apply: contraNN C => C. by rewrite [x]D12 // path_end. * rewrite negb_exists_in => /forall_inP B. exists q => y /B => C D. apply/eqP. apply: contraNT C => C. by rewrite inE C. + move => y /ncpP [Uy [q Hq]]. have Hx : x \in q. { apply/cpP. exact: A. } apply: esym. exact: Hq. - case => A B y Hy. apply/cpP => q. have qy : y \in q by rewrite path_end. move: (split_at_first Hy qy) => [x'] [q1] [q2] [def_q cp_x' Hq1]. suff ?: x' = x. { subst x'. by rewrite def_q mem_pcat path_end. } apply: B. apply/ncpP. split => //. exists q1 => z' H1 H2. exact: Hq1. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)