proposition: Fact part_ordinal1 : partition [set [set x]] [set x].
proof: Proof. rewrite /partition cover1 eq_refl trivIset1 /= in_set1. apply/(introN idP)=> /eqP/setP/(_ x). by rewrite !inE eq_refl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition