proposition: Lemma check_dbound2P (x : G) p b : arity x = nhub -> exact_fitp x p -> check_dbound2 p b -> (dbound2 rt0 rs0 x <= b)%R.
proof: Proof. move=> nFx Exp; rewrite /check_dbound2 /dbound2; have [_ fit_xp] := andP Exp. rewrite /rs0 /rt0 /source_drules /target_drules; case: rf => rs rt _. set ru : drules := [::]; have bound_ru: dbound1 ru x = 0 by []. have{rt} [dnt rt] := sort_drulesP fit_xp rt; move: (size rt + 2) => m. have{rs fit_xp} [dns rs] := sort_drulesP fit_xp rs. rewrite ler_subl_addl addrAC !PoszD [rhs in (_ <= rhs)%R]addrAC. rewrite -ler_subr_addl [rhs in (_ <= rhs)%R]addrAC. case: {dns dnt b}(_ - _)%R => // [nt]; rewrite -PoszD lez_nat. elim: m nt rt => // m IHm nt [|r rt] //= in rs (ru) bound_ru p Exp *. case: ifP => [lt_rt_nt _ | _ /andP[]]. apply: leq_trans (leq_addr _ _); apply: leq_trans lt_rt_nt. by rewrite -add1n leq_add ?leq_b1 ?count_size. case fit_xr: (fitp x r); last by move=> _ /IHm-> //=; rewrite fit_xr. set p1 := meet_part p r; have Exp1: exact_fitp x p1 by apply: exact_fitp_meet. have [_ fit_xp1] := andP Exp1; rewrite (check_unfitP fit_xp1) //. have [dnt] := sort_drulesP fit_xp1 rt; have [dns] := sort_drulesP fit_xp1 rs. move=> {fit_xp1} {}rs {}rt bound_p1 _. case Dnt1: (_ - dnt) => [|nt1] in bound_p1. by case/idPn: Exp1; apply: redpP. have le_dnt: dnt <= dns + nt by rewrite ltnW // -subn_gt0 Dnt1. rewrite add1n addnCA addnA -ltn_subRL addnC -addnBA // Dnt1 addnC addSn ltnS. exact: 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)