proposition: Lemma bag_exit_edge (U : {set G}) x u v : x \in CP U -> u \in bag U x -> v \notin bag U x -> u -- v -> u = x.
proof: Proof. Proof using G_conn. move=> x_cp u_bag vNbag uv. move/cpP/(_ (edgep uv)): (bag_exit x_cp u_bag vNbag). rewrite mem_edgep. case/orP=> /eqP// Exv. move: vNbag. by rewrite -Exv bag_id. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)