proposition: Lemma supp_right_unbounded_p1 c b: znat_fam c -> intp b -> supp_right_unbounded c -> exists2 i, intp i & b <=z zpartial_sum c i.
proof: Proof. move => ha bz hyp. have h := ZS0. case/BZ_i0P: bz => bzz. move/zgt0xP: bzz => /proj1 bzz. by exists \0z; [apply:h | rewrite zpartial_sum_00]. move: (BZ_valN (BZp_sBZ bzz)) => nN. rewrite - (BZp_hi_pr bzz). move: (P b) nN; clear b bzz; apply: Nat_induction. exists \0z => //; rewrite zpartial_sum_00; apply: (zleR h). move => n nN [i iN le1]. move: (hyp i iN) => [j lij etc]; move: (proj32 lij) => jz. exists (BZsucc j); first by apply: ZS_succ. rewrite (zpartial_sum_rec ha jz). move: (zleT le1 (zpartial_sum_mon ha lij)) => le2. move/ (BZsum_le2r (proj31 le2) (proj32 le2) ZS1): (le2). rewrite -/(BZsucc _) (BZsucc_N nN) => le3; apply: (zleT le3). have vN: natp (Vg c j) by move: ha => [_ qa qb]; apply: qb; ue. apply/(BZsum_le2l ZS1 (ZNz vN) (proj32 le2)); apply/(zle_cN NS1 vN). apply: (cge1 (CS_nat vN) etc). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)