proposition: Lemma cpradius2P : radius2 (kernel (cfring cf)).
proof: Proof. rewrite /cfring /cfmap -/cp. elim: {-2}(cpksize cp) (leqnn (cpksize cp)) cp_rad2 => //= i IHi lt_cp_i. move: (proper_cpmask1 cp i) (cpmask1 lt_cp_i cp_ok); set G := cpmap cp. set cm0 := cfmask1 cp i; set x0 := nth _ _ i => cm0ok Dcm0. case: (cpadj cm0 cp) (cpadj_proper cm0ok) (cpmask_adj cp_ok cm0ok) => mr1 mk1. case/andP=> _ Emk1; rewrite {}Dcm0 => Ecm1 /=; set cm1 := Cfmask _ mk1. have cm1ok: proper_cpmask cp cm1 by rewrite /= size_nseq eqxx. move: (cpadj_proper cm1ok) (cpmask_adj cp_ok cm1ok). case: (cpadj cm1 cp) => mr2 mk2 /andP[_ Emk2] Ecm2. case: ifP => [mk2T _ {IHi} | _]; last by apply: IHi; apply: ltnW. set kG := kernel _; have DkG: kG =i fband (cpker cp). move=> x; move: (cpmap_simple cp_ok) (cpmap_cover cp_ok x). rewrite simple_cat fband_cat -/G orbC => /and3P[_ UkG _]. rewrite 2!inE /= fband_rev; case: (x \in _) / hasP => [[y kGy xFy]|_ /= ->//]. by rewrite (closed_connect (fbandF _) xFy) (hasPn UkG). have kGx0: x0 \in kG. by rewrite DkG (subsetP (ring_fband _)) ?mem_nth // size_cpker. apply/radius2P; exists x0 => // x kGx; apply/(at_radius2P (kernelF _)). have /hasP[y kGy /adjP[z xFz zRy]]: has (adj x) (cpmask cm1 cp). rewrite -Ecm2 /= fband_cat; apply/orP; right. suffices <-: cpker cp = mask mk2 (cpker cp) by rewrite -DkG. have /all_pred1P->: all (pred1 true) mk2 by apply: sub_all mk2T => [[]]. by rewrite (eqP Emk2) -size_cpker // mask_true. rewrite /= mask_false /= in kGy. have: has (adj (edge z)) [:: x0]. by rewrite -Ecm1 /= fband_cat; apply/orP; right; apply/hasP; exists y. rewrite has_seq1 adjC; last by apply: cpmap_plain; apply: config_prog_cubic. case/adjP=> t x0Ft tRz; exists t; exists z; split=> //; rewrite DkG. by apply/hasP; exists y; [apply (mem_mask kGy) | rewrite (same_cface tRz)]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring patch cfmap quiz)