proposition: Lemma last_memE (T : eqType) (x : T) (s : seq T) (a : pred T) : last x s \in a -> (x \in a) + { y | y \in s & y \in a}.
proof: Proof. elim/last_ind : s => [|s y _]; first by left. by rewrite last_rcons; right;exists y => //; rewrite mem_rcons mem_head. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) fourcolor(hypermap geometry jordan color coloring combinatorial4ct) GraphTheory(hmap_ops)