proposition: Lemma partdom_anti s1 s2 : is_part s1 -> is_part s2 -> partdom s1 s2 -> partdom s2 s1 -> s1 = s2.
proof: Proof. move=> H1 H2 /partdomP H12 /partdomP H21. apply sumn_take_inj => // k. by apply anti_leq; rewrite H12 H21. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype