proposition: Proposition stablePn : reflect (exists x y, [/\ x \in S, y \in S & x -- y]) (~~ stable).
proof: Proof. rewrite stableEedge. set E := exists _, _. have EE : (exists2 x, x \in S & exists2 y, y \in S & x -- y) <-> E by firstorder. rewrite !negb_forall_in; apply: equivP EE; apply: exists_inPP => x. rewrite negb_forall_in; apply: exists_inPP => y. exact: negPn. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)