proposition: Lemma connected_bag x (U : {set G}) : x \in CP U -> connected (bag U x).
proof: Proof. Proof using G_conn. move => cp_x. suff S z : z \in bag U x -> connect (restrict (bag U x) sedge) x z. { move => u v Hu Hv. apply: connect_trans (S _ Hv). rewrite srestrict_sym. exact: S. } move => Hz. case/connect_irredP : (G_conn z x) => p irr_p. suff/subsetP sP : p \subset bag U x. { rewrite srestrict_sym. exact: (connectRI p). } apply/negPn/negP. move/subsetPn => [z' in_p N]. case/(isplitP irr_p): _ / in_p => [p1 p2 _ _ D]. suff ?: x \in p1 by rewrite -(D x) ?bag_id ?path_end // in N. apply/cpP. exact: bag_exit N. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)