proposition: Lemma zpartial_sum_int c n: znat_fam c -> intp n -> intp (zpartial_sum c n).
proof: Proof. move => [qa qb qc] nz; move: (BZ_valN nz) => vn. rewrite /zpartial_sum. case: (inc_or_not n BZp) => np; Ytac0. apply:ZNz; apply: finite_sum_finite; split. hnf; aw => i lin; rewrite (LgV lin); apply: qc; rewrite qb. apply: ZNz; exact:(NS_inc_nat vn lin). by aw; apply: finite_set_nat. apply: BZm_of_nat_i; 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 vn lin)). by aw; apply: finite_set_nat. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)