proposition: Fact trivsetpart_subproof : partition (T := T) (if S == set0 then set0 else [set S]) S.
proof: Proof. case: (S =P set0) => [-> | /eqP/set0Pn[x xinS]/=]. by rewrite partition_set0. rewrite /partition cover1 eq_refl trivIset1 /=. by rewrite inE eq_sym; apply/set0Pn; exists x. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition