proposition: Lemma finv_skip (T : finType) (a : pred T) (f : T -> T) : injective f -> {in a, finv (skip a f) =1 skip a (finv f)}.
proof: Proof. Abort. Section DelNode. Variables (G : hypermap) (z : G). Let N := fclosure edge (cnode z). Definition del_dart := { x : G | x \notin N }. Lemma del_edge_hom : {homo edge : x / x \notin N}. Proof. move => x. by rewrite /N -(closure_closed cedgeC _ (eqxx _)). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)