proposition: Lemma union_intpartA l k j : union_intpart l (union_intpart k j) = union_intpart (union_intpart k l) j.
proof: Proof. apply val_inj; rewrite !union_intpartE; apply/perm_sortP => //. apply (perm_trans (y := l ++ (k ++ j))). - by rewrite perm_cat2l perm_sort. - apply (perm_trans (y := (k ++ l) ++ j)). + by rewrite catA perm_cat2r perm_catC. + by rewrite perm_cat2r perm_sym perm_sort. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype