proposition: Lemma Exercise5_9f': partition_nq emptyset \0c = C1.
proof: Proof. rewrite / partition_nq /partitions setP_00. apply: set1_pr. apply:Zo_i; last by move => x /in_set0. apply:Zo_i;[ fprops |split; last by move => x /in_set0 ]. by split; [ rewrite setU_0 | move => x y /in_set0 ]. move => x /Zo_P [/Zo_P [ha [_ hb]] hc];case: (emptyset_dichot x)=> // - [t tx]. by move:(card_nonempty1 (hb _ tx) (hc _ tx)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)