proposition: Lemma consistent_setD (G : graph) (V : {set G}) E E' : consistent V E -> consistent V (E :\: E').
proof: Proof. move => con_E e b /setDP [? _]. exact: con_E. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)