proposition: Lemma supp_left_unbounded_p2 c: znat_fam c -> ~ supp_left_unbounded c -> exists2 i, intp i & forall j, j <=z i -> zpartial_sum c j = zpartial_sum c i.
proof: Proof. move => ha hn. case:(all_exists_dichot1 (fun i =>exists2 j, j <=z i & Vg c j <> \0c) BZ)=>//. move => [i iz]. case:(all_exists_dichot2 (fun j => j <=z i /\ Vg c j <> \0c) BZ); last first. by move => [j ja [jb jc]]; case; exists j. move => hyp _. have h: forall j, j <=z i -> Vg c j = \0c. by move => j le;ex_middle bad; case: (hyp _ (proj31 le)). exists i => //. apply: BZ_induction_neg => // j lij; move: (proj31 lij) => jz. rewrite - {1} (BZsucc_pred jz). have aux: BZpred j <=z i. exact (zleT (proj1 (zlt_pred jz)) lij). rewrite (zpartial_sum_rec ha (ZS_pred jz)) (h _ aux). by rewrite (BZsum_0r (zpartial_sum_int ha (ZS_pred jz))). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)