proposition: Lemma induction_on_sum n f (sum := fun n => csumb n f): natp n -> sum (csucc n) = (sum n) +c (f n).
proof: Proof. move=> nN; rewrite /sum (succ_of_nat nN); apply csumA_setU1. apply:(Nat_decent nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)