proposition: Lemma edge_setN (G : graph) (C : {set G}) (e : edge G): e \in edge_set C -> e \notin edge_set (~: C).
proof: Proof. rewrite !inE. by case/andP => -> ->. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient bij preliminaries) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(setoid_bigop structures mgraph mgraph2)