proposition: Lemma csum2_pr6 a b: cardinal (a \cup b) <=c a +c b.
proof: Proof. rewrite - (setU2Cr2 a b) (csum2_pr5 (set_I2Cr b a)) - (csum2cr a b). rewrite - (csum2cr a); apply: csum_Meqle; apply: sub_smaller; apply: sub_setC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)