proposition: Theorem maximal_st_iff_st_dom : maxset stable D <-> (stable D /\ dominating D).
proof: Proof. rewrite -(rwP (maximal_indsysP _ st_hereditary)). rewrite /iff ; split ; last first. - move=> [ stableD /dominatingP dominatingD]. split => // v vnotinD. have [w winD adjwv] := dominatingD _ vnotinD. apply/stablePn; exists v; exists w. by rewrite !inE eqxx winD sgP adjwv orbT. - move => [stableD H1]; split=> //. apply/dominatingP => x xnotinD. have/stablePn [w [z [winDcupx zinDcupx adjwz]]] := H1 x xnotinD. case: (eqVneq z x) => [zisx|zisnotx]. + by subst z; exists w => //; rewrite !inE (sg_edgeNeq adjwz) in winDcupx. + have zinD : z \in D by rewrite !inE (negbTE zisnotx) /= in zinDcupx. exists z => //. move: winDcupx; rewrite in_setU in_set1. case/predU1P => [|winD]; first by move<- ; rewrite sg_sym adjwz. have := stableP D stableD w z winD zinD. apply: contraR. by rewrite adjwz. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)