proposition: Lemma zpartial_sum_p3 c n: znat_fam c -> natp n -> zpartial_sum c (ZN (csucc n)) = (zpartial_sum c (ZN n)) +z ZN (Vg c (ZN n)).
proof: Proof. move => [qa qb qc] nN. rewrite (zpartial_sum_p0 _ (NS_succ nN)) (zpartial_sum_p0 _ nN)(csum_fs _ nN). symmetry;apply: BZsum_cN. apply: finite_sum_finite; split. hnf; aw => i lin; rewrite (LgV lin); apply: qc; rewrite qb. apply: (ZNz (NS_inc_nat nN lin)). by aw; apply: finite_set_nat. by apply: qc; rewrite qb; apply: ZNz. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)