proposition: Lemma dominatingEedge : dominating = [forall (v | v \notin D), exists u in D, u -- v].
proof: Proof. apply/forallP/forall_inP => [H v vND |H v]. - have [u udomv] := bigcupP (H v). rewrite in_cln; case/predU1P => [?|uv]; first by subst;contrab. by apply/exists_inP; exists u. - case: (boolP (v \in D)) => [|/H/exists_inP[u uD uv]]; last exact: mem_clns uv. exact/subsetP/set_sub_clns. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)