proposition: Lemma path_take_nth (T : eqType) (e : rel T) x s n : n < size s -> path e x s -> e (last x (take n s)) (nth x s n).
proof: Proof. elim: s x n => // a s IH x [|n] /=; first by case (e x a). rewrite ltnS => ? /andP [_ ?]; by rewrite (set_nth_default a x) ?IH. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) fourcolor(hypermap geometry jordan color coloring combinatorial4ct) GraphTheory(hmap_ops)