proposition: Lemma sumn_take_merge t x i : is_part t -> sumn (take i.+1 (merge geq [:: x] t)) = maxn (sumn (take i.+1 t)) (x + sumn (take i t)).
proof: Proof. elim: t i => /= [i _| t0 t IHt i /andP[Hhead Hpart]]. by rewrite addn0 max0n. case: (leqP t0 x) => [/maxn_idPr Hxt0 | /ltnW /maxn_idPl Hxt0]; case: i => [|i]; rewrite /= ?take0 /= ?addn0 ?Hxt0 //. - rewrite {IHt} [x + (t0 + _)]addnC -addnA -addn_maxr [_ + x]addnC. congr (t0 + _); apply esym; apply/maxn_idPr. move: Hxt0 => /maxn_idPr/(leq_trans Hhead). elim: t i Hpart {Hhead t0} => [i _ _| t0 t IHt [|i] /andP[Hhead Hpart] /= Ht0] //=. + by rewrite take0 !addn0. + rewrite [x + (t0 + _)]addnC -addnA leq_add2l addnC. exact: (IHt i Hpart (leq_trans Hhead Ht0)). - move/(_ _ Hpart) : IHt => /= ->. by rewrite [x + (t0 + _)]addnC -addnA -addn_maxr [_ + x]addnC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype