proposition: Fact ii_witness : exists2 S, max_st S & W S = ii_w.
proof: Proof. rewrite /ii_w. case: (arg_minnP W inhb_max_st_is_maximal_stable) => S. by exists S. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)