proposition: Lemma hubcap_fit_bound (x : G) p hc : size_part p = nhub -> (0 < dscore x)%R -> hubcap_cover hc && hubcap_fit p hc -> ~~ exact_fitp x p.
proof: Proof. rewrite -!andbA; set v := tally_hubcap hc; set b0 := dboundK nhub. move=> Ep pos_x /and4P[/eqP-Ev v'0 hc_v hc_p]; apply: contraL pos_x => Exp. pose x1 := inv_face2 x; have x1Fx: cface x1 x by rewrite 2!cface1 !nodeK. have nFx: arity x = nhub by rewrite -Ep; have [/eqP] := andP Exp. have nFx1: arity x1 = nhub by rewrite (arity_cface x1Fx). pose b (y : G) m := (dbound2 rt0 rs0 y *+ m)%R. pose db2 w y (i := findex face x1 y) (w_i := nth 0 w i) (v_i := nth 0 v i) := b y (if w_i > 1 then 2 else if w_i < 1 then 0 else (v_i == 1).+1). pose sum_db2 w := (\sum_(y in cface x1) db2 w y)%R. have{v'0} db2v: {in cface x1, forall y1, db2 v y1 = b y1 2}. move=> y x1Fy; congr (_ *+ _)%R; set i := findex face x1 y. have ltin: i < nhub by rewrite -nFx1 findex_max. by case: ltngtP; rewrite // ltnNge lt0n (memPn v'0) ?mem_nth ?Ev. suffices{db2v}: ~~ (0 < b0 *+ 2 - 1 + sum_db2 v)%R. apply: contra => /(dscore_cap2 rf geoG nFx); rewrite -/rs0 -/rt0 -/b0. rewrite [sum_db2 _](eq_bigr _ db2v) sumrMnl (eq_bigl _ _ (same_cface x1Fx)). by rewrite addrAC subr_gt0 -mulrnDl -!lez_add1r (ler_muln2r 2 1%:Z). pose vb w := forall i, nth 0 w i <= nth 0 v i. have vb_inc w i : vb (incr_nth w i) -> nth 0 w i < nth 0 v i /\ vb w. move=> vb_w; split=> [|j]; first by have:= vb_w i; rewrite nth_incr_nth eqxx. by apply: leq_trans (vb_w j); rewrite nth_incr_nth leq_addl. have db2_inc w i (v_i := nth 0 v i) (w' := incr_nth w i) : vb w' -> i < nhub -> v_i <= 2 -> sum_db2 w' = (b (iter i face x1) (v_i == 1)%N.+1 + sum_db2 w)%R. - case/vb_inc; set w_i := nth 0 w i => lt_wvi _ ltin /(leq_trans lt_wvi)ub_wi. have ltix1: i < arity x1 by rewrite nFx1. rewrite 2![sum_db2 _](bigD1 _ (fconnect_iter _ i _)) addrA /= -mulrnDr. congr (_ *+ _ + _)%R; first rewrite findex_iter // nth_incr_nth eqxx /= -/w_i. by do [rewrite -/v_i; case: eqP w_i => [->|_] [|[|?]]] in lt_wvi ub_wi *. apply: eq_bigr => y /andP[x1Fy x1i'y]; congr (_ *+ _)%R; rewrite nth_incr_nth. by have [Di | //] := i =P _; rewrite Di iter_findex ?eqxx in x1i'y. have: vb v by []; rewrite /v -ltr_subl_addl sub0r -leNgt; clearbody v. elim: hc {b0}(_ - 1)%R hc_v hc_p => /= [|i b1 hc IHhc|j i b1 hc IHhc] b0. - by rewrite -leNgt -oppr_ge0 [sum_db2 _]big1 // => y _; rewrite /db2 nth_nil. - case/andP=> /eqP-Dvi v_hc /andP[p_b1 p_hc] vb_hci. have /vb_inc[_ vb_hc] := vb_hci. have [ltin | leni] := ltnP i nhub; last by rewrite nth_default ?Ev in Dvi. rewrite {}db2_inc ?Dvi {vb_hci}//= -ler_subr_addl -opprD addrC. apply: {IHhc vb_hc v_hc p_hc}(le_trans (IHhc _ v_hc p_hc vb_hc)). rewrite ler_opp2 ler_add2r ler_pmuln2r //. by apply: check_dbound2P p_b1; rewrite ?arity_iter_face ?fit_hubcap_rot. set vj := nth 0 v j => /and3P[/eqP-Dvi vj_le2] v_hc /andP[p_b1 p_hc] vb_hcij. have /vb_inc[_ vb_hcj] := vb_hcij; have /vb_inc[vj_gt vb_hc] := vb_hcj. have{vj_gt} vj_gt0: 0 < vj by apply: leq_trans vj_gt. have [ltin | ?] := ltnP i nhub; last by rewrite Dvi nth_default ?Ev in vj_gt0. have [ltjn | ?] := ltnP j nhub; last by rewrite [vj]nth_default ?Ev in vj_gt0. rewrite !{}db2_inc -?Dvi {vb_hcij vb_hcj}//= addrA -ler_subr_addl -opprD -/vj. apply: {IHhc v_hc p_hc vb_hc}(le_trans (IHhc _ v_hc p_hc vb_hc)). rewrite ler_opp2 addrC ler_add2r -mulrnDl ler_pmuln2r //. rewrite addrC -(iter_hub_subn i ltjn) //. apply: check_2dbound2P p_b1; rewrite ?arity_iter_face ?hub_subn_hub //. by rewrite fit_hubcap_rot. 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)