proposition: Lemma contract_ring_max (cc p : seq G) : contract_ring cc p -> size p <= (size cc).+1.
proof: Proof. case=> URp nt_p cc_p; pose df x := [predI cc & pred2 x (edge x)]. have Ddf x: x \in behead p -> ~ df x =1 pred0. move=> p1x dfx0; have{p1x}:= cc_p x p1x. rewrite mem_insertE // => /hasP[y cc_y xEy]. by rewrite plain_orbit // !inE in xEy; case/andP: (dfx0 y). have Udf: {in behead p &, injective (fun x => odflt x (pick (df x)))}. move=> x y p1x p1y; have [px py] := (mem_behead p1x, mem_behead p1y). case: pickP => [x1 /andP[/= _ Dx1] | /(Ddf x p1x)[]//]. case: pickP => [y1 /andP[/= _ Dy1] | /(Ddf y p1y)[]] //= eq_xy1. move: eq_xy1 Dx1 Dy1 => -> /pred2P[] -> /pred2P[] // xey; last exact: edgeI. by have:= diskN_edge_ring cexG URp nt_p py; rewrite diskN_E inE /= -xey px. by have:= diskN_edge_ring cexG URp nt_p px; rewrite diskN_E inE /= xey py. have Up1: uniq (behead p). by case: (p) (andP URp) => // x p' [_ /simple_uniq/andP[]]. rewrite -add1n -leq_subLR subn1 -size_behead -(card_uniqP Up1). rewrite -(card_in_image Udf) (leq_trans _ (card_size cc)) //. apply/subset_leq_card/subsetP=> _ /imageP[x p1x ->]. by case: pickP => [x1 /andP[] | /(Ddf x p1x)]. 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)