proposition: Lemma partdom_trans : transitive partdom.
proof: Proof. move=> s1 s2 s3 /partdomP H12 /partdomP H23. by apply/partdomP => i; exact: (leq_trans (H12 i) (H23 i)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype