hubcap.v

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect.
Require Import ssrbool.
Require Import funs.
Require Import dataset.
Require Import ssrnat.
Require Import seq.
Require Import paths.
Require Import finset.
Require Import connect.
Require Import hypermap.
Require Import geometry.
Require Import quiztree.
Require Import part.
Require Import znat.
Require Import discharge.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

(* Ruling out a part using a combination of discharging and reducibility.    *)
(* In principle, this brings together almost all the elements of the proof   *)
(* development, so for modularity we only import a predicate on parts from   *)
(* the reducibility half, with the assumption that it is always false when   *)
(* the part fits the map. We'll tie up everithing in present.v (anyway,      *)
(* we can't really use the reducibility check in recursive functions, that   *)
(* causes the recursion check to diverge).                                   *)

(* The hubcap concrete syntax is used directly in the source file, so the    *)
(* sector indices start at 1 in the concrete syntax, and are shifted by the  *)
(* parsing and pretty-printing. An additional shift by 2 is done during the  *)
(* verification, to line up with the rules.                                  *)

(* We also define a simpler source cap check, which is used in present12.v   *)
(* to exclude hub sizes greater than 11 (using lemma dscore_cap1).           *)

(* The sequence structure of hubcaps is compressed, not for speed, but to    *)
(* save space in the large proofs generated by the presentation scripts.     *)

Inductive hubcap : Set :=
  | Hubcap0
  | Hubcap1 (j : nat) (b : znat) (hc : hubcap)
  | Hubcap2 (j1 j2 : nat) (b : znat) (hc : hubcap).

Module HubcapSyntax.

Notation "'[]'" := Hubcap0 (at level 8).
Notation "'T' [ j1 ] '<=' b h" := (Hubcap1 (pred j1) (Zpos b) h)
  (at level 8, j1, b at level 0, h at level 9,
   format "'T' [ j1 ] '<=' b  h").
Notation "'T' [ j1 ] '<=' ( - b ) h" := (Hubcap1 (pred j1) (- (Zpos b)) h)
  (at level 8, j1, b at level 0, h at level 9,
   format "'T' [ j1 ] '<=' ( - b )  h").
Notation "'T' [ j1 , j2 ] '<=' b h" := (Hubcap2 (pred j1) (pred j2) (Zpos b) h)
  (at level 8, j1, j2, b at level 0, h at level 9,
   format "'T' [ j1 , j2 ] '<=' b  h").
Notation "'T' [ j1 , j2 ] '<=' ( - b ) h" :=
     (Hubcap2 (pred j1) (pred j2) (- (Zpos b)) h)
  (at level 8, j1, j2, b at level 0, h at level 9,
   format "'T' [ j1 , j2 ] '<=' ( - b )  h").

End HubcapSyntax.

Section Hubcap.

Variables (nhub : nat) (redp : part -> bool) (rf : drule_fork nhub).
Let rs0 := source_drules rf.
Let rt0 := target_drules rf.

Variable g : hypermap.
Hypothesis Hg : plain_cubic_pentagonal g.
Let HgF : pentagonal g := Hg.
Hypothesis Hredp : forall (x : g) p, redp p -> negb (exact_fitp x p).

(* Source bound checking.                                                   *)

Fixpoint check_dbound1_rec (p : part) (rs : drules) (ns m : nat) {struct m}
                       : bool :=
  if m is S m' then
    if rs is Adds r rs' then
      if size rs' < ns then true else
      let p' := meet_part p r in
      (let: SortDrules dns rs'' := sort_drules p' rs' in
       if ns - dns is S ns' then check_dbound1_rec p' rs'' ns' m' else redp p')
      && check_dbound1_rec p rs' ns m'
    else true
  else false.

Definition check_dbound1 p ns :=
  let: DruleFork rs _ _ := rf in check_dbound1_rec p rs ns (size rs + 1).

Lemma check_dbound1P : forall (x : g) p ns,
 arity x = nhub -> exact_fitp x p -> check_dbound1 p ns -> dbound1 rs0 x <= ns.
Proof.
move=> x p ns Hxn; rewrite /check_dbound1 /rs0 /source_drules.
case: rf => rs _ _; move: (size rs + 1) => m.
elim: m ns rs p => // [m Hrec] ns [|r rs] //= p Hxp.
case Hns: (size rs < ns).
  clear; apply: leq_trans Hns.
  by rewrite -add1n; apply leq_add2; [ case (fitp x r) | apply: count_size ].
set p' := meet_part p r; case/andP{Hn}.
case Hxr: (fitp x r); last by clear; apply: Hrec => //=; rewrite Hxr.
have Exp': exact_fitp x p' by apply: exact_fitp_meet.
case/andP: (Exp') => _ Hxp'.
case: (sort_drulesP Hxp' rs) => [dns rs'].
case Dns': (ns - dns) => [|ns']; first by move=> *; case/idPn: Exp'; auto.
have Hns': dns < ns by rewrite ltn_lt0sub Dns'.
move=> Hrsp' _; rewrite -(leq_add_sub (ltnW Hns')) Dns' /=.
rewrite add1n addnS ltnS leq_add2l; eauto.
Qed.

Fixpoint check_unfit (p : part) (ru : drules) {struct ru} : bool :=
  if ru is Adds r ru' then
    if cmp_part p r is Psubset then true else check_unfit p ru'
  else false.

Lemma check_unfitP : forall (x : g) p, fitp x p -> forall ru,
  dbound1 ru x = 0 -> check_unfit p ru = false.
Proof.
move=> x p Hxp; elim=> [|r ru Hrec] //=.
case Hxr: (fitp x r) => // Hru; rewrite {Hrec Hru}(Hrec Hru).
by rewrite (fitp_cmp Hxp) in Hxr; case: (cmp_part p r) Hxr.
Qed.

(* Single target bound checking.                                               *)

Fixpoint check_dbound2_rec (p : part) (rt rs ru : drules) (nt m : nat) {struct m}
                         : bool :=
  if m is S m' then
    if rt is Adds r rt' then
      if size rt' < nt then true else
      let p' := meet_part p r in
      (if check_unfit p' ru then true else
       let: SortDrules dnt rt'' := sort_drules p' rt' in
       let: SortDrules dns rs' := sort_drules p' rs in
       if dns + nt - dnt is S nt' then
          check_dbound2_rec p' rt'' rs' ru nt' m'
       else redp p')
      && check_dbound2_rec p rt' rs (Adds r ru) nt m'
    else true
  else false.

Definition check_dbound2 p b :=
  let: DruleFork rs rt _ := rf in
  let: SortDrules dnt rt' := sort_drules p rt in
  let: SortDrules dns rs' := sort_drules p rs in
  if (dns - dnt + b)%Z is Zpos nt then
    check_dbound2_rec p rt' rs' seq0 nt (size rt' + 2)
  else false.

Lemma check_dbound2P : forall (x : g) p b, arity x = nhub ->
  exact_fitp x p -> check_dbound2 p b -> (dbound2 rt0 rs0 x <= b)%Z.
Proof.
move=> x p b Hxn Exp; rewrite /check_dbound2 /dbound2; case/andP: (Exp) => _ Hxp.
rewrite /rs0 /rt0 /source_drules /target_drules; case: rf => rs rt _.
set ru : drules := seq0; have Hru: dbound1 ru x = 0 by done.
case: {rt}(sort_drulesP Hxp rt)=> dnt rt; set m := size rt + 2.
case: {rs Hxp}(sort_drulesP Hxp rs) => dns rs Hp.
rewrite !zpos_addn -addzA addzCA /leqz -addzA -oppz_sub leqzI oppz_sub.
rewrite addzC -!addzA addzCA (addzA dns).
case: {dns dnt b}(dns - dnt + b)%Z Hp => // nt; rewrite -zpos_addn leqz_nat.
elim: {rt}m nt (rt) rs ru Hru p Exp => // [m Hrec] nt.
case=> //= [r rt] rs ru Hru p Exp; case Hnt: (size rt < nt).
  clear; apply: (leq_trans _ (leq_addl _ _)); apply: leq_trans Hnt.
  by rewrite -add1n; apply leq_add2; [ case (fitp x r) | apply: count_size ].
set p' := meet_part p r; case/andP{Hnt}.
case Hxr: (fitp x r); last by clear; apply: Hrec => //=; rewrite Hxr.
have Exp': exact_fitp x p' by apply: exact_fitp_meet.
case/andP: (Exp') => [_ Hxp'] Hp'rt _; move: Hp'rt.
rewrite (check_unfitP Hxp' Hru).
case: {rt}(sort_drulesP Hxp' rt) => [dnt rt].
case: {Hxp' rs}(sort_drulesP Hxp' rs) => [dns rs].
case Dnt': (subn (addn dns nt) dnt) => [|nt'].
  by move=> *; case/idPn: Exp'; auto.
have Hnt': dnt < dns + nt by rewrite ltn_lt0sub Dnt'.
move=> Hrp'; rewrite -!addnA (addnCA dns) -(leq_add_sub (ltnW Hnt')) Dnt' /=.
rewrite !(addnC dnt) !addnA leq_add2r addnS add1n ltnS; eauto.
Qed.

(* Dual target bound check.                                                      *)

Fixpoint check_2dbound2_rec
          (p1 p2 : part) (rt1 rs1 ru1 rt2 rs2 ru2 : drules) (i nt m : nat)
           {struct m} : bool :=
  if m is S m' then
    if rt1 is Adds r rt1' then
      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) is S nt' then
         check_2dbound2_rec p1' p2' rt1'' rs1' ru1 rt2' rs2' ru2 i nt' m'
       else redp p1')
      && check_2dbound2_rec p1 p2 rt1' rs1 (Adds r ru1) rt2 rs2 ru2 i nt m'
    else
     if rt2 is Seq0 then true else
     check_2dbound2_rec p2 p1 rt2 rs2 ru2 rt1 rs1 ru1 (nhub - i) nt m'
  else false.

Definition check_2dbound2 p1 i b :=
  let p2 := rot_part i p1 in
  let: DruleFork rs rt _ := rf in
  let: SortDrules dnt1 rt1 := sort_drules p1 rt in
  let: SortDrules dns1 rs1 := sort_drules p1 rs in
  let: SortDrules dnt2 rt2 := sort_drules p2 rt in
  let: SortDrules dns2 rs2 := sort_drules p2 rs in
  if ((dns1 + dns2)%dnat - (dnt1 + dnt2)%dnat + b)%Z is Zpos nt then
    let m := size rt1 + (size rt2 + 3) in
    check_2dbound2_rec p1 p2 rt1 rs1 seq0 rt2 rs2 seq0 i nt m
  else false.

Lemma check_2dbound2P : forall (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)%Z.
Proof.
move=> x1 p1 i b Hx1n Ex1p Hi; rewrite /check_2dbound2 /dbound2.
rewrite /rs0 /rt0 /source_drules /target_drules; case: rf => rs rt _.
set ru : drules := seq0; have Hru: forall x : g, dbound1 ru x = 0 by done.
set p2 := rot_part i p1; set x2 := iter i face x1.
move: ru {2 4}ru {Hru}(Hru x1) (Hru x2) => ru1 ru2 Hru1 Hru2.
case/andP: (Ex1p); rewrite Hx1n; move/eqP=> Ep1 Hx1p.
have Ex2p: exact_fitp x2 p2 by rewrite /x2 /p2 -fitp_rot -?Ep1.
case: (sort_drulesP Hx1p rt) => [dnt1 rt1].
case: {Hx1p Ep1}(sort_drulesP Hx1p rs) => [dns1 rs1].
case/andP: (Ex2p) => [_ Hx2p].
case: {rt}(sort_drulesP Hx2p rt) => [dnt2 rt2]; move: (size rt1 + _) => m.
case: {rs Hx2p}(sort_drulesP Hx2p rs) => [dns2 rs2]; rewrite !zpos_addn => Hp.
rewrite -addzA (addzCA (- _)) -oppz_add (addzC dnt1) -addzA 2!(addzA dnt1).
rewrite -(addzA (dnt1 + _)) (addzCA (dnt1 + _)) addzA -oppz_sub.
rewrite (addzC dns1) -(addzA _ dns1) (addzA dns1) (addzC (dns1 + _)).
rewrite /leqz -addzA -oppz_add leqzI addzA -2!addzA (addzA (dns1 + _)).
case: {dns1 dns2 dnt1 dnt2 b}(dns1 + dns2 - (dnt1 + dnt2) + b)%Z Hp => // nt.
rewrite -!zpos_addn -addnA leqz_nat; move: rt2 rs2 ru2 p2 Hru2 Ex2p; rewrite {}/x2.
elim: m rt1 => // m Hrec [|r rt1] /= in nt x1 i Hx1n Hi rs1 ru1 p1 Hru1 Ex1p |- *.
  set x2 := iter i face x1; set i' := nhub - i.
  case=> // r rt; move: {r rt}(Adds r rt) => rt2 rs2 ru2 p2 Hru2 Ex2p.
  rewrite addnC addnCA -[0]/(dbound1 seq0 x1); move: rs1 ru1 p1 Hru1 Ex1p.
  have <-: iter i' face x2 = x1.
    rewrite /x2 -iter_addn addnC /i' leq_add_sub // -Hx1n; exact: iter_face_arity.
  apply: Hrec; auto; [by rewrite /x2 arity_iter_face | exact: leq_subr].
set x2 := iter i face x1 => rt2 rs2 ru2 p2 Hru2 Ex2p.
case Hnt: (size rt1 + size rt2 < nt).
  rewrite addnA => _; apply: leq_trans (leq_addl _ _); apply: leq_trans Hnt.
  rewrite -add1n -addnA; apply leq_add2; first by case (fitp x1 r).
  by apply leq_add2; apply: count_size.
set p1' := meet_part p1 r; case/andP{Hnt}.
case Hxr: (fitp x1 r);
  last by clear; rewrite /= add0n /x2; apply Hrec; rewrite //= Hxr.
have Ex1p': exact_fitp x1 p1' by apply: exact_fitp_meet.
case/andP: (Ex1p'); rewrite Hx1n; move/eqP=> Ep1' Hx1p'.
set p2' := rot_part i p1'.
have Ex2p': exact_fitp x2 p2' by rewrite /x2 /p2' -fitp_rot -?Ep1'.
case/andP: (Ex2p') => [_ Hx2p'] Hp'nt _; move: Hp'nt.
rewrite (check_unfitP Hx1p' Hru1) (check_unfitP Hx2p' Hru2) /=.
case: {rt1}(sort_drulesP Hx1p' rt1) => [dnt1 rt1].
case: {rs1 Hx1p'}(sort_drulesP Hx1p' rs1) => [dns1 rs1].
case: {rt2}(sort_drulesP Hx2p' rt2) => [dnt2 rt2].
case: {rs2 Hx2p'}(sort_drulesP Hx2p' rs2) => [dns2 rs2].
case Dnt': (dns1 + (dns2 + nt) - (dnt1 + dnt2)) => [|nt'].
  by move=> *; case/idPn: Ex1p'; auto.
have Hnt': dnt1 + dnt2 < dns1 + (dns2 + nt) by rewrite ltn_lt0sub Dnt'.
move=> Hrp'; rewrite -!addnA !(addnCA dns1) !(addnCA dns2).
rewrite -(leq_add_sub (ltnW Hnt')) {}Dnt' add1n !addnS ltnS.
rewrite -!addnA -!(addnCA dnt1) -!(addnCA dnt2) !leq_add2l /x2; eauto.
Qed.

(* Cover checking; we compute the multiset of indices in a first pass, then *)
(* check coverage.                                                          *)

Fixpoint tally_hubcap (hc : hubcap) : natseq :=
  match hc with
  | Hubcap1 i _ hc' => incr_sub (tally_hubcap hc') i
  | Hubcap2 i j _ hc' => incr_sub (incr_sub (tally_hubcap hc') i) j
  | _ => seq0
  end.

Fixpoint hubcap_cover_rec (v : natseq) (b : znat) (hc : hubcap) {struct hc}
                          : bool :=
  match hc with
  | Hubcap1 i b' hc' =>
    match sub 0 v i with
    | 1 => hubcap_cover_rec v (b' + (b' + b)) hc'
    | _ => false
    end
  | Hubcap2 i j b' hc' =>
    match sub 0 v i, sub 0 v j with
    | 2, 2 => hubcap_cover_rec v (b' + b) hc'
    | 1, 1 => hubcap_cover_rec v (b' + (b' + b)) hc'
    | _, _ => false
    end
  | Hubcap0 =>
    negb (posz b)
  end.

