proposition: Lemma cpow_less_pr11a x y: infinite_c y -> \2c <=c x -> finite_c x -> x ^<c y = y.
proof: Proof. move => icy x2 xf. have cy := proj1 icy. have cs:= (@cpow_less_pr0 y x). have le1: x ^<c y <=c y. apply: card_ub_sup => // i /funI_P [z /(cardinals_ltP cy) zs ->]. have cz:=proj31_1 zs. case: (finite_or_infinite cz) => fz. apply: cle_fin_inf => //. by apply /NatP; apply: NS_pow; fprops; apply /NatP. rewrite (infinite_power1_a x2 (cle_fin_inf xf fz) fz). rewrite - (gch fz). by move: (cnext_pr1 cz) => [_ _ ]; apply. ex_middle neq. move: (cpow_less_pr2 x (conj le1 neq)); set t := (x ^<c y) => le2. move: (cleT (cpow_Mleeq t x2 card2_nz) le2) => le3. case: (cleNgt le3(cantor (proj32 le3))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)