proposition: Lemma check_dbound1P (x : G) p ns : arity x = nhub -> exact_fitp x p -> check_dbound1 p ns -> dbound1 rs0 x <= ns.
proof: Proof. move=> nFx; rewrite /check_dbound1 /rs0 /source_drules. case: rf => rs _ _; move: (size rs + 1) => m. elim: m ns rs p => // m IHm ns [|r rs] //= p fit_xp. case: ifP => [/(leq_trans _)-> //| _ /andP[]]. by rewrite -add1n leq_add ?leq_b1 ?count_size. case fit_xr: (fitp x r); last by clear 1; apply: IHm => //=; rewrite fit_xr. set p1 := meet_part p r. have Efit_p1: exact_fitp x p1 by apply: exact_fitp_meet. have [_ /sort_drulesP[dns rs1]] := andP Efit_p1. case Dns1: (ns - dns) => [|ns1]; first by move/redpP/negP/(_ Efit_p1). have dns_lt_ns: dns < ns by rewrite -subn_gt0 Dns1. move=> bound_p1 _; rewrite -(subnKC (ltnW dns_lt_ns)) Dns1 /=. by rewrite addnCA leq_add2l ltnS; apply: IHm bound_p1. Qed.
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)