proposition: Lemma add_node_cnodeE u v : cnode (Icp u : h_add_node) (Icp v) = cnode u v.
proof: Proof. apply/idP/idP; case/connectP => p. - elim/(size_ind (@size h_add_node)) : p u => -[/= _ u _ [->] //|/= z p IH u]. have [fuEx /andP[/eqP <-] {z}|fuDx] := eqVneq u x. + case: p IH => [|z p] //= IH => /andP[/eqP<-] {z}. by rewrite cnode1 fuEx; apply: IH. + case: z => [||z]; rewrite // inj_eq // => /andP [/eqP fu_z pth_p lst_p]. rewrite cnode1 fu_z. exact: IH pth_p lst_p. - elim: p u => //= [u _ -> //|z p IHp u /andP[/eqP fu_z] pth_p lst_p]. have ? := @nodeI h_add_node; rewrite same_fconnect1 //=. have [fu_x|_] := eqVneq u x; last by rewrite fu_z; exact: IHp. rewrite same_fconnect1 //= -fu_x fu_z. exact: IHp. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)