proposition: Lemma Exercise5_9a q E: finite_set E -> natp (cardinal (partition_nq E q)).
proof: Proof. move => fE; apply/NatP. have h: sub (partition_nq E q) (partitions E) by apply: Zo_S. have h': sub (partitions E) (\Po (\Po E)) by apply: Zo_S. apply:(sub_finite_set (sub_trans h h')). by apply:setP_finite; apply:setP_finite. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)