fact: Fixpoint red_popqzp (zp : zpart) (q : question) {struct q} : bool := match q with | Qask0 => true | Qask1 _ => red_pop zp | QaskL qa ql => red_pop zp && red_popqzp (zstepLt zp) ql | QaskR qa qr => red_pop zp && red_popqzp (zstepRt zp) qr | QaskLR qa ql qr => [&& red_pop zp, red_popqzp (zstepL zp) ql & red_popqzp (zstepR zp) qr] | QaskLL qa ql => let zpl := zstepL zp in red_pop zpl && red_popqzp (zstepL zpl) ql | QaskRR qa qr => let zpr := zstepR zp in red_pop zpr && red_popqzp (zstepR zpr) qr end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)