proposition: Lemma partdomshP {n1 n2 s1 s2} : reflect (forall i, n1 + sumn (take i s1) <= n2 + sumn (take i s2)) (partdomsh n1 n2 s1 s2).
proof: Proof. apply (iffP allP) => H i; last by move=> _; exact: H. case: (ltnP i (size s1)) => Hi. - by apply: H; rewrite mem_iota /= add0n ltnS; apply ltnW. - have /H : (size s1) \in iota 0 (size s1).+1. by rewrite mem_iota /= add0n ltnS. rewrite take_size (take_oversize Hi) => /leq_trans; apply. by rewrite leq_add2l; apply: sumn_take_leq. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype