proposition: Lemma partdomP s1 s2 : reflect (forall i, sumn (take i s1) <= sumn (take i s2)) (partdom s1 s2).
proof: Proof. by apply (iffP partdomshP) => H i; have:= H i; rewrite ?add0n. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype