fact: Definition zstepRt zp := match zp with | Zpart Zhub _ _ => zshiftr Zhubr zp | Zpart Zhubl _ _ => zshiftl Zhubl zp | Zpart Zhubr pl pr => Zpart Zhat pl pr | Zpart Zhat pl pr => Zpart (zfanR pl) pl pr | Zpart Zhatl pl pr => Zpart Zhub pl pr | Zpart Zhatr _ pr => zshiftr (zfanLt pr) zp | Zpart Zfan0r _ _ => zshiftl Zhatl zp | Zpart Zfan1r pl pr => Zpart Zfan0r pl pr | Zpart Zfan2r pl pr => Zpart Zfan1r pl pr | Zpart Zfan3r pl pr => Zpart Zfan2r pl pr | Zpart _ pl pr => Zpart Znil pl pr end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)