fact: Definition zmove zi (x : G) := match zi with | Znil => x | Zhub => x | Zhubl => node x | Zhubr => node (node x) | Zhat => node (edge (node (node x))) | Zhatl => edge (node (node x)) | Zhatr => face (node (node x)) | Zfan0l => face (edge (iter 2 (edge \o node) (node x))) | Zfan1l => face (edge (iter 3 (edge \o node) (node x))) | Zfan2l => face (edge (iter 4 (edge \o node) (node x))) | Zfan3l => face (edge (iter 5 (edge \o node) (node x))) | Zfan0r => edge (iter 2 face (node x)) | Zfan1r => edge (iter 3 face (node x)) | Zfan2r => edge (iter 4 face (node x)) | Zfan3r => edge (iter 5 face (node x)) end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)