proposition: Lemma zpartial_sum_mon c n m: znat_fam c -> n <=z m -> zpartial_sum c n <=z zpartial_sum c m.
proof: Proof. move => ha hb. move: (zleR (zpartial_sum_int ha (proj31 hb))) => hh. move: m hb; apply:(BZ_induction_pos) => // m lnm Hrec; apply: (zleT Hrec). have mz := (proj32 lnm). rewrite (zpartial_sum_rec ha mz). apply: (BZsum_Mp (zpartial_sum_int ha mz)). by apply: BZ_of_natp_i; move: ha =>[qa qb qc]; apply: qc; ue. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)