proposition: Lemma part_set1_eq (P : {set {set T}}) : partition P [set x] -> P = [set [set x]].
proof: Proof. move=> /[dup] /and3P[H1 _ Hn0] /triv_part; apply. move: H1; rewrite eqEsubset=> /andP[subPx /subsetP/(_ x)]. rewrite inE=> /(_ (eq_refl _))/bigcupP[/= A AinP xinA]. suff <- : A = [set x] by []. apply/eqP; rewrite eqEsubset. apply/andP; split; last by apply/subsetP=> y; rewrite inE=> /eqP->{y}. exact: (subset_trans (bigcup_sup _ _) subPx). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition