proposition: Lemma stableEedge : stable = [forall u in S, forall v in S, ~~ (u -- v)].
proof: Proof. symmetry ; rewrite /stable ; apply/stableP_alt/disjointP => stS. - move => x /bigcupP [y yS adjyx] xS. move: adjyx. rewrite in_opn. apply/negP. by apply: stS. - move => x y xS yS. apply/negP => adjxy. exact: (stS y (mem_opns xS adjxy) yS). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)