fact: Fixpoint red_zpart_rec (zp : zpart) (d : nat) : bool := if d isn't d'.+1 then false else let zp' := zshiftr Zhub zp in let: Zpart _ pl pr := zp in let s := get_spoke pr in let sqt := qzt_getr s (qzt_truncate qt) in if (if qzt_proper sqt then let: Zpart _ pl' pr' := zp' in let sl := get_spoke pl in if red_qzt_leaf (Zpart Zhubr pl' pr') (zshiftl Zhubl zp) (Zpart Zhat pl pr) (qzt_getr s (qzt_getr sl (qzt_get1 ahub qt))) then red_popr_spoke pr && red_popl_spoke pl pr else if red_qzt_leaf (Zpart (zfanLt pr) pl' pr') zp (Zpart (zfanRt pl) pl pr) (qzt_getr (get_hat pr) (qzt_getr sl sqt)) then [&& red_popr_hat pr, red_popl_spoke pl pr & red_popr_spoke pr] else let zpnil := Zpart Znil pl' pr' in match pr with | Pcons Pr55 h _ => if red_qzt_leaf (Zpart Zhatr pl' pr') (Zpart Zhatl pl pr) zpnil (qzt_getr (get_hat pr') (qzt_getr h sqt)) then red_popr_hat pr' && red_popr_hat pr else false | Pcons6 h f1 _ => if red_qzt_leaf (Zpart Zfan0l pl' pr') (Zpart Zhatl pl pr) zpnil (qzt_getr f1 (qzt_getr h sqt)) then red_popl_fan1r pl' pr' && red_popr_hat pr else if red_qzt_leaf (Zpart Zhatr pl' pr') (Zpart Zfan0r pl' pr') zpnil (qzt_getr (get_hat pr') (qzt_getr f1 sqt)) then red_popr_hat pr' && red_popl_fan1r pl' pr' else false | Pcons7 h f1 f2 _ => if red_qzt_leaf (Zpart Zfan1l pl' pr') (Zpart Zhatl pl pr) zpnil (qzt_getr f1 (qzt_getr h sqt)) then red_popl_fan1r pl' pr' && red_popr_hat pr else if red_qzt_leaf (Zpart Zfan0l pl' pr') (Zpart Zfan0r pl' pr') zpnil (qzt_getr f2 (qzt_getr f1 sqt)) then red_popl_fan2r pl' pr' && red_popl_fan1r pl' pr' else if red_qzt_leaf (Zpart Zhatr pl' pr') (Zpart Zfan1r pl' pr') zpnil (qzt_getr (get_hat pr') (qzt_getr f2 sqt)) then red_popr_hat pr' && red_popl_fan2r pl' pr' else false | Pcons8 h f1 f2 f3 _ => if red_qzt_leaf (Zpart Zfan2l pl' pr') (Zpart Zhatl pl pr) zpnil (qzt_getr f1 (qzt_getr h sqt)) then red_popl_fan1r pl' pr' && red_popr_hat pr else if red_qzt_leaf (Zpart Zfan1l pl' pr') (Zpart Zfan0r pl' pr') zpnil (qzt_getr f2 (qzt_getr f1 sqt)) then red_popl_fan2r pl' pr' && red_popl_fan1r pl' pr' else if red_qzt_leaf (Zpart Zfan0l pl' pr') (Zpart Zfan1r pl' pr') zpnil (qzt_getr f3 (qzt_getr f2 sqt)) then red_popl_fan3r pl' pr' && red_popl_fan2r pl' pr' else if red_qzt_leaf (Zpart Zhatr pl' pr') (Zpart Zfan2r pl' pr') zpnil (qzt_getr (get_hat pr') (qzt_getr f3 sqt)) then red_popr_hat pr' && red_popl_fan3r pl' pr' else false | _ => false end else false) then true else red_zpart_rec zp' d'.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)