proposition: Lemma even_genus_WalkupE : even_genus G' -> even_genus G.
proof: Proof. move=> evenG'; apply/eqP; rewrite -eqSS /genus -subSS -Euler_lhs_WalkupE evenG'. rewrite -addnS -Euler_rhs_WalkupE addnCA 2!addnA subnDr eqn_add2r. rewrite -doubleD -doubleB half_double -doubleD subnK // addnC /n_comp_z. by case: glink cross_edge not_cross_connected => [|[|->]]; rewrite ?leq_addr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap)