fact: Fixpoint check_dbound1_rec (p : part) (rs : drules) ns m {struct m} : bool := if m is m'.+1 then if rs is r :: rs' then if size rs' < ns then true else let p' := meet_part p r in (let: SortDrules dns rs'' := sort_drules p' rs' in if ns - dns is ns'.+1 then check_dbound1_rec p' rs'' ns' m' else redp p') && check_dbound1_rec p rs' ns m' else true else false.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) mathcomp(bigop order ssralg ssrnum ssrint) fourcolor(hypermap geometry quiztree part discharge)