proposition: Lemma disconnectedE (G : sgraph) (S : {set G}) : disconnected S <-> ~ connected S.
proof: Proof. split; first by case=> [x] [y] [x_S y_S /negP xNy] /(_ x y x_S y_S). move=> SNconn. apply/'exists_'exists_and3P. rewrite -[X in is_true X]negbK. apply/negP => SNdisconn. apply: SNconn => x y x_S y_S. move: SNdisconn. rewrite negb_exists => /forallP/(_ x). rewrite negb_exists => /forallP/(_ y). by rewrite x_S y_S /= negbK. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)