proposition: Lemma partition_nq_pr7 E n q: \0c <c q -> cardinal E = q *c n -> nonempty (partition_nq E q).
proof: Proof. have H: forall A B, B \Eq A -> nonempty A -> nonempty B. move => A B /card_eqP ca /nonemptyP /card_nonempty0 cb. by case: (emptyset_dichot B)=> // bE; case: cb; rewrite - ca bE cardinal_set0. move=> qp eq1; move:(proj32_1 qp) => cq. have e1: E \Eq q \times n by apply/card_eqP; rewrite eq1 - cprod2_pr1. apply: (H _ _ (partition_nq_pr6d q e1)); clear H eq1 e1. set X := fun_image n (indexed q). have ra: forall x, inc x X -> cardinal x = q. by move => x /funI_P [i _ ->]; rewrite cardinal_indexed (card_card cq). have rb:inc X (\Po (\Po (q \times n))). apply/setP_P => t/funI_P [z zn ->]. apply/setP_P => s /setX_P [ha hb /set1_P hc]. by apply/setX_P; split => //;rewrite hc. have rc:alls X nonempty. move=> x /ra cx; apply/nonemptyP => xe. by case: (proj2 qp); rewrite - cx xe cardinal_set0. have rd:union X = q \times n. set_extens t. move /setU_P => [y ty yx]; move/setP_P: rb=> xa. by move/setP_P:(xa _ yx); apply. move => /setX_P [pa pb pc]; apply/setU_P; exists (indexed q (Q t)). apply/setX_P; split => //; fprops. apply/funI_P; ex_tac. have he:disjoint_set X. move => a b /funI_P [a' _ ->] /funI_P [b' _ ->]. by apply:disjoint_pr1 => x /setX_P [_ _ /set1_P <-] /setX_P [_ _ /set1_P <-]. exists X; apply:Zo_i => //; apply: Zo_i => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)