proposition: Lemma K5nonplanar : ~ inhabited (plane_embedding 'K_5).
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| = 20 by rewrite (card_emb emb_g simpleD) card_edge_Kn. have -> : Euler_lhs D = 22. by rewrite /Euler_lhs (emb_n_comp emb_g) n_comp_Kn cD. have -> : Euler_rhs D = 15 + F. { rewrite /Euler_rhs (emb_ncard emb_g) (emb_ecard emb_g simpleD). by rewrite card_ord card_edge_Kn. } suff: F < 7 by case: F => [|[|[|[|[|[|[|]]]]]]]. apply: contra_eqT cD. rewrite eqn_leq negb_and -!ltnNge ltnS => F7. apply/orP;left; rewrite (sum_roots_order faceI). have bound : {in froots (@face D), forall x, 2 < arity x}. { apply:in1W => x; apply: emb_arity3 emb_g simpleD _ _ => {x} x. exact: leq_trans (deg_Kn _). } 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 (7 * 3)); rewrite // leq_mul2r F7. 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)