proposition: Lemma neighbor11 x y: neighbor [set x] [set y] = x -- y.
proof: Proof. apply/neighborP/idP => [[?[?[/set1P -> /set1P ->]]] //|xy]. by exists x,y; rewrite !inE eqxx. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)