proposition: Theorem maximal_st_is_minimal_dom : maxset stable D -> minset dominating D.
proof: Proof. rewrite maximal_st_iff_st_dom => -[/stableP stableD dominatingD]. apply/(minimal_indsysP _ dom_superhereditary); split=> // x xinD. apply/dominatingPn ; exists x ; first by rewrite in_setD1 eqxx andFb. move=> y /setD1P [_ yinD]. exact: stableD. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)