fact: Fixpoint check_2dbound2_rec p1 p2 (rt1 rs1 ru1 rt2 rs2 ru2 : drules) i nt m {struct m} : bool := if m isn't m'.+1 then false else if rt1 isn't r :: rt1' then if rt2 is [::] then true else check_2dbound2_rec p2 p1 rt2 rs2 ru2 rt1 rs1 ru1 (nhub - i) nt m' else if size rt1' + size rt2 < nt then true else let p1' := meet_part p1 r in let p2' := rot_part i p1' in [&& if check_unfit p1' ru1 || check_unfit p2' ru2 then true else let: SortDrules dnt1 rt1'' := sort_drules p1' rt1' in let: SortDrules dns1 rs1' := sort_drules p1' rs1 in let: SortDrules dnt2 rt2' := sort_drules p2' rt2 in let: SortDrules dns2 rs2' := sort_drules p2' rs2 in if dns1 + (dns2 + nt) - (dnt1 + dnt2) isn't nt'.+1 then redp p1' else check_2dbound2_rec p1' p2' rt1'' rs1' ru1 rt2' rs2' ru2 i nt' m' & check_2dbound2_rec p1 p2 rt1' rs1 (r :: ru1) rt2 rs2 ru2 i nt m'].
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)