proposition: Lemma skip_hom : {homo skip : x / x \in a}.
proof: Proof. move => x in_a. by case: skipP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)