proposition: Lemma supp_left_unbounded_p3 c (x := zpartial_sum c): znat_fam c -> ~ supp_left_unbounded c -> (exists2 i, intp i & Vg c i <> \0c) -> exists i, [/\ intp i, x i <z x (BZsucc i) & forall j, intp j -> x i <=z x j] .
proof: Proof. move => ha hb [k kz xnz]. move:(supp_left_unbounded_p2 ha hb) =>[i]; rewrite -/x => iz ip. have la: x k <z x (BZsucc k). rewrite /x (zpartial_sum_rec ha kz). apply: (BZsum_Mps (zpartial_sum_int ha kz)). have h: natp (Vg c k) by move: ha =>[qa qb qc]; apply: qc; ue. by move:(cpred_pr h xnz) =>[qa ->]; apply: BQpsS_fromN1. case:(zleT_el iz kz); last first. move/(zlt_succ2P kz iz) => lb. case: (proj2 la); rewrite (ip _ lb). exact: (ip _ (zleT (proj1 (zlt_succ kz)) lb)). move => lik. set A := Zo Nat (fun j => x (i +z (ZN j)) <z x (BZsucc (i +z (ZN j)) )). have AN : sub A Nat by apply: Zo_S. have AE: nonempty A. move/(zle_diffP iz kz): lik => dp. move:(BZ_valN (ZS_diff kz iz)) => dN. by exists (P (k -z i)); apply: Zo_i => //; rewrite (BZp_hi_pr dp) BZsum_diff. move: (inf_Nat AN AE); set j := intersection _. move => [/Zo_P [jN ja] jb]. move:(ZSs iz (ZNz jN)) => rz. exists (i +z ZN j); split => //. move => n nz. suff -> : x (i +z ZN j) = x i. case:(zleT_ee nz iz). move/ip => -> ;exact: (zleR (zpartial_sum_int ha iz)). by move/(zpartial_sum_mon ha). suff: forall m, natp m -> m <=c j -> x (i +z ZN m) = x i. apply => //; apply:(cleR (CS_nat jN)). apply: Nat_induction; first by rewrite (BZsum_0r iz). move => m mN Hrec le. rewrite - (Hrec (cleT (cleS mN) le)); ex_middle bad. move/ (cleSltP mN): le => /cltNge; case. have le2: (i +z ZN m) <=z (i +z ZN (csucc m)). apply /(BZsum_le2l (ZNz mN) (ZNz (NS_succ mN)) iz). apply/(zle_cN mN (NS_succ mN)); apply: (cleS mN). have /jb //: inc m A. apply: (Zo_i mN). have<- : (i +z ZN (csucc m)) = (BZsucc (i +z ZN m)). by rewrite /BZsucc- (BZsumA iz (ZNz mN) ZS1) - (BZsucc_N mN). exact: (conj (zpartial_sum_mon ha le2) (nesym bad)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)