proposition: Lemma fct_sum_rec0 f n: natp n -> csumb (Nintc n) f = (csumb (Nint1c n) f) +c (f \0c).
proof: Proof. move=> nN; move: (Nint_pr5 nN) => [<- aux]. by apply csumA_setU1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)