proposition: Lemma sumn_add_ribbon : sumn res = nbox.+1 + sumn sh.
proof: Proof. move: Hret; rewrite /add_ribbon. move: (startremE sh nbox.+1 pos) (startrem_leq sh nbox.+1 pos). case: startrem => start [|rem]// Heq /(_ (ltn0Sn _)) lesmin [<- _]. have:= lesmin; rewrite leq_min => /andP[lespos lessz]. rewrite /add_ribbon_on !sumn_cat /= sumn_mapS. rewrite size_drop size_take -/(minn _ _). rewrite sumn_nseq mul1n -(take_takel _ lespos) !addnA. rewrite ![_ + sumn (drop start _)]addnAC -sumn_cat cat_take_drop. rewrite ![_ + (_ - start) + _]addnAC addnBA //. rewrite minnE -addnA (subnKC (leq_subr _ _)) // 2![_ + pos]addnAC. rewrite [sumn (take _ _) + _ ]addnC 2![_ + sumn (take _ _) + _]addnAC Heq. rewrite ![_ + start + _]addnAC addnK [_ + nbox.+1]addnC -!addnA; congr (_ + _). rewrite addnCA sumn_take addnA -big_nat_recr //= -sumn_take. by rewrite -sumn_cat cat_take_drop. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition