proposition: Lemma bag_nontrivial (U : {set G}) x : bag U x != [set x] -> exists2 y, y \in bag U x & y != x.
proof: Proof. apply: setN01E. apply/set0Pn. exists x. by rewrite bag_id. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)