proposition: Lemma zpartial_sum_mon_spec c n m j : znat_fam c -> intp n -> intp m -> zbetween j (zpartial_sum c n) (zpartial_sum c (BZsucc m)) -> exists2 p, zbetween_eq p n m & zbetween j (zpartial_sum c p) (zpartial_sum c (BZsucc p)).
proof: Proof. move => ha nZ mZ hb. have lnm: n <=z m. move: hb =>[la lb]. move: (zpartial_sum_mon_bis ha nZ (ZS_succ mZ) (zle_ltT la lb)). by move/(zlt_succ1P nZ mZ). clear mZ; move: m lnm j hb. apply:(BZ_induction_pos). by move => j jj; exists n => //; split; apply: (zleR nZ). move => m lnm Hrec j [ja jb]. move:(proj32 lnm) => mz; move:(ZS_succ mz) => smz. move:(proj1 (zlt_succ mz)) => lmz. have ii: intp (zpartial_sum c (BZsucc m)) by apply:zpartial_sum_int. move:(zleT lnm lmz) (zleR smz) => qa qb. case: (zleT_el ii (proj31_1 jb)) => lb. by exists (BZsucc m). move: (Hrec j (conj ja lb)) => [p [pa pb] pc]. exists p => //; split => //; exact: (zleT pb lmz). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)