proposition: Fact Gamma_maxset D : min_dom D -> W D = Gamma_w -> maxset min_dom D.
proof: Proof. move => min_domD GammaD; apply: maxweight_maxset => // A. rewrite -/W GammaD; exact: Gamma_max. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)