proposition: Lemma enum_setpart_set0 : enum (setpart (@set0 T)) = [:: setpart_set0 ].
proof: Proof. move Hl : (enum _)=> l. case: l Hl=> /= [|p0 [|p1 l]] Hl. - exfalso; have:= mem_enum (setpart set0) setpart_set0. by rewrite Hl inE in_nil. - by rewrite (setpart_set0_eq_set0 p0). - exfalso; rewrite (setpart_set0_eq_set0 p0) (setpart_set0_eq_set0 p1) in Hl. by have:= enum_uniq (setpart (@set0 T)); rewrite Hl /= inE eq_refl /=. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition