proposition: Proposition gamma_w_leq_ii_w : gamma_w <= ii_w.
proof: Proof. rewrite /ii_w. have [S max_stS _] := arg_minnP W inhb_max_st_is_maximal_stable. have domS := minsetp (maximal_st_is_minimal_dom max_stS). exact: gamma_min. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)