proposition: Lemma kplanar_add_edge (G : sgraph) (V1 V2 : {set G}) (x y : G) : x != y -> proper_separation V1 V2 -> V1 :&: V2 = [set x; y] -> smallest vseparator (V1 :&: V2) -> kplanar G -> kplanar (@induced (add_edge G x y) V1) /\ kplanar (@induced (add_edge G x y) V2).
proof: Proof. move => xDy psepV capVxy ssepV [K33G K5G]. have exV1 := add_edge_separation_excluded xDy psepV capVxy ssepV. split; first by split; apply: exV1. move/proper_separation_symmetry in psepV. rewrite [V1 :&: V2]setIC in capVxy ssepV. have exV2 := add_edge_separation_excluded xDy psepV capVxy ssepV. by split; apply: exV2. Qed.
imports: HB(structures) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(sgraph connectivity minor excluded) fourcolor(hypermap geometry walkup color coloring combinatorial4ct) GraphTheory(set_tac) GraphTheory(hmap_ops smerge embedding arc K4plane)