proposition: Lemma triad_valid (cc : seq G) x0 : sparse (insertE cc) -> size cc = 4 -> triad (insertE cc) x0 -> forall p, ~ contract_ring cc p.
proof: Proof. move=> cc_sparse cc4 triad_x0 p cc_p. have p_le5: size p <= 5 by rewrite -cc4; apply: (contract_ring_max cc_p). have{cc_p}[[URp nt_p cc_p] nt0p] := (cc_p, sparse_contract_ring cc_sparse cc_p). case: (size p =P 5) (Birkhoff cexG p_le5 URp) => [sz_p triv1p | _ /idP[]//]. have [y0 sAy0Fp]: exists y0, {subset adj y0 <= fband p}. have [y sAyFp | no_y] := pickP (fun y => adj y \subset fband p). by exists y; apply: (subsetP sAyFp). have [[y0 dFy0] [y1 dFCy1]] := nontrivial0P _ nt0p. case/nontrivial1P: triv1p; split. have /subsetPn[y /adjP[z y0Fz zRy] pF'y] := no_y y0. exists y0 => //; exists (face (edge z)); last first. by rewrite (same_cface y0Fz) -cface1r bridge'G. rewrite /rlink cface1 (closed_connect (diskF_face p) y0Fz) in zRy dFy0. rewrite !inE (closed_connect (fbandF p) zRy) (fclosed1 (diskN_node p)). by rewrite pF'y edgeK; case/andP: dFy0. have /subsetPn[y /adjP[z y1Fz zRy] pF'y] := no_y y1. exists y1 => //; exists (face (edge z)); last first. by rewrite (same_cface y1Fz) -cface1r bridge'G. rewrite /rlink cface1 (closed_connect (diskFC_face p) y1Fz) in zRy dFCy1. rewrite !inE (closed_connect (fbandF p) zRy) (fclosed1 (diskN_node p)). by rewrite pF'y edgeK; case/andP: dFCy1. have sFpAy0: {subset fband p <= adj y0}. move=> x pFx; apply: contraLR (pentaG y0) => not_y0Ax. rewrite -size_spoke_ring -sz_p -ltnNge. have URy0 := scycle_spoke_ring cexG y0. rewrite -(scycle_fcard_fband URp) -(scycle_fcard_fband URy0). rewrite [rhs in _ < rhs](cardD1 (froot face x)) inE (roots_root cfaceC). rewrite /= -(closed_connect (fbandF p) (connect_root _ x)) pFx. apply/subset_leq_card/subsetP => y /andP/=[Dy]. rewrite fband_spoke_ring => y0Ay. rewrite !inE Dy sAy0Fp // -(eqP Dy) (sameP eqP (rootP cfaceC)). by rewrite cfaceC (no_adj_adj not_y0Ax y0Ay). have [z /andP/=[pF'z] | p_cc] := pickP [predD insertE cc & fband p]. rewrite mem_insertE // => /hasP[z1 /rot_to[i cc1 Dcc1] z1Ez]. case/eqP/idPn: sz_p; rewrite neq_ltn orbC ltnNge p_le5 -cc4 ltnS. rewrite -(size_rot i cc) Dcc1 /=; apply: contract_ring_max; split=> // t p1t. have{p1t} [p_t] := (mem_behead p1t, cc_p t p1t). rewrite !mem_insertE // -(has_rot i) Dcc1 /=; case/orP=> //. rewrite cedgeC -(same_cedge z1Ez) plain_orbit // !inE => /pred2P[] Dt. by case/hasP: pF'z; exists t => //; rewrite Dt. case/hasP: pF'z; exists (next p t); first by rewrite mem_next. by rewrite -[z]ee -Dt; case/andP: URp => cycRp _; apply: (next_cycle cycRp). have [[x0Fy0 [_] | x0F'y0 []]] := (boolP (cface x0 y0), andP triad_x0). case/subsetP=> x cc_c; rewrite inE (adjF x0Fy0) [adj _ _]sFpAy0 //. by apply: contraFT (p_cc x); rewrite !inE => ->. rewrite ltnNge (leq_trans _ (fcard_adj_max cexG x0F'y0)) //. apply: (@leq_trans (count (mem (fband (insertE cc))) (spoke_ring x0))). rewrite /spoke_ring count_map; elim: (orbit face x0) => //= z q IHq. rewrite rev_cons -cats1 count_cat /= -(fclosed1 (fbandF _)) addn0. by rewrite addnC leq_add2r. rewrite -size_filter -simple_fcard_fband; last first. have /andP[_] := scycle_spoke_ring cexG x0; rewrite !simple_recI. elim: (spoke_ring x0) => //= z q IHq /andP[qF'z /IHq]. case: ifP => //= ccEFz; rewrite (contra _ qF'z) => // /hasP[t]. by rewrite mem_filter => /andP[_ qt] tFz; apply/hasP; exists t. apply/subset_leq_card/subsetP => z; rewrite !inE => /andP[-> /hasP[t]]. rewrite mem_filter /= => /andP[/hasP[u ccEu tFu] x0r_t] zFt; apply/andP; split. apply: contraFT (p_cc u) => /= /contra-> //. by rewrite (adjFr zFt) (adjFr tFu) => /sFpAy0. by rewrite -fband_spoke_ring; apply/hasP; exists t. 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)