proposition: Lemma is_part_nseq1 n : is_part (nseq n 1).
proof: Proof. by elim: n => //= n ->; rewrite andbT; case n. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype