proposition: Lemma neighbor_add_edgeC (G : sgraph) (s1 s2 : G) : @neighbor (add_edge s1 s2) =2 @neighbor (add_edge s2 s1).
proof: Proof. move => x y. apply/neighborP/neighborP => [] [u] [v] [? ? ?]; exists u; exists v. all: by rewrite add_edgeC. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)