proposition: Lemma last_head_behead (T : eqType) (x : T) (p : seq T) : last (head x p) (behead (rcons p x)) = x.
proof: Proof. case: p => //= ? ?. exact: last_rcons. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) fourcolor(hypermap geometry jordan color coloring combinatorial4ct) GraphTheory(hmap_ops)