proposition: Lemma last_belast (T : eqType) (x : T) (s : seq T) : uniq (x :: s) -> last x s \in belast x s = false.
proof: Proof. elim: s x => //= y s IH x /andP [Hx ?]. rewrite inE IH // orbF. apply: contraNF Hx => /eqP <-. exact: mem_last. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) fourcolor(hypermap geometry jordan color coloring combinatorial4ct) GraphTheory(hmap_ops)