proposition: Lemma sub_smaller_contra Z X: Z <=cc X -> exists2 Y, sub Y X & cardinal Z = cardinal Y.
proof: Proof. by move => /eq_subset_cardP1/set_leP [y yx /card_eqP h]; exists y. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)