proposition: Lemma zpartial_sum_p1 c n: natp n -> zpartial_sum c (ZNo n) = ZNo (csumb n (fun i => Vg c (ZNo (csucc i)))).
proof: Proof. move => nN; rewrite /zpartial_sum. case: (equal_or_not n \0c) => nz. have aux: ZNo \0c = \0z by rewrite /ZNo; Ytac0. by rewrite nz aux (Y_true ZpS0) BZ0_val /csumb !csum_trivial; aw. move: (BZm_of_natms_i nN nz) => /BZ_di_neg_pos vn. by rewrite (Y_false vn) BZm_of_nat_val. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)