fact: Definition rlink_connected (a : pred G) := {in a &, forall x y, exists2 p, path rlink (node (face x)) (rcons p y) & all a p}.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)