proposition: Lemma partsums_cat s1 s2 : s1 != [::] -> s2 != [::] -> partsums (s1 ++ s2) = partsums s1 ++ sumn s1 :: [seq sumn s1 + i | i <- partsums s2].
proof: Proof. case: s1 => // i s _ Hs2; move Hs1 : (i :: s) => s1. have Hszs1 : (size s1).-1.+1 = size s1 by rewrite -Hs1. have Hsz : size s = (size s1).-1 by rewrite -Hs1. rewrite /partsums. have -> : (size (s1 ++ s2)).-1 = (size s1).-1 + size s2. by rewrite -Hs1 /= size_cat. rewrite iotaD map_cat; congr (_ ++ _). apply eq_in_map => [[|l]]; rewrite mem_iota add1n => //=. rewrite -Hsz -/(size (i :: s)) Hs1 => Hl. by rewrite takel_cat // (leq_trans _ Hl). case: s2 Hs2 => // j t _; move Hs2 : (j :: t) => s2. have Hszs2 : (size s2).-1.+1 = size s2 by rewrite -Hs2. rewrite add1n Hszs1 -Hszs2 /= take_size_cat //; congr cons. rewrite -addn1 iotaDl -!map_comp; apply eq_in_map => k /= _. by rewrite take_cat ltnNge leq_addr /= sumn_cat [size s1 + k]addnC addnK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype