proposition: Lemma sparse_contract_ring (cc : seq G) : sparse (insertE cc) -> forall p, contract_ring cc p -> nontrivial_ring 0 p.
proof: Proof. rewrite /sparse simple_recI /= => cc_sparse. suffices dF_cc p: contract_ring cc p -> ~ diskF p =i pred0. move=> p cc_p; apply/nontrivial0P; split. by apply/existsP/pred0P; apply: dF_cc. have{cc_p} [URp nt_p cc_p] := cc_p. have URp1: scycle rlink (rot 1 p) by rewrite rot_scycle. have/(_ _)/pred0P/existsP[|y] := dF_cc (rev_ring (rot 1 p)); last first. by rewrite diskF_rev_ring ?proper_ring_rot // diskFC_rot; exists y. split=> [||y py]; first exact: scycle_rev_ring. by rewrite proper_rev_ring // proper_ring_rot. suff: edge y \in insertE cc by rewrite !mem_insertE // -(eq_has (cedge1 y)). apply: cc_p; case: (p) py => //= x p1; rewrite rot1_cons /rev_ring. by rewrite -map_rev rev_rcons /= -{1}[y]ee (mem_map edgeI) mem_rev. elim: {p}_.+1 {-2}p (ltnSn (size p)) => // n IHn p le_p_n [URp nt_p cc_p] dF0. have [cycRp /simple_uniq Up] := andP URp. case Dp: p (nt_p) => [|x [|x1 p0]] // _. have p_x: x \in p by rewrite Dp mem_head. have dNx: x \in diskN p by rewrite diskN_E inE Dp /= mem_head. move: (negbT (dF0 (node x))) (negbT (dF0 (node (node x)))). rewrite !inE -!(fclosed1 (diskN_node p)) dNx !andbT !negbK => pFnx pFnnx. have{pFnx} p_nx: node x \in p. without loss dEnx: / node x \in diskE p. by rewrite !inE -(fclosed1 (diskN_node p)) dNx andbT => /wlog_neg. have pFenx: edge (node x) \in fband p. by apply/hasP; exists x; rewrite // -{2}[x]nodeK fconnect1. rewrite (fclosed1 (diskE_edge geoG URp)) in dEnx. have [[pjnx nxFj] [pjenx enxFj]] := (fprojP pFnx, fprojP pFenx). have Djenx: fproj p (edge (node x)) = x. rewrite cface1 nodeK cfaceC in enxFj. by apply: (scycle_cface URp); rewrite // Dp mem_head. have j'x: x != fproj p (node x). apply: contraTneq nxFj => <-; by rewrite -{2}[x]nodeK -cface1r bridge'G. have j'x1: x1 != fproj p (node x). apply: contraTneq nxFj => <-; rewrite cfaceC -[node x]nodeK -cface1r. have:= cycRp; rewrite Dp => /andP[/same_cface <- _]. by rewrite (canRL nodeK (nnn x)) cface1 bridge'G. have [i p1 _ Dp1 -> Eip] := rot_to_arc Up p_x pjnx j'x. rewrite -[node x]ee -{3}Djenx -cat_cons in Eip. case: (IHn (chord_ring p (edge (node x)))) => [||y]; last 1 first. - by rewrite diskF_chord_ring ?ee // inE /= dF0 andbF. - rewrite -ltnS (leq_trans _ le_p_n) // ltnS -(size_rot i p) Eip Dp1 size_cat. by rewrite {2}Dp /arc /= eqxx /= (negPf j'x) (negPf j'x1) !ltnS leq_addl. split=> [||y /= q_y]; try by apply: scycle_chord_ring; rewrite ?ee. by apply: (proper_chord_ring cexG); rewrite ?ee. have p_y: y \in p by rewrite -(mem_rot i) Eip mem_cat q_y orbT. apply: cc_p; rewrite Dp in p_y *; case/predU1P: p_y => // y_x. by rewrite -(rot_uniq i) Eip -{1}y_x /= mem_cat q_y orbT in Up. have{dNx pFnnx p_x n IHn le_p_n dF0 cycRp Up URp} p_nnx: node (node x) \in p. without loss dEnnx: / node (node x) \in diskE p. by rewrite !inE -!(fclosed1 (diskN_node p)) dNx andbT => /wlog_neg. have pFennx: edge (node (node x)) \in fband p. by apply/hasP; exists (node x); rewrite // -{2}[node x]nodeK fconnect1. have [[pjnnx nnxFj] [pjennx ennxFj]] := (fprojP pFnnx, fprojP pFennx). have Djennx: fproj p (edge (node (node x))) = node x. by rewrite cface1 nodeK cfaceC in ennxFj; apply: (scycle_cface URp). have Lp0: last x1 p0 = node x. apply: (can_inj (prev_next Up)). rewrite -(next_rotr 1 Up) {1}Dp lastI rotr1_rcons /= eqxx. apply/esym/(scycle_cface URp); rewrite ?mem_next //. by rewrite -(same_cface (next_cycle cycRp p_nx)) -{2}[x]nodeK fconnect1. have j'nx: node x != fproj p (node (node x)). apply: contraTneq nnxFj => <-. by rewrite -{2}[node x]nodeK -cface1r bridge'G. have j'x: x != fproj p (node (node x)). apply: contraTneq nnxFj => <-. by rewrite (canRL nodeK (nnn x)) cfaceC -cface1r bridge'G. have [i p1 _ Dp1 ->] := rot_to_arc Up p_nx pjnnx j'nx. rewrite -{3}Djennx -cat_cons {p1}Dp1 -{2}[node (node x)]ee -{2}[p](rotrK 1). rewrite arc_rot ?rotr_uniq ?mem_rotr // {2}Dp lastI rotr1_rcons /= Lp0. rewrite {1}/arc /= eqxx /= (negPf j'nx) (negPf j'x) => Eip. case: (IHn (chord_ring p (edge (node (node x))))) => [||y]. - rewrite -ltnS (leq_trans _ le_p_n) // ltnS -(size_rot i p) Eip size_cat. by rewrite !ltnS leq_addl. - split=> [||y /= q_y]; first by apply: scycle_chord_ring; rewrite ?ee. by rewrite proper_chord_ring ?ee -?(fclosed1 (diskE_edge cexG _)). have p_y: y \in p by rewrite -(mem_rot i) Eip mem_cat q_y orbT. apply: cc_p; move: p_y; rewrite Dp => /predU1P[y_x | //]. move: Up; rewrite -(rot_uniq i) Eip/= -[x as X in X \in _]y_x. by rewrite !mem_cat/= q_y orbT andbF. rewrite diskF_chord_ring ?ee //; first by rewrite inE /= dF0 andbF. by rewrite -(fclosed1 (diskE_edge cexG _)). have x'nx := cubic_neq cexG x. have{p_nx} cc_nx: node x \in insertE cc. by apply: cc_p; move: p_nx; rewrite Dp inE x'nx. have{p nt_p p_nnx cc_p x1 p0 Dp} cc_nnx: node (node x) \in insertE cc. by apply: cc_p; move: p_nnx; rewrite Dp inE (canF_eq nnn) eq_sym x'nx. elim: cc cc_sparse cc_nx cc_nnx => [|y cc IHcc] //=. rewrite unfold_in /= !inE => /and3P[/norP[_ yN'cc] eyN'cc cc_sparse]. case/predU1P=> [->|]. rewrite (cubic_neq cexG) [_ == _](contraFF _ (bridge'G (node (node y)))). by move=> cc_ny; case/hasP: yN'cc; exists (node y); rewrite ?fconnect1. by move/eqP=> {2}->; rewrite 2!cface1r -{2}[y]nnn !nodeK. case/predU1P=> [-> | cc_nx]. rewrite (cubic_neq cexG) [_ == _](contraFF _ (bridge'G (face y))) => [?|]. by case/hasP: eyN'cc; exists (node (edge y)); last apply: fconnect1. by rewrite 2!cface1r -(canRL nodeK (nnn _)) (canRL ee (faceK _)) => /eqP->. case/predU1P=> [nnx_y | /predU1P[nnx_ey | /IHcc[]//]]. by case/hasP: yN'cc; exists (node x); last by rewrite cnode1r nnx_y. by case/hasP: eyN'cc; exists (node x); last by rewrite /= cnode1r nnx_ey. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup geometry color coloring patch) fourcolor(snip revsnip birkhoff)