proposition: Lemma neighborC A B : neighbor A B = neighbor B A.
proof: Proof. by apply/neighborP/neighborP => [] [x] [y] [*];exists y; exists x; rewrite sgP. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)