proposition: Lemma n_comp_Kn n : n_comp (--) 'K_n.+1 = 1.
proof: Proof. apply: connected_n_comp1 (ord0 : 'K_n.+1) _. apply: (@connected_center _ (ord0 : 'K_n.+1)) => // j _. by have [-> //|?] := eqVneq ord0 j; apply: connect1. 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)