proposition: Lemma subseq_notin (T : eqType) (z : T) (p s1 s2 : seq T) : z \notin s1 -> subseq (z :: p) (s1 ++ z :: s2) -> subseq p (z :: s2).
proof: Proof. elim: s1 => [_|a s1 IH]. - rewrite cat0s [X in X -> _]/= eqxx => sub_p. exact: subseq_trans sub_p (subseq_cons _ _). - rewrite inE negb_or [X in _ -> X -> _]/= => /andP[/negPf-> zNs1]. exact: IH. 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)