proposition: Lemma add_node_face_orbitE : orbit add_node_face IcpX = [:: IcpX, IcpXe & [seq Icp z | z <- orbit face x]].
proof: Proof. rewrite /orbit. have -> : order add_node_face IcpX = (arity x).+2. { rewrite /order -[in RHS](card_imset _ Ico_inj). set IcpF := [set _ _ | _ in _]. rewrite [LHS](eq_card (_ : _ =i [set IcpX; IcpXe] :|: IcpF)). - rewrite -setUA !cardsU1 !inE /= 2![_ \in IcpF](negbTE _) //. all: by apply/negP => /imsetP [?]. - move => z; rewrite !inE. case: (eqVneq z IcpX) => [->|]; first by rewrite connect0. case: (eqVneq z IcpXe) => [->|]; first by rewrite connect1. have ? := @faceI h_add_node. case: z => [z||]//= z _ _; rewrite same_fconnect1 //= same_fconnect1 //=. rewrite /IcpF mem_imset // inE. exact: add_node_cfaceE. } rewrite /=; congr [:: _ , _ & _]. apply: (@eq_from_nth _ (Icp x)); first by rewrite size_map !size_traject. move => n; rewrite size_traject => lt_n_st. rewrite nth_traject // (nth_map x) ?size_traject // nth_traject //. elim: n lt_n_st => // n IHn lt_Sn_x. rewrite iterS IHn 1?ltnW //= -iterS ifF //. apply: contraTF (lt_Sn_x) => /eqP; rewrite -leqNgt => fix_x. exact: order_le_fix. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)