proposition: Lemma add_edge_orbitX : cface x y -> orbit face (IcpX : H) = IcpX :: [seq Icp z | z <- arc (orbit face x) y x].
proof: Proof. set face' := add_edge_face; have faceI' : injective face' by apply: (@faceI H). rewrite cfaceC => cface_xy. have -> : arc (orbit face x) y x = arc (orbit face y) y x. { have/orbit_rot_cycle : x \in orbit face y by rewrite -fconnect_orbit. move=> /(_ face); rewrite cycle_orbit // orbit_uniq => /(_ isT isT) [i ->]. by rewrite arc_rot // in_orbit. } rewrite arc_orbit // /orbit -orderSpred -findex_finv /=. congr (_ :: _); rewrite -findex_f ?fconnect_finv //= f_finv // -/face'. have F n : n < findex face y x -> iter n face' (Icp y) = Icp (iter n face y). { elim: n => // n IHn lt_n_y. rewrite iterS IHn 1?ltnW //= -iterS !ifF //; last first. - by apply:negPf; apply: before_findex. - apply: contraTF (cface_xy) => /eqP it_n. apply: (iter_looping (m := n.+1)). + move => m Hm. apply: before_findex => //. exact: ltn_trans lt_n_y. + by rewrite /looping it_n /= mem_head. } suff I : findex face' (Icp y) IcpX = findex face y x. { rewrite I. apply: (@eq_from_nth _ (Icp y)); rewrite ?size_map !size_traject // => n Hn. by rewrite nth_traject // (nth_map y) ?size_traject // nth_traject ?F. } have idx0 : 0 < findex face y x by rewrite lt0n findex_eq0 eq_sym. apply/eqP; rewrite eqn_leq; apply/andP; split. - apply: findex_bound. rewrite -(prednK idx0) iterS F ?prednK //. rewrite -[iter _ _ _](finv_f faceI) -iterS prednK // iter_findex //=. by rewrite !f_finv // eqxx. - rewrite leqNgt; apply/negP; set m := findex face' _ _ => /F. by rewrite iter_findex // same_fconnect1_r //= connect0. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)