fact: Definition zshiftr zi zp := match zp with | Zpart _ _ (Pcons _ _ Pnil) => Zpart zi p0l p0r | Zpart _ _ (Pcons6 _ _ Pnil) => Zpart zi p0l p0r | Zpart _ _ (Pcons7 _ _ _ Pnil) => Zpart zi p0l p0r | Zpart _ _ (Pcons8 _ _ _ _ Pnil) => Zpart zi p0l p0r | Zpart _ pl (Pcons s h pr) => Zpart zi (Pcons s h pl) pr | Zpart _ pl (Pcons6 h f1 pr) => Zpart zi (Pcons6 h f1 pl) pr | Zpart _ pl (Pcons7 h f1 f2 pr) => Zpart zi (Pcons7 h f1 f2 pl) pr | Zpart _ pl (Pcons8 h f1 f2 f3 pr) => Zpart zi (Pcons8 h f1 f2 f3 pl) pr | Zpart _ _ Pnil => Zpart zi p0rl p0rr end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)