fact: Definition redpart p (nhub := size_part p) (ahub := qarity_of_nat nhub) := let fix loop d p' := if d is d'.+1 then red_zpart ahub (loop d') (rev_part p') p' else false in (nhub == ahub) && loop (nhub * 12) p.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)