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