proposition: Theorem cardinal_le_setCP a b: cardinalp a -> cardinalp b -> ((b <=c a) <-> (exists2 c, cardinalp c & b +c c = a)).
proof: Proof. move=> ca cb; split. by move/cdiff_pr => H; exists (a -c b) => //; apply: CS_diff. by move=> [c cc <-]; apply:csum_M0le. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)