proposition: Proposition dominatingP : reflect (forall v : G, v \notin D -> exists2 u : G, u \in D & u -- v) dominating.
proof: Proof. rewrite dominatingEedge; apply/dominatingP_alt. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)