proposition: Lemma subdescset_partsumP c1 c2 : reflect {subset partsums c1 <= partsums c2} (descset c1 \subset descset c2).
proof: Proof. apply (iffP subsetP) => Hsub /= i Hin. - have Hi := allP (all_partsums c1) _ Hin. have ltin : i.-1 < n.-1 by case: n i Hi {Hin} => [|n0][|i]. have {Hin}/Hsub : (Ordinal ltin) \in descset c1. by rewrite /descset inE mem_pmap_sub /= map_f. rewrite /descset inE mem_pmap_sub /= {ltin} => /mapP[j Hin Heq]. suff -> : i = j by []. have {Hin} := allP (all_partsums c2) _ Hin. by case: i j Hi Heq => // i [|j] //= _ ->. - case: i Hin => [i Hi] /=. rewrite /descset !inE !mem_pmap_sub /= => /mapP[j /Hsub Hin Heq]. by rewrite Heq map_f. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype