proposition: Lemma K33nonplanar : ~ inhabited (plane_embedding 'K_3,3).
proof: Proof. move => [/simple_embedding [[D g emb_g planarD] /= simpleD]]. suff : Euler_lhs D - Euler_rhs D > 0 by rewrite -genus_gt0 (eqP planarD). pose F := fcard face D. have cD : #|D| = 18 by rewrite (card_emb emb_g simpleD) card_edge_Knm. have -> : Euler_lhs D = 20. by rewrite /Euler_lhs (emb_n_comp emb_g) n_comp_Knm cD. have -> : Euler_rhs D = 15 + F. { rewrite /Euler_rhs (emb_ncard emb_g) (emb_ecard emb_g simpleD). by rewrite card_sum card_ord card_edge_Knm. } suff : F <= 4 by case: F => [|[|[|[|[|]]]]]. apply: contra_eqT (cD); rewrite -ltnNge eqn_leq negb_and -ltnNge => F5. apply/orP;left; rewrite (sum_roots_order faceI). suff bound : {in froots (@face D), forall x, 3 < arity x}. { apply: leq_trans (leq_sum _ bound) ; rewrite sum_nat_const. have -> : #|froots (@face D)| = F by apply: eq_card => z; rewrite !inE andbT. by apply: (@leq_trans (5 * 4)); rewrite // leq_mul2r F5. } move=> x _; rewrite ltn_neqAle (emb_arity3 emb_g simpleD) ?andbT 1?eq_sym. - have/even_cycle_Knm := emb_face_cycle emb_g x. by apply: contraNneq; rewrite size_map size_orbit => ->. - move=> y. exact: leq_trans (deg_Knm _). Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry color coloring walkup combinatorial4ct cfmap) GraphTheory(edone preliminaries bij digraph sgraph) GraphTheory(connectivity minor hmap_ops smerge hcycle arc)