fact: Definition subpart_loc_move i g x := match i with | Pspoke => @edge g x | Phat => edge (iter 2 face (edge x)) | Pfan1 => edge (iter 3 face (edge x)) | Pfan2 => edge (iter 4 face (edge x)) | Pfan3 => edge (iter 5 face (edge x)) end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)