proposition: Lemma EqHypermapEN (G : hypermap) (e n f : G -> G) (Eenf : cancel3 e n f) : edge =1 e -> node =1 n -> G =m Hypermap Eenf.
proof: Proof. move => eE nE; suff fE : face =1 f by apply: EqHypermap. by move => x; rewrite -{1}[x](@faceK (Hypermap Eenf)) /= -eE -nE nodeK. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)