proposition: Lemma Exercise5_5_b1 x y: cardinal x +c cardinal y = cardinal (x \cup y) +c cardinal (x \cap y).
proof: Proof. have di: disjoint (x -s y) (x \cap y). by apply: disjoint_pr => u /setC_P [_ pa] /setI2_P []. move: (csum2_pr5(set_I2Cr x y)); rewrite setU2Cr2 setU2_C => ->. rewrite csum2cr csum2cr - csumA - (csum2_pr5 di). by rewrite - setCC_r setC_v setC_0 csumC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)