proposition: Lemma bag_exit (U : {set G}) x u v : x \in CP U -> u \in bag U x -> v \notin bag U x -> x \in cp u v.
proof: Proof. Proof using G_conn. move => cp_x. rewrite [v \in _]ncp_bag // => N1 N2. have [y [Y1 Y2 Y3]] : exists y, [/\ y \in CP U, x != y & y \in ncp U v]. { case: (setN01E _ N2); first by rewrite (ncp0 x). move => y Y1 Y2. exists y; split => //; by [rewrite eq_sym|case/ncpP : Y1]. } move/bagP : N1 => /(_ _ Y1). apply: contraTT => /cpPn [p] irr_p av_x. case/ncpP : Y3 => _ [q] /(_ _ cp_x) A. have {A} Hq : x \notin q. { apply/negP => /A ?. subst. by rewrite eqxx in Y2. } apply: (cpNI (p := pcat p q)). by rewrite mem_pcat negb_or av_x. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)