proposition: Lemma le_genus_WalkupE : genus G' <= genus G.
proof: Proof. have [/orP/genus_WalkupE_eq-> // |] := boolP (glink z z || ~~ cross_edge). case/norP=> zG'z /negPn-zEnz; rewrite /(genus G) -subSS. rewrite -Euler_lhs_WalkupE -Euler_rhs_WalkupE /n_comp_z !ifN // zEnz. by rewrite half_leq // leq_sub2r ?leq_addl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap)