proposition: Lemma sum_diff sh i : \sum_(l <- sh) (l - i) = \sum_(l <- take (nth 0 (conj_part sh) i) sh) (l - i).
proof: Proof. set c := nth 0 (conj_part sh) i. rewrite -{1}(cat_take_drop c sh) !big_cat /=. rewrite [X in _ + X]big_seq [X in _ + X]big1 ?addn0 // => /= j jin. rewrite -(nth_index 0 jin) nth_drop. apply/eqP; rewrite subn_eq0. by rewrite conj_leqE // /c leq_addr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype