proposition: Lemma maxstabset_stable S H : S \in maxstabsets H -> stable S.
proof: Proof. by rewrite !inE -andbA => /and3P[_ -> _]. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)