proposition: Lemma neighbor1P (x : G) (A : {set G}) : reflect (exists2 y, x -- y & y \in A) (neighbor [set x] A).
proof: Proof. apply: (iffP (neighborP _ _)) => [[z] [y] [/set1P->]|[y ? ?]]; first by exists y. by exists x, y; rewrite !inE. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)