proposition: Lemma check_2dbound2P (x : G) p i b : arity x = nhub -> exact_fitp x p -> i <= nhub -> check_2dbound2 p i b -> (dbound2 rt0 rs0 x + dbound2 rt0 rs0 (iter i face x) <= b)%R.
proof: Proof. move: x p => x1 p1 nFx1 Exp1 ub_i; rewrite /check_2dbound2 /dbound2. rewrite /rs0 /rt0 /source_drules /target_drules; case: rf => rs rt _. set ru : drules := [::]; have b1ru (x : G): dbound1 ru x = 0 by []. set p2 := rot_part i p1; set x2 := iter i face x1. move: ru {2 4}ru {b1ru}(b1ru x1) (b1ru x2) => ru1 ru2 b1ru1 b1ru2. have [/eqP Ep1 fit_p1] := andP Exp1; rewrite nFx1 in Ep1. have Exp2: exact_fitp x2 p2 by rewrite /x2 /p2 -fitp_rot -?Ep1. have [dnt1 rt1] := sort_drulesP fit_p1 rt. have{fit_p1 Ep1} [dns1 rs1] := sort_drulesP fit_p1 rs. have [_ fit_p2] := andP Exp2. have{rt} [dnt2 rt2] := sort_drulesP fit_p2 rt; move: (size rt1 + _) => m. have{fit_p2} [dns2 rs2] := sort_drulesP fit_p2 rs; rewrite !PoszD => b2p. rewrite addrACA -opprD addrACA [rhs in (- rhs)%R]addrACA opprD [leLHS]addrACA. rewrite -ler_subr_addl opprB [rhs in (_ <= rhs)%R]addrC ler_subl_addl. case: {dns1 dns2 dnt1 dnt2 b}(_ + b)%R b2p => // nt; rewrite lez_nat. move: @x2 rt2 rs2 ru2 p2 b1ru2 Exp2 => /=. elim: m rt1 => // m IHm [|r rt1]/= in nt x1 i nFx1 ub_i rs1 ru1 p1 b1ru1 Exp1 *. set x2 := iter i face x1; set i1 := nhub - i. case=> // r rt; move: {r rt}(r :: rt) => rt2 rs2 ru2 p2 b1ru2 Exp2. rewrite ![_ + dbound1 _ x2]addnC -[0]/(dbound1 [::] x1). move: rs1 ru1 p1 b1ru1 Exp1. have <-: iter i1 face x2 = x1. by rewrite -iterD subnK // -nFx1 iter_face_arity. by apply: IHm => //; rewrite ?arity_iter_face ?leq_subr. set x2 := iter i face x1 => rt2 rs2 ru2 p2 b1ru2 Exp2. case: ifP => [lt_rt_nt _ | _ /andP[]]. apply: leq_trans (leq_addl _ _); apply: leq_trans lt_rt_nt. by rewrite -add1n addnA !leq_add ?leq_b1 ?count_size. case fit_r: (fitp x1 r); last by clear 1; apply: IHm; rewrite //= fit_r. set p11 := meet_part p1 r; set p21 := rot_part i p11. have Exp11: exact_fitp x1 p11 by apply: exact_fitp_meet. have [/eqP Ep11 fit_p11] := andP Exp11; rewrite nFx1 in Ep11. have Exp21: exact_fitp x2 p21 by rewrite -fitp_rot -?Ep11. have [_ fit_p21] := andP Exp21 => check_p _; move: check_p. rewrite (check_unfitP fit_p11) // (check_unfitP fit_p21) //=. have{rt1} [dnt1 rt1] := sort_drulesP fit_p11 rt1. have{rs1 fit_p11} [dns1 rs1] := sort_drulesP fit_p11 rs1. have{rt2} [dnt2 rt2] := sort_drulesP fit_p21 rt2. have{rs2 fit_p21} [dns2 rs2] := sort_drulesP fit_p21 rs2. case Dnt1: (_ - _) => [|nt1]; first by move/redpP/negP/(_ Exp11). have le_dn: dnt1 + dnt2 <= dns1 + (dns2 + nt) by rewrite ltnW // -subn_gt0 Dnt1. move=> check_m; rewrite -addnA addnACA (addnACA dns1) add1n -ltn_subRL. rewrite -addnA addnCA -[_ + nt]addnA -addnBA // Dnt1 addnS ltnS. exact: IHm check_m. 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)