proposition: Lemma induction_sum0 f a b: (~ inc b a) -> csum (restr f (a +s1 b)) = csum (restr f a) +c (Vg f b).
proof: Proof. move => nba; exact: (csumA_setU1 (Vg f) nba). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)