proposition: Lemma fconnect_frestrict (T : finType) (P : pred T) (f : T -> T) (x y : sig P) (hom_f : {homo f : x / x \in P}) : fconnect (frestrict hom_f) x y = fconnect f (val x) (val y).
proof: Proof. apply/idP/idP => /iter_findex; move: (findex _ _ _) => n. move<-. elim: n x => [//|n IHn x]. rewrite iterSr. by apply: connect_trans (connect1 _) (IHn _); rewrite /= val_frestrict. move: x y => [x Px] [y Py] /=; rewrite -[exist _ _ _]/(Sub x Px) -[exist _ _ _]/(Sub y Py). elim: n x Px y Py => [|n IHn] x Px y Py. by move => ?; subst y; rewrite (eq_irrelevance Px Py). rewrite iterSr => it_n. apply: connect_trans (IHn _ _ _ _ it_n) => [|Pfx] ; first exact: hom_f Px. by apply: connect1; rewrite /= -val_eqE. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)