proposition: Lemma n_comp_Knm n m : n_comp (--) 'K_n.+1,m.+1 = 1.
proof: Proof. set K := 'K__,_; pose x : K := inl ord0. suff S : connect (--) x =i K. by rewrite -(eq_n_comp_r S) n_comp_connect //; exact: sconnect_sym. move => y; rewrite !inE. case: y => [y|y]; last exact: connect1. by apply: (@connect_trans _ _ (inr ord0)); 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)