proposition: Lemma intpartn_cons : IntPartN Hlla = rowpartn l0 +|+ IntPartN Hla.
proof: Proof. apply val_inj; rewrite union_intpartnE /= rowpartnE. move: Hlla => /andP[_] Hpart. have:= part_head_non0 Hpart => /=. move: Hpart; rewrite is_part_sortedE => /andP[Hsort _]. case: l0 Hsort => // l Hsort _. apply (sorted_eq (leT := geq)) => //; first exact: sort_sorted. by rewrite perm_sym perm_sort. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype