proposition: Lemma smerge2_neighbor (G : sgraph) (x y : G) (xDy : x != y) : val @: N(Sub x xDy : smerge2 G x y) = (N(x) :|: N(y)) :\: [set x;y].
proof: Proof. apply/setP => z; rewrite !inE; apply/imsetP/andP => [[z0 Hz0 ->]|[]]. move: Hz0. rewrite !inE negb_or (valP z0) /edge_rel/= eqxx andbF /=. case: (eqVneq (sval z0) x) => /= [<-|]; by rewrite ?sg_irrefl ?[sval _ -- _]sg_sym. rewrite negb_or => /andP [zDx zDy]; exists (Sub z zDy) => //. by rewrite inE /edge_rel/= eqxx andbF /= ![z -- _]sg_sym zDx. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity minor treewidth arc set_tac)