proposition: Lemma cpow_less_pr8 x: infinite_c x -> (forall y, y<c x -> \2c ^c y <c x) -> [/\ \2c ^c x = gimel_fct x, x <c (\cf (gimel_fct x)) & (\cf x = omega0 -> \2c ^c x = x ^c omega0)].
proof: Proof. move => icx h. have cx := proj1 icx. have pa: \2c ^c x = gimel_fct x. rewrite (cpow_less_pr6a icx). have le1 : (\2c ^<c x) <=c x. apply: card_ub_sup; first exact: cx. move =>i /funI_P [z] /(cardinals_ltP cx) pa. move => ->; apply: (proj1 (h _ pa)). by rewrite (cleA le1 (proj1 (cpow_less_compare icx))). split; first by exact. by rewrite -pa; apply: power_cofinality2. by rewrite pa /gimel_fct => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)