proposition: Lemma card_partition_induced1 X f F g: (forall x, inc x X -> inc (f x) F) -> csumb X g = csumb F (fun i => csumb (Zo X (fun z => f z = i)) g).
proof: Proof. move => fim. pose h i := (Zo X (fun z => f z = i)). have pa: (partition_w_fam (Lg F h) (domain (Lg X g))). aw; split; first by fprops. rewrite /h; hnf; aw => i j iF jF. rewrite !LgV //; mdi_tac eq1 => u /Zo_hi fu. by move /Zo_hi => fv; case: eq1; rewrite -fu fv. rewrite /h;set_extens t. by move /setUb_P; aw; move => [y yf]; rewrite LgV//; move => /Zo_P []. move => tx; apply /setUb_P; aw; move: (fim _ tx) => ft; ex_tac. by rewrite LgV//; apply /Zo_P. rewrite {1} /csumb (csum_An pa); aw. apply:csumb_exten => i iF; rewrite /h !LgV//. apply:csumb_exten => z zi; rewrite LgV //; apply: Zo_S zi. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)