proposition: Lemma supp_left_unbounded_p1 c b: znat_fam c -> intp b -> supp_left_unbounded c -> exists2 i, intp i & zpartial_sum c i <=z b.
proof: Proof. move => ha bz hyp. have h := ZS0. case/BZ_i2P: bz => bzz. move/zlt0xP: bzz => /proj1 bzz. by exists \0z; [apply:h | rewrite zpartial_sum_00]. move: (BZ_valN (BZm_sBZ bzz)) => nN. rewrite - (BZm_hi_pr bzz). move: (P b) nN; clear b bzz; apply: Nat_induction. exists \0z => //. by rewrite /ZNo (Y_true (erefl \0c)) zpartial_sum_00; apply: (zleR h). move => n nN [i iN le1]. move:(ZS_pred iN) => piz. move: (hyp _ piz) => [j lij etc]; move: (proj31 lij) => jz. exists j => //. have wz := (zpartial_sum_int ha jz). have le2: BZsucc j <=z i. by rewrite - (BZsucc_pred iN); apply/ (BZsum_le2r jz piz ZS1). apply/(zle_diffP wz (BZm_of_nat_i (NS_succ nN))). rewrite - BZopp_p /BZdiff - (BZoppD (ZNz (NS_succ nN)) wz). apply: BZopp_negative2; rewrite BZsumC -(BZsucc_N nN). apply/zge0xP; rewrite (BZsumA wz (ZNz nN) ZS1). move: (zleT (zpartial_sum_mon ha le2) le1). rewrite (zpartial_sum_rec ha jz). have vN: natp (Vg c j) by move: ha => [_ qa qb]; apply: qb; ue. move: (ZNz vN) => vz. move/(zle_diffP (ZSs wz vz) (BZm_of_nat_i nN)). rewrite - BZopp_p /BZdiff - (BZoppD (ZNz nN) (ZSs wz vz)). move/BZopp_positive2; rewrite (BZopp_K (ZSs (ZNz nN) (ZSs wz vz))). move/zge0xP; rewrite BZsumC (BZsum_AC wz vz (ZNz nN)). apply: zleT. apply/(BZsum_le2l ZS1 vz (ZSs wz (ZNz nN))). apply/(zle_cN NS1 vN). apply: (cge1 (CS_nat vN) etc). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)