proposition: Lemma sum_minn s b : \sum_(l <- s) minn l b = sumn s - \sum_(l <- s) (l - b).
proof: Proof. elim: s => [|s0 s IHs] /=; first by rewrite !big_nil !sub0n. rewrite !big_cons {}IHs minnE. case: (leqP s0 b) => [le_s0_b | /ltnW le_b_s0]. - have:= le_s0_b; rewrite -subn_eq0 => /eqP ->; rewrite add0n subn0. by rewrite addnBA // sumnE; apply: leq_sum => n _; apply: leq_subr. - rewrite subKn // subnDA subnBA // -addnA [s0 + _]addnC addnK [_ + b]addnC. by rewrite addnBA // sumnE; apply: leq_sum => n _; apply: leq_subr. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)