proposition: Lemma fpath_sub_belast (T : eqType) (f : T -> T) x (s : seq T) (p : {pred T}) : fpath f x s -> {subset x::s <= p} -> {in belast x s, forall y, p (f y)}.
proof: Proof. rewrite -[{subset _ <= _}]/({in x::s, forall y, p y}) !(rwP allP). elim: s x => //= a s IHs x /andP [/eqP->] pth_s /and3P [_ pa all_s] /=. by rewrite pa IHs. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)