proposition: Lemma cpow_less_pr12 x: regular_cardinal x -> x ^<c x = x.
proof: Proof. move => /regular_cardinalP [ix cx]; move: (ix) => [cax _]. have aux: x ^c \1c = x by rewrite cpowx1. have x1:=(infinite_gt1 ix). apply: cleA; last by rewrite - {1} aux; apply cpow_less_pr2. apply: (card_ub_sup cax) => i. move /funI_P => [z] /(cardinals_ltP cax) zx ->. case: (equal_or_not z \0c) => zz. by rewrite zz cpowx0; move: x1 => []. rewrite (infinite_power10_b); fprops; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)