proposition: Theorem Jordan_planar G : Jordan G -> planar G.
proof: Proof. move: {-1}_.+1 (ltnSn #|G|) => m; elim: m G => // m IHm G leGm JordanG. have [x _ | noG] := pickP G; last first. have o0 (a : pred G): #|a| = 0 by apply: eq_card0 => z; have:= noG z. by rewrite /planar /genus /Euler_rhs /Euler_lhs /n_comp_mem !{1}o0. have /pred0Pn[z /andP[_ leaf_z]] := Euler_tree x JordanG. rewrite /planar -(@genus_WalkupE_eq _ z) //. by apply: IHm (Jordan_WalkupE JordanG); rewrite -card_S_Walkup. apply/orP; case/orP: leaf_z => [|->]; last exact: orbT. by case/clinkP=> [{2}-> | {2}<-]; rewrite (glinkN, glinkF). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup)