proposition: Lemma Bell_pr E : finite_set E -> cardinal (partitions E) = csumb (Nintc (cardinal E)) (fun p => cardinal (partitionsx E p)).
proof: Proof. set n := cardinal E; move /NatP => nN. suff h: (forall x, inc x (partitions E) -> inc (cardinal x) (Nintc n)). by rewrite (card_partition_induced h); apply:csumb_exten. move => x /Zo_P [] pa [[pb pd] pc]; apply /(NintcP nN). suff: injection (Lf rep x E) by move/inj_source_smaller; aw. apply: lf_injective. by move => t tx; move: (rep_i (pc _ tx)) => h; rewrite - pb; union_tac. move => u v ux vx sr; case: (pd _ _ ux vx) => // bad. empty_tac1 (rep u); first exact: (rep_i (pc _ ux)). rewrite sr;exact: (rep_i (pc _ vx)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)