proposition: Lemma Exercise5_5_b2 I: finite_set I -> cardinal (union I) +c csumb (even_card0_sub I) (fun z => cardinal (intersection z)) = csumb (odd_card_sub I) (fun z => cardinal (intersection z)).
proof: Proof. move => h. move: (Exercise5_5_b3 id h);rewrite - setU_prop. set s1 := csumb _ _; set s2 := csumb _ _. set s3 := csumb _ _; set s4 := csumb _ _. have ->: s1 = s3 by apply: csumb_exten => t; rewrite setI_prop. have -> //: s2 = s4 by apply: csumb_exten => t; rewrite setI_prop. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)