proposition: Lemma bag_exit' (U : {set G}) x u v : x \in CP U -> u \in bag U x -> v \in x |: ~: bag U x -> x \in cp u v.
proof: Proof. Proof using G_conn. move => cp_x Hu. case/setU1P => [->|]; first by rewrite cp_sym mem_cpl. rewrite inE. exact: bag_exit Hu. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)