proposition: Lemma fconnect_skip u v : fconnect skip u v = fconnect f (val u) (val v).
proof: Proof. apply/idP/idP; rewrite /= fconnect_orbit => /trajectP[n _ Dv]. rewrite {v}Dv fconnect_sym; elim: n => //= n; rewrite same_fconnect1 //. by case: eqP => // ->; rewrite same_fconnect1. elim: {n}n.+1 {-2}n (ltnSn n) => // m IHm n lemn in u Dv *. case: n => [|n] in Dv lemn; first exact/eq_connect0/val_inj. have ltn1m: n - (f (val u) == z) < m by rewrite (leq_ltn_trans (leq_subr _ _)). rewrite (same_fconnect1 inj_skip) (IHm _ ltn1m) //= -fun_if -subSKn -iterSr. case: eqP => // Dfu; rewrite -[in RHS]Dfu -iterSr subn1 prednK // lt0n. by apply: contraFneq (z'G' v) => /= n_0; rewrite Dv iterSr Dfu n_0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap)