proposition: Lemma infinite_power7d x (y := cardinal (cardinals_lt x)): cardinalp x -> x <> \0c -> (y <=c x /\ y <> \0c).
proof: Proof. move=> cx xnz;rewrite -(card_card cx); split. apply:sub_smaller=> t /Zo_P [_ ok]; move: (oclt ok). by move =>/ oltP0 [_ _]. apply: card_nonempty1; exists \0c. by apply /(cardinals_ltP cx); split; [apply: cle0x | apply:nesym ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)