proposition: Lemma trivial_hom_ring x p : pre_hom_ring x p -> fcard face (diskF (map h (x :: p))) <= 0 -> rlink (last x p) x.
proof: Proof. rewrite leqNgt => xHRp /(fcard0P (diskF_face _))/(introN existsP)/existsPn-pF_0. elim: {p}_.+1 x {-2}p (ltnSn (size p)) pF_0 xHRp => // n IHn x p. rewrite ltnS; set xp := x :: p => le_p_n pF_0 [xRp p_ac URhp]. set y := last x p; have xp_y: y \in xp := mem_last x p. have xp_hy: h y \in map h xp := map_f h xp_y. have ac_y: ac y := p_ac y xp_y. have xpFnhy: node (h y) \in fband (map h xp). apply: contraR (pF_0 (node (h y))); rewrite !inE => ->. by rewrite -(fclosed1 (diskN_node _)) diskN_E xp_hy. have:= xpFnhy; rewrite unfold_in has_map => /hasP[z xpz] /=. rewrite cfaceC => zFnhy. have p_hz: h z \in map h xp by apply: map_f. case/splitPl Dp: p / (xpz) => [p1 p2 Lp1]. case/lastP: p2 Dp => [|p2 y1] Dp. by rewrite /y Dp cats0 Lp1 -{1}[h z]nodeK -cface1 cfaceC bridge'Gm in zFnhy. have Dy1: y1 = y by rewrite /y Dp last_cat last_rcons. case/lastP: p1 => [|p1 z1] /= in Lp1 Dp. case/andP: URhp; rewrite /= Dp map_rcons !rcons_path last_rcons => /andP[_]. rewrite Lp1 (rlinkFr zFnhy) Dy1 -[node (h y)]nodeK. by rewrite /rlink -cface1r cface1 (canRL nodeK (n3m _)) bridge'Gm. rewrite last_rcons in Lp1; rewrite {z1}Lp1 {y1}Dy1 in Dp. pose eny := edge (node y). have ac_eny: eny \in ac by rewrite (fclosed1 acF) nodeK. have h_eny: h eny = edge (node (h y)) by rewrite -[y]nodeK hF ?faceK. have enyRz: rlink eny z. case p_hny: (node (h y) \in map h xp). case/mapP: p_hny => [t xpt Dht]. case/splitPl Dp3: p / (xpt) => [p3 p4 Lp3]. have Dp4: p4 = [:: y]. case: p4 => [|t1 [|t2 p4]] in Dp3 *. - rewrite cats0 in Dp3; rewrite -Dp3 -/y in Lp3. by have /idP[] := bridge'Gm (h t); rewrite -{2}Dht cface1r nodeK Lp3. - by rewrite /y Dp3 last_cat. case/andP: URhp; rewrite /= Dp3 map_cat rcons_cat -cat_cons cat_path. rewrite last_map Lp3 simple_cat /= => /and3P[_ htRt1 _] /and3P[_ _]. rewrite simple_cons -map_cons unfold_in => /andP[/hasP[]]. exists (h y); first by rewrite map_f // /y Dp3 last_cat /= mem_last. by rewrite -(same_cface htRt1) -Dht cface1 nodeK. have Dt: t = node y. move: xRp; rewrite Dp3 cat_path Lp3 Dp4 => /and3P[_ tRy _]. have ac_et: edge t \in ac by rewrite (closed_connect acF tRy). apply/edgeI/cface_inj_embed=> //; first by rewrite cface1r nodeK. by rewrite embed_functor -?Dht // p_ac. case: p2 Dp (congr1 (last x \o belast x) Dp) => [|z1 p2] Dp. rewrite Dp3 Dp4 /= !belast_cat !last_cat /= last_rcons Lp3 => <-. by rewrite /rlink e2c Dt. rewrite Dp3 Dp4 /= !belast_cat /= Lp3 !last_cat /= belast_rcons /= => Lp2. case/andP: URhp => _; rewrite Dp (lastI z1) -Lp2 cat_rcons -cat_cons. rewrite map_cat !map_cons simple_cat !simple_cons => /and4P[_ _]. by rewrite unfold_in !map_rcons !has_rcons orbCA -Dht zFnhy. pose q := rcons p2 eny. have henyFy: cface (h eny) (h y) by rewrite cface1 h_eny nodeK. have zHRq: pre_hom_ring z q. apply: intro_pre_hom_ring => [||t|]. - move: xRp; rewrite Dp cat_path last_rcons => /andP[_]. by rewrite !rcons_path {4}/rlink cface1r nodeK. - by rewrite /rlink last_rcons cfaceC (same_cface zFnhy) h_eny e2m. - rewrite -rcons_cons mem_rcons inE => /predU1P[-> // | p2t]. by rewrite p_ac // Dp cat_rcons -rcons_cons -cats1 inE !mem_cat p2t !orbT. rewrite -{q}rcons_cons map_rcons simple_rcons. rewrite (closed_connect (fbandF _) henyFy) -simple_rcons. case/andP: URhp => _; rewrite Dp cat_rcons -cat_cons -rcons_cons. by rewrite map_cat -map_rcons simple_cat => /and3P[]. rewrite -(last_rcons z p2 eny) -/q IHn // => [|u]. apply: leq_trans le_p_n; rewrite Dp size_cat !size_rcons. by rewrite addSnnS leq_addl. have hxpFeny: h eny \in fband (map h xp) by apply/hasP; exists (h y). have Ehzq: chord_ring (map h xp) (h eny) = map h (rotr 1 (z :: q)). rewrite -rcons_cons rotr1_rcons !map_cons; congr (_ :: _). have <-: h y = fproj (map h xp) (h eny). have [xpj] := fprojP hxpFeny. by rewrite (same_cface henyFy); apply: (scycle_cface URhp). rewrite h_eny e2m. have <-: h z = fproj (map h xp) (node (h y)). have [xpj] := fprojP xpFnhy. by rewrite -(same_cface zFnhy); apply: (scycle_cface URhp). case/andP: URhp => _ /simple_uniq. rewrite -map_cons -/xp -(rotrK 1 xp) map_rot rot_uniq => Up. rewrite arc_rot //; last by apply map_f; rewrite mem_rotr. move: Up; rewrite /xp Dp -cat_cons -rcons_cat rotr1_rcons -rcons_cons. by rewrite cat_rcons map_cons map_cat !map_cons; apply: right_arc. rewrite -[z :: q](rotrK 1) map_rot /= diskF_rot -Ehzq. rewrite diskF_chord_ring // ?h_eny ?e2m //. - by rewrite negb_and pF_0 orbT. - by rewrite /xp Dp (headI p2); case: (p1) => [|? []]. rewrite -(fclosed1 (diskE_edge _ _)) // inE /= p_hny -map_cons -/xp. by rewrite -(fclosed1 (diskN_node _)) diskN_E xp_hy. have ac_ny: node y \in ac. by rewrite -[node y]e2c (closed_connect acF enyRz) p_ac. have h_ny: h (node y) = node (h y). by apply edgeI; rewrite -h_eny -embed_functor. pose enny := edge (node (node y)). have ac_enny: enny \in ac by rewrite (fclosed1 acF) nodeK. have h_enny: h enny = edge (node (node (h y))). by rewrite -h_ny -[node y]nodeK (hF ac_enny) faceK. have hyRx: rlink (h y) (h x). by case/andP: URhp; rewrite /= rcons_path last_map => /andP[_]. have ennyRx: rlink enny x. have [|p'nnhy] := boolP (node (node (h y)) \in map h xp). case/mapP=> t xpt Dht; case/splitPl Dp4: p / xpt => [p3 p4 Lp3]. have Dp3: p3 = [::]. case: p3 => //= t1 p3 in Dp4 Lp3 *; case/andP: URhp => _. rewrite /rlink -[h y]n3m cface1 nodeK Dht in hyRx. rewrite map_cons simple_cons {1}Dp4 -cat_cons lastI Lp3 cat_rcons. by rewrite map_cat fband_cat /= fband_cons cfaceC hyRx !orbT. rewrite -{}Lp3 {p3 p4 Dp4}Dp3 /= in Dht. have Dp1: p1 = [::]; last rewrite {p1}Dp1 /= in Dp. case: p1 Dp => // x1 p1 Dp. case/andP: URhp; rewrite Dp /= => /andP[hxRx1 _]. rewrite !simple_cons cat_rcons map_cat fband_cat /= => /and3P[_ /negP[]]. rewrite orbC fband_cons -(same_cface hxRx1) cfaceC -Dht cface1r nodeK. by rewrite zFnhy. suffices Dx: x = node (node y) by rewrite /rlink e2c -Dx. move: xRp; rewrite Dp /= => /andP[xRz _]. have ac_ex: edge x \in ac by rewrite (closed_connect acF xRz) p_ac. rewrite /rlink e2c -[node y]nodeK -/enny -cface1 in enyRz. rewrite cfaceC -(same_cface xRz) in enyRz; apply/edgeI/cface_inj_embed=> //. by rewrite (embed_functor (p_ac _ (mem_head _ _)) ac_ex) -Dht. pose q := rcons p1 enny. have hennyFz: cface (h enny) (h z) by rewrite cface1 h_enny nodeK cfaceC. have xHRq: pre_hom_ring x q. apply: intro_pre_hom_ring => [||t|]. - move: xRp; rewrite Dp cat_path andbC => /andP[_]. by rewrite !rcons_path -(rlinkFr enyRz) e2c {4}/rlink cface1r nodeK. - by rewrite last_rcons h_enny /rlink e2m (canRL nodeK (n3m _)) -cface1. - rewrite -rcons_cons mem_rcons inE => /predU1P[-> //|p1t]. by rewrite p_ac // Dp cat_rcons -cat_cons mem_cat p1t. rewrite {}/q -rcons_cons map_rcons simple_rcons. rewrite (closed_connect (fbandF _) hennyFz) -simple_rcons. case/andP: URhp => _; rewrite -map_rcons Dp -cat_cons map_cat. by rewrite simple_cat => /and3P[]. rewrite -(last_rcons x p1 enny) -/q IHn // => [|u]. apply: leq_trans le_p_n; rewrite Dp size_cat !size_rcons. by rewrite -addSnnS leq_addr. have xpFhenny: h enny \in fband (map h xp) by apply/hasP; exists (h z). rewrite /rlink -[h y]n3m cface1 nodeK in hyRx. have xpFnnhy: node (node (h y)) \in fband (map h xp). by apply/hasP; exists (h x); first apply: mem_head. have Ehzq: chord_ring (map h xp) (h enny) = map h (rotr 1 (x :: q)). rewrite /q -rcons_cons rotr1_rcons map_cons; congr (_ :: _). have <-: h z = fproj (map h xp) (h enny). have [xpj] := fprojP xpFhenny. by rewrite (same_cface hennyFz); apply: (scycle_cface URhp). have <-: h x = fproj (map h xp) (edge (h enny)). have [xpj] := fprojP xpFnnhy. rewrite (same_cface hyRx) h_enny e2m; apply: (scycle_cface URhp) => //. exact: mem_head. case/andP: URhp => _ /simple_uniq. by rewrite /xp Dp cat_rcons map_cons map_cat !map_cons; apply: left_arc. rewrite -[x :: q](rotrK 1) map_rot /= diskF_rot -Ehzq. rewrite diskF_chord_ring // ?h_enny ?e2m //. - by rewrite negb_and pF_0 orbT. - by rewrite /xp Dp (headI p2); case: (p1) => [|x1 []]. rewrite -(fclosed1 (diskE_edge _ _)) // inE /= p'nnhy. by rewrite -!(fclosed1 (diskN_node _)) diskN_E xp_hy. by rewrite /rlink e2c (canRL nodeK (n3c _)) -?cface1 // [~~ _]ac_bc in ennyRx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color chromogram coloring patch) fourcolor(snip revsnip kempe birkhoff contract)