proposition: Lemma union_genus (G1 G2 : hypermap) : genus (G1 ∔ G2) = genus G1 + genus G2.
proof: Proof. rewrite {1}/genus. suff -> : Euler_lhs (G1 ∔ G2) = Euler_lhs G1 + Euler_lhs G2. { have -> : Euler_rhs (G1 ∔ G2) = Euler_rhs G1 + Euler_rhs G2. by rewrite /Euler_rhs !fcard_sumf //; ring. rewrite subnDA -addnBAC -1?addnBA ?Euler_le //. by rewrite halfD -!/(genus _) !even_genusP -2?addnBA // ?subnn !addn0 !odd_double. } rewrite /Euler_lhs card_sum (n_compC (fun x : (G1 ∔ G2)%H => x)). have ? := glinkC. have cl_inl : closed (@glink (G1 ∔ G2)) is_inl by apply: intro_closed => // -[x|x] [y|y]. have cl_inr := predC_closed cl_inl. have inl_adj : @rel_adjunction (G1 ∔ G2)%H G1 (@inl _ _) glink glink is_inl. { apply: strict_adjunction => //; first exact: inl_inj. apply/subsetP=> -[z _|//]; exact: codom_f. } have inr_adj : @rel_adjunction (G1 ∔ G2)%H G2 (@inr _ _) glink glink [predC is_inl]. { apply: strict_adjunction => //; first exact: inr_inj. apply/subsetP=> -[//|z _]; exact: codom_f. } rewrite (adjunction_n_comp _ _ _ _ inl_adj) ?(adjunction_n_comp _ _ _ _ inr_adj) //. by rewrite doubleD -!addnA; congr (_ + _); rewrite [RHS]addnC [#|_| + #|_|]addnC -!addnA. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)