fact: Fixpoint red_qzt_leaf (qtl : quiz_tree) : bool := if qtl is QztLeaf q1 q2 q3 qtl' then if fitqzp zp3 q3 then if fitqzp zp2 q2 then if fitqzp zp1 q1 then [&& red_popqzp zp1 q1, red_popqzp zp2 q2 & red_popqzp zp3 q3] else red_qzt_leaf qtl' else red_qzt_leaf qtl' else red_qzt_leaf qtl' else false.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)