proposition: Fact ii_min S : max_st S -> ii_w <= W S.
proof: Proof. rewrite /ii_w. by case: (arg_minnP W inhb_max_st_is_maximal_stable) => A _ ; apply. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)