proposition: Lemma union_intpartC l k : union_intpart l k = union_intpart k l.
proof: Proof. apply val_inj; rewrite !union_intpartE. by apply/perm_sortP; rewrite // perm_catC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype