proposition: Lemma zpartial_sum_p4 c n: znat_fam c -> natp n -> zpartial_sum c (ZNo (csucc n)) +z ZN (Vg c (ZNo (csucc n))) = zpartial_sum c (ZNo n).
proof: Proof. move => [qa qb qc]nN. rewrite (zpartial_sum_p1 _ (NS_succ nN)) (zpartial_sum_p1 _ nN)(csum_fs _ nN). set u := csumb _ _. have uN: natp u. apply: finite_sum_finite; split. hnf; aw => i lin; rewrite (LgV lin); apply: qc; rewrite qb. apply: BZm_of_nat_i; exact: (NS_succ (NS_inc_nat nN lin)). by aw; apply: finite_set_nat. set v := Vg _ _. have vN: natp v. by apply: qc; rewrite qb; apply: BZm_of_nat_i; exact: (NS_succ nN). move: (ZNz uN) (ZNz vN) => uz vz. rewrite - BZopp_p - (BZsum_cN uN vN) (BZoppD uz vz) (BZsum_diff1 vz (ZSo uz)). by rewrite BZopp_p. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)