fact: Definition radius2 := ~~ [disjoint A & [pred x | A \subset at_radius2 x]].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup geometry color chromogram)