proposition: Lemma power_cofinality2 x: infinite_c x -> x <c \cf (\2c ^c x).
proof: Proof. move=> xi;move: (infinite_pow2 xi) => iy. have ynz:= infinite_nz iy. have ia := (cofinality_infinite_cardinal iy). case: (cleT_el (proj1 ia) (proj1 xi)) => le2 //. case: (cltNge (power_cofinality1 iy)). rewrite -{3} (csquare_inf xi) cpow_pow; exact:(cpow_Meqle ynz le2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)