proposition: Lemma card_partition_induced X f F: (forall x, inc x X -> inc (f x) F) -> cardinal X = csumb F (fun k => cardinal (Zo X (fun z => f z = k))).
proof: Proof. move => fim; rewrite - csum_pr0; apply /card_eqP. rewrite disjointU_E; set S := unionf _ _. exists (Lf (fun x => J x (f x)) X S); hnf; saw; apply lf_bijective. move => x xX; move: (fim _ xX) => ok. by apply /setUf_P; aw; ex_tac; aw; apply: indexed_pi; apply /Zo_P. move => u v _ _ sv; exact: (pr1_def sv). move => y /setUf_P; aw; move => [z zf]; aw. move =>/indexed_P [px /Zo_P [pc pd] pe];ex_tac. by rewrite -{1} px pd pe. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)