proposition: Lemma decC z : (z \in C) + (z \in ~: C)%type.
proof: Proof. case: (boolP (z \in C)) => p; [by left|right]. by rewrite inE p. 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)