proposition: Lemma supp_right_unbounded_p2 c: znat_fam c -> ~ supp_right_unbounded c -> exists2 i, intp i & forall j, i <=z j -> zpartial_sum c j = zpartial_sum c i.
proof: Proof. move => ha hn. case:(all_exists_dichot1 (fun i =>exists2 j, i <=z j & Vg c j <> \0c) BZ)=>//. move => [i iz]. case:(all_exists_dichot2 (fun j => i <=z j /\ Vg c j <> \0c) BZ); last first. by move => [j ja [jb jc]]; case; exists j. move => hyp _. have h: forall j, i <=z j -> Vg c j = \0c. by move => j le;ex_middle bad; case: (hyp _ (proj32 le)). exists i => //. apply: BZ_induction_pos => // j lij. rewrite (zpartial_sum_rec ha (proj32 lij)) (h _ lij). by rewrite (BZsum_0r (zpartial_sum_int ha (proj32 lij))). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)