proposition: Lemma fconnect_skip: {in a&, fconnect skip =2 fconnect f}.
proof: Proof. move => x y x_a y_a; apply/idP/idP. - move/iter_findex<-; move: (findex _ _ _) => n; elim: n x x_a => //= n IHn x x_a. apply: connect_trans (IHn _ x_a) _. case: skipP => [|m *]; last exact: fconnect_iter. by apply/iter_in => //; apply: skip_hom. - move/iter_findex => E; rewrite -{}E in y_a *. move: (findex _ _ _) y_a => n. have [m Hm] := ubnP n; elim: m n Hm x x_a {y} => // m IHm [//|n] /ltnSE n_leq_m x x_a iter_n_f. case: (boolP [exists k : 'I_n, (iter k.+1 f x \in a)]). + case/existsP => [[k Hk] iter_k_f]. apply: connect_trans (IHm _ _ _ _ iter_k_f) _ => //. by apply: leq_trans n_leq_m. apply: connect_trans (IHm (n.+1 - k.+1) _ _ _ _) _ => //. * apply: leq_trans n_leq_m. by rewrite subSS ltnS leq_subr. * by rewrite -iterD subnK // ltnW. * by rewrite -iterD subnK // ltnW. + move/existsPn => Hn. rewrite (_ : iter n.+1 f x = skip x) ?fconnect1 //. case: skipP => // k _ K1 K2. rewrite (_ : n = k) //; apply/eqP. rewrite eqn_leq K2 // andbT leqNgt. apply: contraTN K1 => Hk; exact: (Hn (Ordinal Hk)). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)