proposition: Lemma bagPn (U : {set G}) x z : reflect (exists2 y, y \in CP U & x \notin cp z y) (z \notin bag U x).
proof: Proof. Proof using. rewrite /bag -lock inE negb_forall. apply: (iffP existsP) => [[y]|[y] A B]. - rewrite negb_imply => /andP[? ?]. by exists y. - exists y. by rewrite A. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)