proposition: Lemma dominatingPn : reflect (exists2 v : G, v \notin D & {in D, forall u, ~~ u -- v}) (~~ dominating).
proof: Proof. rewrite dominatingEedge negb_forall_in. apply: exists_inPP => x; exact: exists_inPn. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)