proposition: Lemma partition_nq_pr1 E q p: inc p (partition_nq E q) -> cardinal E = q *c (cardinal p).
proof: Proof. move => /Zo_P [/Zo_P[ ha [[hb1 hb2] hb3]] hc]. have hd:mutually_disjoint (identity_g p). by hnf;rewrite identity_d => i j ip jp; rewrite !identity_ev //; apply: hb2. rewrite - hb1 - setUb_identity (csum_pr4 hd) identity_d. rewrite cprod2cr - csum_of_same; apply: csumb_exten => a ap. by rewrite (identity_ev ap); apply: hc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)