proposition: Lemma path_take (T : eqType) (e : rel T) x s n : path e x s -> path e x (take n s).
proof: Proof. by rewrite -{1}[s](cat_take_drop n) cat_path; case/andP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) fourcolor(hypermap geometry jordan color coloring combinatorial4ct) GraphTheory(hmap_ops)