proposition: Fact Gamma_max D : min_dom D -> W D <= Gamma_w.
proof: Proof. move: D ; rewrite /Gamma_w. by case: (arg_maxnP W inhb_min_dom_is_minimal_dominating). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)