proposition: Lemma neighbor_add_edge (G : sgraph) (s1 s2 : G) : subrel (@neighbor G) (@neighbor (add_edge s1 s2)).
proof: Proof. move => A B /neighborP [u] [v] [? ? E]. apply/neighborP; exists u; exists v. by rewrite /edge_rel/= E. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)