proposition: Fact Gamma_witness : exists2 D, min_dom D & W D = Gamma_w.
proof: Proof. rewrite /Gamma_w. case: (arg_maxnP W inhb_min_dom_is_minimal_dominating) => D. by exists D. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)