proposition: Lemma union_adjn_rl (G H : hypermap) (x : H) (y : G) : @adjn (G ∔ H)%H (inr x) (inl y) = false.
proof: Proof. by apply: (introF exists_inP); move => -[[z|z]]; rewrite !inE /= ?fconnect_sumf. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)