proposition: Lemma consistent_del1 (G : graph) (x : G) : consistent [set~ x] (~: edges_at x).
proof: Proof. move => e b. rewrite !inE. apply: contraNneq => <-. by existsb b. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)