proposition: Lemma partition_nq_pr3 E: E = emptyset \/ partition_nq E \0c = emptyset.
proof: Proof. case: (emptyset_dichot (partition_nq E \0c))=> h; [by right | left ]. by move: h => [p /partition_nq_pr1]; rewrite cprod0l; apply:card_nonempty. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)