proposition: Lemma cpow_less_pr5e x: infinite_c x -> x ^<c omega0 = x.
proof: Proof. move => icx; move: (proj1 icx) => cx. apply: cleA (cpow_less_pr5a cx (infinite_ge2 CIS_omega)). apply: card_ub_sup => // i /funI_P [z za ->]; move: za. move /(cardinals_ltP CS_omega) => za. move: (oclt za) => /oltP0; move=> [_ _ xn]. by apply: cpow_inf1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)