proposition: Lemma zpartial_sum_rec c n: znat_fam c -> intp n -> zpartial_sum c (BZsucc n) = (zpartial_sum c n) +z ZN (Vg c n).
proof: Proof. move => cp nz; have mN := BZ_valN nz. case/BZ_i0P: nz => np; last first. rewrite - (BZp_hi_pr np) (BZsucc_N mN); exact: (zpartial_sum_p3 cp mN). move: (BZms_hi_pr np) =>[qa qb]. move: (cpred_pr mN qa) =>[sa sb]. have mz := (ZNz sa). rewrite - qb sb (zpartial_sum_p4 cp sa) - BZopp_p - (BZsucc_N sa). by rewrite /BZsucc (BZoppD mz ZS1) (BZsum_diff1 ZS1 (ZSo mz)) BZopp_p. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)