proposition: Lemma conj_nseq n : 0 < n -> conj_part (nseq n 1) = [:: n].
proof: Proof. by elim: n => //= [] [|n] // /(_ (ltn0Sn n))->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype