proposition: Lemma add_edge_no_cross : cface x y -> ~~ cface (IcpX : H) (IcpXe : H).
proof: Proof. move => f_x_y; rewrite /= -fconnect_switched //; last exact: (@faceI H). rewrite same_fconnect1 /=; last by apply/switch_inj/(@faceI H). rewrite -[y](f_finv faceI) -same_fconnect1_r // in f_x_y. have := iter_findex (f_x_y). have Hx: forall m, iter m.+1 face x = x -> findex face x (finv face y) <= m. { move => m Ex. rewrite -ltnS. have L : looping face x m.+1 by rewrite /looping Ex /= inE eqxx. apply: leq_trans (order_le_looping L). exact: findex_max. } move: (findex _ _ _) Hx => n Hx In. elim: n {-3}x In Hx => [/= z|n IHn z In Hx]. - move => Ez _. apply: connect1 => /=. by rewrite Ez f_finv // eqxx [_ == x]eq_sym (negbTE xDy). - rewrite iterSr in In. move/IHn in In. rewrite same_fconnect1 /=; last by apply/switch_inj/(@faceI H). have/negbTE -> : face z != x. move: (Hx 0). by apply: contraPneq => /= -> /(_ erefl). case:(altP (face z =P y)) => // fzy. apply In => m. rewrite -iterSr. by move/Hx. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)