proposition: Lemma cpow_less_pr10 x: singular_cardinal x -> (cpow_less_ecb x) -> \2c ^c x = \2c ^<c x.
proof: Proof. move => [icx sx] [a ax ha]. have H:=(cofinality_card icx). have cg:= (cofinality_small icx). have [c [ac cf cx]]: exists c, [/\ a <=c c, \cf x <=c c& c <c x]. have ca:= proj31_1 ax. have cx:=(proj31 cg); have le1:= (cleR cx); have le2:= (cleR ca). case: (cleT_ee ca cx) => h; first by exists (\cf x). by exists a. have p2: (\2c ^<c x) = \2c ^c c. apply: cleA (cpow_less_pr2 \2c cx). apply: card_ub_sup ;first fprops. move=> i /funI_P [z zi ->]. move: zi => /(cardinals_ltP (proj1 icx)) zx. case: (cleT_ee (proj31_1 zx) (proj31_1 cx)) => zc. apply: cpow_Mlele ; fprops. rewrite - (ha _ (cleT ac zc) zx); apply: cpow_Mlele ; fprops. move: (cpow_less_pr6a icx). move: (cofinality_infinite icx); rewrite H => coi. have cnz := (infinite_nz coi). rewrite p2 - cpow_pow cprod_inf//; apply (cle_inf_inf coi cf). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)