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