proposition: Lemma supp_left_unbounded_p4 c (x := zpartial_sum c) (i := zpartial_sum_least x): znat_fam c -> ~ supp_left_unbounded c -> (exists2 i, intp i & Vg c i <> \0c) -> [/\ intp i, x i <z x (BZsucc i), forall j, j <=z i -> x j = x i & forall j, intp j -> x i <=z x j] .
proof: Proof. move => pa pb pc. pose p := (fun i => x i <z x (BZsucc i) /\ forall j , intp j -> x i <=z x j). have Ha: (exists2 i, intp i & p i). move:(supp_left_unbounded_p3 pa pb pc) => [j [ia ib ic]]. by exists j. have Hb: singl_val2 (inc^~ BZ) p. move => a b az p_a bz p_b. case:(zleT_ell az bz) => //. move => /(zlt_succ2P az bz) /(zpartial_sum_mon pa) la. case: (zltNge (zlt_leT (proj1 p_a) la) (proj2 p_b a az)). move => /(zlt_succ2P bz az) /(zpartial_sum_mon pa) la. case: (zltNge (zlt_leT (proj1 p_b) la) (proj2 p_a b bz)). move: (select_pr Ha Hb). rewrite - [select p BZ]/i; move => [[ia ib] ic]. move;split => // j leji. exact: (zleA (zpartial_sum_mon pa leji) (ib _ (proj31 leji))). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)