proposition: Lemma cardinals_le_alt a: cardinalp a -> (cardinals_le a) = fun_image (\Po a) cardinal.
proof: Proof. move => h; set_extens t. move/(cardinals_leP h) => ha. move/cardinal_le_aux1: (ha) => /set_leP [y /setP_P yx /card_eqP exy]. by apply /funI_P; ex_tac; rewrite - (card_card (proj31 ha)). move/funI_P => [z /setP_P /sub_smaller ha ->]; apply /(cardinals_leP h). by rewrite - (card_card h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)