proposition: Lemma csum_fs f n: natp n -> csumb (csucc n) f = csumb n f +c (f n).
proof: Proof. move => nN. rewrite (succ_of_nat nN) /osucc /csumb. have eq0: domain (Lg (n +s1 n) f) = (n +s1 n) by aw. have n1:= (Nat_decent nN). have n2: inc n (n +s1 n) by fprops. have n3: sub n (n +s1 n) by fprops. by rewrite (induction_sum1 eq0 n1) restr_Lg // LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)