proposition: Lemma Exercise5_9e E q n: natp n -> natp q -> \0c <c q -> cardinal E = q *c n -> cardinal (partition_nq E q) = Ex59_val q n.
proof: Proof. move => nN qN qp cE. move:(Exercise5_9b nN qN) => [ha hb hc]. have /(Exercise5_9a q) hd: finite_set E by apply/NatP; rewrite cE; fprops. move: (esym (partition_nq_pr9 nN qN qp cE)); rewrite (cprodC (cardinal _)) => h. exact:(cdivides_pr2 ha hb hd (Exercise5_9b' nN qN) h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)