proposition: Lemma rowpartnE d : rowpartn d = (if d is 0 then [::] else [:: d]) :> seq nat.
proof: Proof. by rewrite /rowpartn -lock. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype