proposition: Lemma cover_setpart P : cover P = S.
proof: Proof. by case: P => P /= /and3P[/eqP ->]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition