proposition: Lemma colpartnP x0 d (la : 'P_d) : head x0 la <= 1 -> la = colpartn d.
proof: Proof. move=> /(part_nseq1P (intpartnP _)) Heq. apply val_inj; rewrite /= colpartnE. by rewrite (sumn_intpartn la) in Heq. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype