proposition: Lemma add_node_genus : genus h_add_node = genus G.
proof: Proof. set H := h_add_node. have SX : IcpX != IcpXe :> H by []. pose G' := @WalkupE (WalkupE (IcpXe : H)) (Sub IcpX SX). suff i : hiso G G'. { rewrite (hiso_genus i) !genus_WalkupE_eq //. - rewrite glinkN; tauto. - have E : Sub IcpX SX = @edge (WalkupE (IcpXe : H)) (Sub IcpX SX). exact: val_inj. by rewrite {2}E glinkE; tauto. } have S (z : G) : Icp z != IcpX by done. pose i (z : G) : G' := Sub (Sub (Icp z) (S z)) SX. pose i_inv (z : G') : G := if val (val z) is Icp i then i else x. have vvE (z : G') : exists z', val (val z) = Icp z'. { move: z; (do 3 case) => //= a. by exists a. } have can_fwd : cancel i_inv i. { move => u; case: (vvE u) => u' E; rewrite /i /i_inv E. do 2 apply: val_inj => /=. by symmetry. } have can_bwd : cancel i i_inv by done. have com_i_node u : i (node u) = node (i u). { do 2 apply/val_inj; rewrite /= !fun_if /= -val_eqE /=. by case: (eqVneq u x) => //= ->. } have com_i_edge u : i (edge u) = edge (i u). { do 2 apply: val_inj => //=; by case: (eqVneq (face (edge u)) x). } exact: (@Hiso _ _ (Bij can_bwd can_fwd) com_i_edge com_i_node). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)