proposition: Lemma stabsetsP H S : reflect (S \subset H /\ stable S) (S \in stabsets H).
proof: Proof. by rewrite in_stabsets; exact: andP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)