proposition: Lemma edges_add_node (G : sgraph) (A : {set G}) : E(add_node G A) = [set [set None; Some x] | x in A] :|: [set Some @: (e : {set G}) | e in E(G)].
proof: Proof. apply/setP => e; apply/edgesP/setUP => [[x] [y] [-> xy]|]. - have [None_e|NoneNe] := boolP (None \in [set x;y]); [left|right]. + wlog ? : x y xy {None_e} / None = x; [move=> W|subst x]. by case/set2P : None_e; last rewrite setUC; apply: W; rewrite // sgP. by case: y xy => //= a a_A; apply: imset_f. + move: x y xy NoneNe => [x|] [y|]; rewrite !inE ?eqxx //= => xy _. by apply/imsetP; exists [set x;y]; rewrite ?in_edges // imsetU1 imset_set1. - move=> [/imsetP[x xA ->]|/imsetP[e' eG ->]]; first by exists None, (Some x). have [x[y [-> xy]]] := edgesP _ eG; exists (Some x),(Some y). by rewrite imsetU1 imset_set1. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)