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