proposition: Proposition alpha_w_leq_Gamma_w : alpha_w <= Gamma_w.
proof: Proof. rewrite /alpha_w. have [S stS maxWS] := arg_maxnP W stable0. have max_stS := maxweight_maxset positive_weights stS maxWS. have min_domS := maximal_st_is_minimal_dom max_stS. exact: Gamma_max. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)