proposition: Lemma undup_subseq (T : eqType) (s : seq T) : subseq (undup s) s.
proof: Proof. elim: s => // x s IHs; rewrite [undup _]/=; case: ifP; last by rewrite /= eqxx. by move=> _; apply: subseq_trans IHs (subseq_cons _ _). Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry color coloring walkup combinatorial4ct cfmap) GraphTheory(edone preliminaries bij digraph sgraph) GraphTheory(connectivity minor hmap_ops smerge hcycle arc)