proposition: Theorem even_genusP G : even_genus G.
proof: Proof. move: {2}_.+1 (ltnSn #|G|) => n; elim: n => // n IHn in G * => leGn. have [z _ | noG] := pickP G. by apply/(@even_genus_WalkupE G z)/IHn; rewrite -card_S_Walkup. have o0 (a : pred G): #|a| = 0 by apply: eq_card0 => x; have:= noG x. by rewrite /even_genus /genus /Euler_rhs /Euler_lhs /n_comp_mem !{1}o0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup)