proposition: Fact setpart1_subproof : partition [set [set x] | x in S] S.
proof: Proof. apply/and3P; split. - rewrite eqEsubset /cover; apply/andP; split; apply/subsetP=> x. + move/bigcupP=> [/= P /imsetP[y yinS ->{P}]]. by rewrite inE=> /eqP->. + move=> xinS; apply/bigcupP=> /=; exists [set x]; last exact: set11. exact: imset_f. - apply/trivIsetP=> A B /imsetP[x _ ->{A}] /imsetP[y _ ->{B}]. by rewrite disjoints1 inE; apply contra=> /eqP ->. - apply/imsetP=> [][x _] /(congr1 (fun A : {set T} => x \in A)). by rewrite !inE eqxx. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition