proposition: Lemma add_edge_cnodeE u v : cnode (Icp u : H) (Icp v) = cnode u v.
proof: Proof. apply/idP/idP; case/connectP => p. - elim/(size_ind (@size H)) : 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. + have [fuEy /andP[/eqP <-] {z}|fuDy] := eqVneq u y. * case: p IH => [|z p] //= IH => /andP[/eqP<-] {z}. by rewrite cnode1 fuEy; 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_edge; rewrite same_fconnect1 //=. have [fu_x|_] := eqVneq u x; first by rewrite same_fconnect1 //= -fu_x fu_z; exact: IHp. have [fu_y|_] := eqVneq u y; first by rewrite same_fconnect1 //= -fu_y fu_z; exact: IHp. by rewrite fu_z; exact: IHp. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)