proposition: Lemma Exercise5_9i' E q n: natp n -> natp q -> cardinal E = q *c n -> \0c <c q -> cardinal (partition_nq E q) = csumb (Nintc n) (fun k => (cardinal (Ex59_k_interval E q k))).
proof: Proof. move => nN qN cE qp. move:(Exercise5_9i nN qN cE qp) => [_ ha <-]. by rewrite (csum_pr4 ha);aw; apply:csumb_exten => k kn; rewrite LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)