proposition: Lemma union_plain (G H: hypermap) : plain G -> plain H -> plain (G ∔ H)%H.
proof: Proof. move => plainG plainH; apply/plainP => -[x|x] _ /=. by rewrite (inj_eq inl_inj) plain_eq ?plain_neq. by rewrite (inj_eq inr_inj) plain_eq ?plain_neq. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)