proposition: Lemma genus_patch : genus G = genus Gd + genus Gr.
proof: Proof. pose eb := nilp bG; have ebPd: if eb then bGd = [::] else exists xd, xd \in bGd. by rewrite /eb /bG; case: bGd => [|xd p] //; exists xd; apply: mem_head. have ebPr: if eb then bGr = [::] else exists xr, xr \in bGr. rewrite /eb /nilp -size_rev -DbGr; case: bGr => [|xr p] //=. by exists xr; apply: mem_head. have oGdE: fcard edge Gd = ~~ eb + fcard edge [predC codom hr]. rewrite (n_compC (mem bGd)); congr (_ + _). case: (eb) ebPd => [-> | [xd b_xd]]. by apply: eq_card0 => x; rewrite !inE andbF. by rewrite -(eq_n_comp_r (EbGdE b_xd)) (n_comp_connect cedgeC). have clGr' := predC_closed closed_Gr. rewrite (adjunction_n_comp hd cedgeC cedgeC clGr'). by apply: eq_n_comp_r => x; rewrite !(im_hr, inE) codom_f (mem_map Ihd). apply (strict_adjunction cedgeC clGr' Ihd) => [|xd yd]. by apply/subsetP=> x; rewrite !(im_hr, inE) => /norP[/negbNE]. rewrite !(inE, im_hr) negbK codom_f (mem_map Ihd) /= => b'xd. by rewrite -hdE // (inj_eq Ihd). have oGdF: fcard face Gd = size bG + fcard face (predC outer). rewrite patch_fcard_face_d; congr (_ + _). rewrite (adjunction_n_comp _ cfaceC cfaceC closed_outerC adj_hd). by apply: eq_card => xd; rewrite !inE outer_hd. have oGdN: fcard node Gd = fcard node (codom hd). rewrite (adjunction_n_comp hd cnodeC cnodeC closed_Gd). by apply: eq_card => xd; rewrite !inE codom_f. apply: (strict_adjunction cnodeC closed_Gd Ihd (subxx _)) => xd yd _ /=. by rewrite -hdN (inj_eq Ihd). have oGdG: n_comp glink Gd = ~~ eb + n_comp glink (predC a). have [cG cGd] := (@glinkC G, @glinkC Gd). have hdG xd yd: xd \notin bGd -> glink (hd xd) (hd yd) = glink xd yd. by move=> b'xd; rewrite {1}/glink /= -hdN -hdE -?hdF // !(inj_eq Ihd). have clGa' := predC_closed clGa. have adj_Gd: rel_adjunction hd glink glink (predC a). apply (strict_adjunction cGd clGa' Ihd) => [|xd yd /negbNE/= a'x]. apply/subsetP=> x a'x; have /orP[//| /= xrP] := EhdUr x. by rewrite !inE mem_closure in a'x. by rewrite hdG // -EbGdr (contra ((subsetP (subset_closure _ _)) _) a'x). rewrite (adjunction_n_comp hd cG cGd clGa' adj_Gd). rewrite (n_compC (preim hd a)); congr (_ + _). case: (eb) ebPd => [bGd0 | [xd b_xd]] /=. apply: eq_card0 => xd; apply/nandP; right; apply/exists_inP=> [[y /=]]. rewrite inE -clink_glink => /connectP[p xCp ->{y}] /idPn[]. elim: p xd xCp => /= [|y p IHp] xd; first by rewrite /= EbGdr bGd0. case/andP=> /clinkP[/(canLR nodeK) | ] <-. by rewrite -[xd]edgeK hdN nodeK; apply: IHp. by rewrite -hdF ?bGd0 //; apply: IHp. rewrite -(n_comp_connect cGd xd); apply: eq_n_comp_r => yd; rewrite !inE. apply/exists_inP/idP=> /= [[z] |]. rewrite inE -clink_glink => /connectP[p yCp ->{z}]. elim: p yd yCp => [|z p IHp] yd /= => [_ | /andP[]]. rewrite EbGdr -{b_xd}(EbGdE b_xd). by apply: connect_sub => zd _ /eqP <-; rewrite connect1 ?glinkE. case/clinkP=> [/(canLR nodeK) | ] <-{z}. rewrite -[yd]edgeK hdN nodeK -(same_connect1r cGd (glinkN _)). exact: IHp. have [| /hdF <-] := boolP (yd \in bGd); last first. by rewrite (same_connect1r cGd (glinkF _)); apply: IHp. rewrite -(EbGdE b_xd) => xdNyd _ _. by apply: connect_sub xdNyd => zd _ /eqP <-; rewrite connect1 ?glinkE. rewrite cGd => /connectP[p yGp Dxd]; rewrite {xd}Dxd in b_xd *. elim: p yd yGp b_xd => [|yd p IHp] xd /= => [_ | /andP[xGy yGp]] b_p. by exists (hd xd); rewrite ?inE ?EbGdr. have [|b'xd] := boolP (xd \in bGd). by exists (hd xd); rewrite ?inE ?EbGdr. have [x xGyd Gr_x] := IHp _ yGp b_p; exists x => //. by apply: connect_trans xGyd; rewrite connect1 ?hdG. have oGrE: fcard edge Gr = fcard edge (codom hr). rewrite (adjunction_n_comp hr cedgeC cedgeC closed_Gr). by apply: eq_card => z; rewrite !inE codom_f. apply (strict_adjunction cedgeC closed_Gr Ihr (subxx _)) => xr yr _ /=. by rewrite -hrE (inj_eq Ihr). have oGrN: fcard node Gr = ~~ eb + fcard node [predC codom hd]. have clGd' := predC_closed closed_Gd. rewrite (adjunction_n_comp hr cnodeC cnodeC clGd'). rewrite (n_compC [preim hr of codom hd]); congr (_ + _). case: (eb) ebPr => [bGr0 | [xr b_xr]] /=. by apply: eq_card0 => x; rewrite !inE EbGrd bGr0 andbF. rewrite -(n_comp_connect cnodeC xr); apply: eq_n_comp_r => y /=. by rewrite !inE EbGrd (EbGrN b_xr). apply (strict_adjunction cnodeC clGd' Ihr) => [|xr yr /=]. by apply/subsetP => x; rewrite !(im_hd, inE) => /norP[/negbNE]. by rewrite negbK !inE EbGrd -(inj_eq Ihr) => /hrN->. rewrite {1}/genus -(subnDl (Euler_lhs Gd + Euler_lhs Gr)). rewrite addnC {1 4 5}/Euler_lhs !even_genusP /Euler_rhs (n_compC a). rewrite (n_compC (mem (codom hr))) (n_compC (mem (codom hd))) (n_compC outer). rewrite oGdE oGdF -oGdN oGdG -oGrE -patch_fcard_face_r oGrN -oaGr !doubleD. rewrite -!addnA -(addnn (~~ eb)) (addnCA #|Gd|) (addnA #|Gd|) card_patch. rewrite -!addnA -!(addnCA (~~ eb)) !subnDl addnCA !subnDl. rewrite -(addnCA #|G|) subnDl addnC -!addnA !(addnCA (genus Gr).*2). rewrite -doubleD; do 2!rewrite addnA addnCA subnDl. rewrite -!addnA !subnDl; do 2!rewrite addnCA subnDl. by rewrite addKn half_double addnC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry jordan color coloring)