proposition: Lemma at_radius2P {x y} : fclosed face A -> reflect (exists x', exists2 y', cface x x' /\ cface y y' & edge x' \in A /\ cface (edge x') (edge y')) (at_radius2 x y).
proof: Proof. move=> clFA; apply: (iffP pred0Pn); case. move=> z /and3P[/adjP[y' yFy' y'Rz] /adjP[x' xHx' x'Rz] Az]. exists x', y' => //; split; first by rewrite (closed_connect clFA x'Rz). by rewrite (same_cface x'Rz) cfaceC. move=> x' [y' [xFx' yFy'] [Aex' ex'Fey']]; exists (edge x'). by rewrite !inE /in_mem /= (adjF xFx') (adjF yFy') (adjFr ex'Fey') !adjE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup geometry color chromogram)