proposition: Lemma power_cofinality5 x y: \2c <=c x -> infinite_c y -> y <c \cf (x ^c y).
proof: Proof. move => x2 icy. have cx:= proj32 x2. case: (cleT_ee cx (proj1 icy)) => aux. by rewrite (infinite_power1_a x2 aux icy);apply: power_cofinality2. have icx := (cle_inf_inf icy aux). have pi:= (CIS_pow2 icx icy). move:(power_cofinality1 pi). set c := (\cf x ^c y). rewrite - cpow_pow => lt1. move:(cofinality_infinite_cardinal pi) => ww. case: (cleT_el (proj1 ww) (proj1 icy)) => // cy. case: (proj2 lt1);rewrite (cprod_inf cy icy (infinite_nz ww)) //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)