proposition: Lemma bag_id (U : {set G}) x : x \in bag U x.
proof: Proof. rewrite /bag -lock inE. apply/forall_inP => y _. exact: mem_cpl. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)