proposition: Lemma csum_M0le a b: cardinalp a -> a <=c (a +c b).
proof: Proof. move => ca; rewrite - {1} (card_card ca) - (card_card (CS_sum2 a b)). move:(sub_smaller (@subsetU2l (a *s1 C1) (b *s1 C0))). by rewrite - (disjointU2_pr3 a b C0_ne_C1) cardinal_indexed. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)