proposition: Lemma add_edge_orbitXe : cface x y -> orbit face (IcpXe : H) = IcpXe :: [seq Icp z | z <- arc (orbit face x) x y].
proof: Proof. set face' := add_edge_face; have faceI' : injective face' by apply: (@faceI H). move=> cface_xy; rewrite arc_orbit // /orbit -orderSpred -findex_finv /=. congr (_ :: _); rewrite -findex_f ?fconnect_finv //= f_finv // -/face'. have F n : n < findex face x y -> iter n face' (Icp x) = Icp (iter n face x). { elim: n => // n IHn lt_n_y. rewrite iterS IHn 1?ltnW //= -iterS !ifF //. - 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 x) IcpXe = findex face x y. { rewrite I. apply: (@eq_from_nth _ (Icp x)); rewrite ?size_map !size_traject // => n Hn. by rewrite nth_traject // (nth_map x) ?size_traject // nth_traject ?F. } have idx0 : 0 < findex face x y by rewrite lt0n findex_eq0. 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 eq_sym (negPf xDy). - 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)