proposition: Lemma sum_conj sh k : \sum_(l <- sh) minn l k = sumn (take k (conj_part sh)).
proof: Proof. elim: sh => [// | s0 sh]; first by rewrite big_nil. rewrite big_cons /= => ->; move: (conj_part sh) => c. elim: c s0 k => [// | c0 c IHc] s0 k /=. - rewrite /= addn0. elim: s0 k => [| s IHs] k; first by rewrite min0n. case: k => [| k] /=; first by rewrite minn0. by rewrite minSS IHs add1n. - case: s0 => [| s0]; first by rewrite min0n add0n. case: k => //= k. by rewrite -IHc !addnA minSS addSnnS [minn _ _ + _]addnC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype