proposition: Lemma cpow_less_ec_pr0 x y: infinite_c y -> \2c <=c x -> infinite_c (x ^<c y).
proof: Proof. move => icy x2. have pa: forall n, natp n -> n <=c x ^<c y. move => n nN; apply (cleT (proj1 (cantor (CS_nat nN)))). move: nN => /NatP nN. apply: cleT _ (cpow_less_pr2 x (clt_fin_inf nN icy)). by apply: cpow_Mleeq => //; apply: card2_nz. apply: (cle_inf_inf CIS_omega). by rewrite omega_limit0; apply: (card_ub_sup (proj32 (pa _ NS2))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)