proposition: Lemma neighbor_del_edge1 (G : sgraph) (s1 s2 : G) (A B : {set G}) : s1 \notin A -> s1 \notin B -> @neighbor (add_edge s1 s2) A B -> @neighbor G A B.
proof: Proof. move => ? ?. rewrite neighbor_add_edgeC. exact: neighbor_del_edge2. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)