proposition: Lemma add_node_diso_proof (G : sgraph) (A : {set G}) (x : G) : x \in A -> @add_edges2_rel (add_node G [set x]) [set None] [set Some x | x in A :\ x] =2 add_node_rel A.
proof: Proof. move=> x_A [u|] [v|] //=; rewrite [in LHS]/edge_rel/= ?inE //. - rewrite andbT andFb /= mem_imset ?inE; last exact: Some_inj. by have [->|//] := eqVneq u x; rewrite x_A. - rewrite andbF andTb orbF mem_imset ?inE; last exact: Some_inj. by have [->|//] := eqVneq v x; rewrite x_A. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry color coloring walkup combinatorial4ct cfmap) GraphTheory(edone preliminaries bij digraph sgraph) GraphTheory(connectivity minor hmap_ops smerge hcycle arc)