proposition: Lemma partition_nq_pr2 E q n p : cardinalp n -> natp q -> q <> \0c -> cardinal E = q *c n -> inc p (partition_nq E q) -> cardinal p = n.
proof: Proof. move => cn qN qnz ha hb. move: (partition_nq_pr1 hb); rewrite ha => hc. by move:(cprod_eq2lx qN cn (CS_cardinal p) qnz hc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)