proposition: Lemma zpartial_sum_p0 c n: natp n -> zpartial_sum c (ZN n) = (ZN (csumb n (fun i => Vg c (ZN i)))).
proof: Proof. by move => nN; rewrite /zpartial_sum (Y_true (BZ_of_natp_i nN)) BZ_of_nat_val. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)