proposition: Lemma cnf_subset_finite E c: finite_set E -> natp c -> finite_set (cnf_subset E c).
proof: Proof. move => ha nN. apply: finite_fun_image; apply finite_Zo; apply: setP_finite. apply (finite_prod2 ha). apply/NatP; rewrite (card_card); fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)