proposition: Lemma hiso_adjn x y : adjn (i x) (i y) = adjn x y.
proof: Proof. apply/exists_inP/exists_inP => -[z Z1 Z2]. - exists (i^-1 z); first by rewrite inE hiso_cnode bijK'. by rewrite inE hiso_cnode hiso_edge bijK'. - exists (i z); first by rewrite inE -hiso_cnode. by rewrite inE -hiso_edge -hiso_cnode. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)