fact: Definition get_fan3r p := match p with | Pcons8 _ _ _ f3 _ => f3 | _ => Pr59 end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)