proposition: Lemma radius2P : reflect (exists2 x, x \in A & {subset A <= at_radius2 x}) radius2.
proof: Proof. apply: (iffP pred0Pn) => [[x /andP[]] | [x]] Ax /subsetP; exists x => //. by rewrite !inE Ax. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup geometry color chromogram)