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