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