proposition: Lemma union_planar (G1 G2 : hypermap) : planar (G1 ∔ G2) <-> planar G1 /\ planar G2.
proof: Proof. rewrite /planar union_genus addn_eq0. by do 2 case (_ == 0) => //=; firstorder. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)