proposition: Lemma fct_sum_rec1 f n: natp n -> csumb (csucc n) f = (csumb n (fun i=> f (csucc i))) +c (f \0c).
proof: Proof. move=> nN. rewrite - (NintE (NS_succ nN)) -(Nint_co_cc nN). rewrite (fct_sum_rec0 _ nN); congr (_ +c (f \0c)). have aux u: inc u n -> cardinalp u. move =>h; exact:(CS_nat (NS_inc_nat nN h)). apply: csum_Cn2; split. + move => t /(NltP nN) => tn; apply /(Nint1cP nN). by split; [ apply: succ_nz | apply/(cleSltP (NS_lt_nat tn nN))]. + by move=> u v un vn;apply: csucc_inj; apply: aux. + move=> y; aw; move/(Nint1cP nN) => [nyz le_s]. have [pN ns] := (cpred_pr (NS_le_nat le_s nN) nyz). exists (cpred y) => //; apply/(NltP nN); apply/(cleSltP pN); ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)