proposition: Lemma partition_nq_pr4 E: cardinal (partition_nq E \0c) = Yo (E = emptyset) \1c \0c.
proof: Proof. case: (equal_or_not E emptyset) => ee; Ytac0;last first. by case:(partition_nq_pr3 E) => // ->; rewrite cardinal_set0. have ha: inc emptyset (partition_nq E \0c). apply:Zo_i; last by move => p /in_set0. apply:Zo_i; [ apply:setP_0i | split; first split ]. - by rewrite setU_0 ee. - by move => a b /in_set0. - by move => a /in_set0. have hb: forall z, inc z (partition_nq E \0c) -> z = emptyset. move => z /Zo_P [/Zo_P [ra [rb rc]] rd]. move: ra; rewrite ee setP_0 setP_1 => /set2_P; case => // zz. have: inc emptyset z by rewrite zz; fprops. by move/rc => /nonemptyP. by rewrite (set1_pr ha hb) cardinal_set1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)