proposition: Lemma hiso_genus : genus G = genus H.
proof: Proof. have fcardF := hiso_fcard faceI (hiso_face i). have fcardN := hiso_fcard nodeI (hiso_node i). have fcardE := hiso_fcard edgeI (hiso_edge i). rewrite /genus /Euler_rhs fcardF fcardN fcardE; do 2 f_equal. rewrite /Euler_lhs. rewrite (card_bij i). suff adj : rel_adjunction i glink glink H. { rewrite (adjunction_n_comp _ _ _ _ adj) //; exact: glinkC. } apply: comm_adj => x y. by rewrite /glink/= -hiso_edge -hiso_face -hiso_node !(inj_eq). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)