proposition: Lemma stabsets_gt0 A : 0 < #|stabsets A|.
proof: Proof. apply/card_gt0P; exists set0; rewrite inE sub0set; apply/stableP. by move => u v; rewrite inE. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)