Definition hubcap_cover hc :=
  let b := dboundK nhub in
  let bb := decz (b + b) in
  let v := tally_hubcap hc in
  and3b (size v =d nhub) (negb (v 0)) (hubcap_cover_rec v bb hc).

Definition hubcap_rot j := rot_part (if j is S (S j') then j' else nhub + j - 2).

Lemma fit_hubcap_rot : forall (x : g) p, arity x = nhub -> exact_fitp x p ->
  forall j, j < nhub -> exact_fitp (iter j face (inv_face2 x)) (hubcap_rot j p).
Proof.
move=> x p Hxn Hxp; have Hn := (ltnW (ltnW (ltnW (HgF x)))); rewrite Hxn in Hn.
case/andP: (Hxp); rewrite Hxn; move/eqP=> Ep _.
case=> [|[|j]] Hj; rewrite -?iter_f.
- rewrite -(iter_face_arity x) Hxn -(leq_add_sub Hn) /hubcap_rot addn0.
  by rewrite /inv_face2 /= !Eface -fitp_rot -?Ep ?leq_subr.
- rewrite -(iter_face_arity x) Hxn -(leq_add_sub (ltnW Hn)) /hubcap_rot addn1.
  by rewrite subSS /inv_face2 /= Enode Eface -fitp_rot -?Ep ?leq_subr.
by rewrite /hubcap_rot /inv_face2 /= !Enode -fitp_rot -?Ep //; do 3 apply ltnW.
Qed.

Definition hub_subn i j := (if j <= i then i else i + nhub) - j.

Lemma hub_subn_hub : forall i j, i < nhub -> j < nhub -> (hub_subn i j) <= nhub.
Proof.
move=> i j Hi Hj; rewrite /hub_subn leq_sub_add.
case: (leqP j i) => Hij; first by apply: (leq_trans (ltnW Hi)); apply leq_addl.
by rewrite leq_add2r; apply ltnW.
Qed.

Lemma iter_hub_subn : forall i j, j < nhub -> forall x : g, arity x = nhub ->
  iter (hub_subn i j) face (iter j face x) = iter i face x.
Proof.
move=> i j Hj x Hxn; rewrite -iter_addn addnC /hub_subn leq_add_sub //.
  by case (j <= i); last by rewrite iter_addn -Hxn iter_face_arity.
by case Hij: (j <= i); last by apply: (leq_trans (ltnW Hj)); apply leq_addl.
Qed.

Fixpoint hubcap_fit (p : part) (hc : hubcap) {struct hc} : bool :=
  match hc with
  | Hubcap1 j b hc' =>
    check_dbound2 (hubcap_rot j p) b && hubcap_fit p hc'
  | Hubcap2 j1 j2 b hc' =>
    check_2dbound2 (hubcap_rot j1 p) (hub_subn j2 j1) b && hubcap_fit p hc'
  | Hubcap0 =>
    true
  end.

Lemma hubcap_fit_bound : forall (x : g) p hc, size_part p = nhub ->
  posz (dscore x) -> hubcap_cover hc && hubcap_fit p hc -> negb (exact_fitp x p).
Proof.
move=> x p hc Ep Hx Hhc; apply/idP => Exp; case/andP: (Exp); rewrite Ep.
move/eqP=> Hxn _; case/idPn: Hx; case/andP: Hhc; case/and3P.
set v := tally_hubcap hc; set b0 := dboundK nhub; move/eqP=> Ev Hv0 Hhc Hhcp.
pose vb (v' : natseq) := forall i, sub 0 v' i <= sub 0 v i.
have Hvb: forall v' i, vb (incr_sub v' i) -> sub 0 v' i < sub 0 v i /\ vb v'.
  move=> v' i Hv'; split; first by move: (Hv' i); rewrite sub_incr_sub set11.
  by move=> j; apply: leq_trans (Hv' j); rewrite sub_incr_sub leq_addl.
pose x' := inv_face2 x.
pose db2 (v' : natseq) (y : g) :=
  let b := dbound2 rt0 rs0 y in
  let i := findex face x' y in
  match sub 0 v' i, sub 0 v i with
  | 1, 1 => (b + b)%Z
  | n, _ => iter n (addz b) 0
  end.
have Hxx': cface x x' by rewrite 2!cface1r /x' /inv_face2 !Enode connect0.
have Edb2: forall v' i, vb (incr_sub v' i) -> i < nhub ->
    let y := iter i face x' in let b := dbound2 rt0 rs0 y in
    let is11 := (sub 0 v' i =d 0) && (sub 0 v i =d 1) in
    let bb := if is11 then (b + b)%Z else b in
    sumz (db2 (incr_sub v' i)) (cface x') = (bb + sumz (db2 v') (cface x'))%Z.
  move=> v' i Hv' Hi y b is11 bb; rewrite -Hxn (arity_cface Hxx') in Hi.
  rewrite 2!(sumz_setID (set1 y) _ (cface x')) addzA; congr addz.
    have Ex'y: setI (cface x') (set1 y) =1 set1 y.
      move=> z; rewrite /setI andbC; case: (y =P z) => // <-.
      by rewrite /y fconnect_iter.
    rewrite !(eq_sumz_r Ex'y) !sumz_set1 /db2 /= /y findex_iter //.
    rewrite sub_incr_sub set11 /= /bb /is11; case/Hvb: Hv'.
    by case: (sub 0 v' i) (sub 0 v i) => [|[|m]] [|[|k]] // _ _; rewrite addz0.
  apply: eq_sumz_l => z; move/andP=> [Hyz Hz]; rewrite /db2 sub_incr_sub.
  case: (i =P findex face x' z) => // Di; case/eqP: Hyz.
  by rewrite /y Di; apply iter_findex.
have Hdb2: negb (posz (decz (b0 + b0) + sumz (db2 v) (cface x'))).
  have Hvbv: vb v by move=> i; apply leqnn.
  move: (decz (addz b0 b0)) Hvbv Hhc Hhcp => b.
  rewrite {1 3}/v -{2}[b]subz0 addzC addz_subA -oppz_sub -leq0z sub0z.
  elim: (hc) b => [|i b' hc' Hrec|j i b' hc' Hrec] b /= Hiv'.
  - rewrite -(@eq_sumz g (@zconst g 0)).
      by rewrite sumz_const leq0z oppz_opp addzC /= addz0.
    by move=> y; rewrite /db2 /= sub_default.
  - case Dvi: (sub 0 v i) (Hvb _ _ Hiv') => [|[|k]] // [Hiv Hv'] Hhc'.
    move/andP=> [Hip Hhc'p]; rewrite ltnS leqn0 in Hiv.
    case: (leqP nhub i) => Hi; first by rewrite sub_default ?Ev in Dvi.
    apply: {Hrec Hv' Hhc' Hhc'p}(leqz_trans (Hrec _ Hv' Hhc' Hhc'p)).
    rewrite leqz_opp2 Edb2 // Dvi Hiv /= !addzA leqz_add2r {b}.
    rewrite addzC -addzA leqz_add2l {db2 Edb2}.
    have Hx'p := fit_hubcap_rot Hxn Exp Hi.
    rewrite (arity_cface Hxx') -(arity_iter_face i x') in Hxn.
    by apply leqz_add2; exact (check_dbound2P Hxn Hx'p Hip).
  case Dvi: (sub 0 v i) (Hvb _ _ Hiv') => [|[|[|k]]] // [Hiv Hjv'];
    case Dvj: (sub 0 v j) (Hvb _ _ Hjv') => [|[|[|k']]] // [Hjv Hv'] Hhc'.
  - move/andP=> [Hijp Hhc'p]; rewrite !ltnS !leqn0 in Hiv Hjv.
    case: (leqP nhub i) => Hi; first by rewrite sub_default ?Ev in Dvi.
    case: (leqP nhub j) => Hj; first by rewrite sub_default ?Ev in Dvj.
    apply: {Hrec Hv' Hhc' Hhc'p}(leqz_trans (Hrec _ Hv' Hhc' Hhc'p)).
    rewrite leqz_opp2 !Edb2 // Dvi Dvj Hiv Hjv /= !addzA leqz_add2r addzC {b}.
    rewrite -!addzA leqz_add2l addzC addzCA !addzA -addzA {db2 Edb2}.
    have Hx'p := fit_hubcap_rot Hxn Exp Hj; rewrite (arity_cface Hxx') in Hxn.
    rewrite -(iter_hub_subn i Hj Hxn); rewrite -(arity_iter_face j x') in Hxn.
    apply leqz_add2; exact (check_2dbound2P Hxn Hx'p (hub_subn_hub Hi Hj) Hijp).
  move/andP=> [Hijp Hhc'p]; rewrite !ltnS in Hiv Hjv.
  case: (leqP nhub i) => Hi; first by rewrite sub_default ?Ev in Dvi.
  case: (leqP nhub j) => Hj; first by rewrite sub_default ?Ev in Dvj.
  apply: {Hrec Hv' Hhc' Hhc'p}(leqz_trans (Hrec _ Hv' Hhc' Hhc'p)).
  rewrite leqz_opp2 !Edb2 // Dvi Dvj !andbF /= !addzA leqz_add2r {b}.
  rewrite addzC {db2 Edb2}leqz_add2l addzC.
  have Hx'p := fit_hubcap_rot Hxn Exp Hj; rewrite (arity_cface Hxx') in Hxn.
  rewrite -(iter_hub_subn i Hj Hxn); rewrite -(arity_iter_face j x') in Hxn.
  exact (check_2dbound2P Hxn Hx'p (hub_subn_hub Hi Hj) Hijp).
set db := (b0 + sumz (dbound2 rt0 rs0) (cface x'))%Z.
suffice: ~ posz (decz (db + db)).
  move=> H; apply/idP => Hx; case: H; move: (dscore_cap2 rf Hg Hxn Hx).
  rewrite -/rs0 -/rt0 -/b0 (eq_sumz_r (same_cface Hxx')) -/db.
  by rewrite decz_def -addzA; case: db => [[|n]|n].
apply: negP; apply: etrans Hdb2 {p Ep Exp vb Hvb Edb2 Hhcp}; congr negb.
congr posz; rewrite !decz_def -!(addzC (-(1))) -!addzA; congr addz.
rewrite /db -!addzA; congr addz; rewrite addzCA -sumz_add; congr addz.
apply: eq_sumz_l => y Hy; rewrite {}/db2.
move: (dbound2 rt0 rs0 y) => b; set i := findex face x' y.
have Hi: i < nhub by rewrite -Hxn (arity_cface Hxx'); apply: findex_max.
case Hi0: (sub 0 v i =d 0).
  by case/idP: Hv0; rewrite -(eqP Hi0) mem_sub ?Ev.
case Dvi: (sub 0 v i) (Hi0) => [|[|[|k]]] //=; first by rewrite addz0.
case/eqP: {b Ev Hv0}Hi0; rewrite /v.
move: v Dvi (decz (b0 + b0)) Hhc => v Dvi.
elim: hc => [|j b' hc' Hrec|j1 j2 b' hc' Hrec] b /=; try by case i.
  rewrite sub_incr_sub; case: (j =P i) => [->|_]; first by rewrite Dvi.
  by case: (sub 0 v j) => [|[|k']] //; apply: Hrec.
rewrite !sub_incr_sub; case: (j1 =P i) => [->|_]; first by rewrite Dvi.
case: (sub 0 v j1) => [|[|[|k1]]] //;
 (case: (j2 =P i) => [->|_]; first by rewrite Dvi);
 case: (sub 0 v j2) => [|[|[|k2]]] //; exact: Hrec.
Qed.

End Hubcap.

Unset Implicit Arguments.