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